sig
  type transformation = string * string
  type strategy = string
  type node_ID = int
  val root_node : Itp_communication.node_ID
  val is_root : Itp_communication.node_ID -> bool
  type global_information = {
    provers : (string * string * string) list;
    transformations : Itp_communication.transformation list;
    strategies : (string * Itp_communication.strategy) list;
    commands : string list;
  }
  type message_notification =
      Proof_error of Itp_communication.node_ID * string
    | Transf_error of bool * Itp_communication.node_ID * string * string *
        Loc.position * string * string
    | Strat_error of Itp_communication.node_ID * string
    | Replay_Info of string
    | Query_Info of Itp_communication.node_ID * string
    | Query_Error of Itp_communication.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 node_type =
      NRoot
    | NFile
    | NTheory
    | NTransformation
    | NGoal
    | NProofAttempt
  type color =
      Neg_premise_color
    | Premise_color
    | Goal_color
    | Error_color
    | Error_line_color
    | Error_font_color
    | Search_color
  type update_info =
      Proved of bool
    | Name_change of string
    | Proof_status_change of Controller_itp.proof_attempt_status * bool *
        Call_provers.resource_limits
  type notification =
      Reset_whole_tree
    | New_node of Itp_communication.node_ID * Itp_communication.node_ID *
        Itp_communication.node_type * string * bool
    | Node_change of Itp_communication.node_ID *
        Itp_communication.update_info
    | Remove of Itp_communication.node_ID
    | Next_Unproven_Node_Id of Itp_communication.node_ID *
        Itp_communication.node_ID
    | Initialized of Itp_communication.global_information
    | Saving_needed of bool
    | Saved
    | Message of Itp_communication.message_notification
    | Dead of string
    | Task of Itp_communication.node_ID * string *
        (Loc.position * Itp_communication.color) list * Loc.position option *
        string
    | File_contents of string * string * Env.fformat * bool
    | Source_and_ce of string *
        (Loc.position * Itp_communication.color) list * Loc.position option *
        Env.fformat
    | Ident_notif_loc of Loc.position
  type next_unproved_node_strat = Prev | Next | Clever
  type config_param = Max_tasks of int | Timelimit of float | Memlimit of int
  type ide_request =
      Command_req of Itp_communication.node_ID * string
    | Add_file_req of string
    | Set_config_param of Itp_communication.config_param
    | Set_prover_policy of Whyconf.prover * Whyconf.prover_upgrade_policy
    | Get_file_contents of string
    | Get_task of Itp_communication.node_ID * bool * bool * bool
    | Remove_subtree of Itp_communication.node_ID
    | Copy_paste of Itp_communication.node_ID * Itp_communication.node_ID
    | Save_file_req of string * string
    | Get_first_unproven_node of Itp_communication.next_unproved_node_strat *
        Itp_communication.node_ID
    | Find_ident_req of Loc.position
    | Unfocus_req
    | Save_req
    | Export_as_zip
    | Reload_req
    | Check_need_saving_req
    | Exit_req
    | Interrupt_req
    | Reset_proofs_req
    | Get_global_infos
  val print_request :
    Stdlib.Format.formatter -> Itp_communication.ide_request -> unit
  val print_msg :
    Stdlib.Format.formatter -> Itp_communication.message_notification -> unit
  val print_notify :
    Stdlib.Format.formatter -> Itp_communication.notification -> unit
end