package why3
val root_node : node_IDval is_root : node_ID -> booltype global_information = {provers : (string * string * string) list;transformations : transformation list;strategies : (string * strategy) list;commands : string list;
}type message_notification = | Proof_error of node_ID * string| Transf_error of bool * node_ID * string * string * Loc.position * string * string| Strat_error of node_ID * string| Replay_Info of string| Query_Info of node_ID * string| Query_Error of node_ID * string| Information of string| Task_Monitor of int * int * int| Parse_Or_Type_Error of Loc.position * Loc.position * string| File_Saved of string| Error of string| Open_File_Error of string
type update_info = | Proved of bool| Name_change of string| Proof_status_change of Controller_itp.proof_attempt_status * bool * Call_provers.resource_limit
type notification = | Reset_whole_tree| New_node of node_ID * node_ID * node_type * string * bool| Node_change of node_ID * update_info| Remove of node_ID| Next_Unproven_Node_Id of node_ID * node_ID| Initialized of global_information| Saving_needed of bool| Saved| Message of message_notification| Dead of string| Task of node_ID * string * (Loc.position * color) list * Loc.position option * string| File_contents of string * string * Env.fformat * bool| Source_and_ce of string * (Loc.position * color) list * Loc.position option * Env.fformat| Ident_notif_loc of Loc.position
type ide_request = | Command_req of node_ID * string| Add_file_req of string| Set_config_param of string * int| Set_prover_policy of Whyconf.prover * Whyconf.prover_upgrade_policy| Get_file_contents of string| Get_task of node_ID * bool * bool| Remove_subtree of node_ID| Copy_paste of node_ID * node_ID| Save_file_req of string * string| Get_first_unproven_node of next_unproved_node_strat * node_ID| Find_ident_req of Loc.position| Unfocus_req| Save_req| Reload_req| Check_need_saving_req| Exit_req| Interrupt_req| Reset_proofs_req| Get_global_infos
val print_request : Format.formatter -> ide_request -> unitval print_msg : Format.formatter -> message_notification -> unitval print_notify : Format.formatter -> notification -> unit