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 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 stringtype update_info = | Proved of bool| Name_change of string| Proof_status_change of Controller_itp.proof_attempt_status
* bool
* Call_provers.resource_limittype 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| Saved| Message of message_notification| Dead of string| Task of node_ID * string * (Loc.position * color) list| File_contents of string * string| Source_and_ce of string * (Loc.position * color) listtype 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 node_ID| Unfocus_req| Save_req| Reload_req| Exit_req| Interrupt_req| Get_global_infosval modify_session : ide_request -> boolval print_request : Format.formatter -> ide_request -> unitval print_msg : Format.formatter -> message_notification -> unitval print_notify : Format.formatter -> notification -> unit