module Itp_communication:sig
..end
typetransformation =
string * string
typestrategy =
string
typenode_ID =
int
val root_node : node_ID
val is_root : node_ID -> bool
type
global_information = {
|
provers : |
|
transformations : |
|
strategies : |
|
commands : |
}
Global information known when server process has started and that can be shared with the IDE through communication
type
message_notification =
| |
Proof_error of |
|||
| |
Transf_error of |
(* | Transf_error (is_fatal, nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_transf | *) |
| |
Strat_error of |
|||
| |
Replay_Info of |
|||
| |
Query_Info of |
|||
| |
Query_Error of |
(* | General information | *) |
| |
Information of |
(* | Number of task scheduled, running, etc | *) |
| |
Task_Monitor of |
(* | A file was read or reloaded and now contains a parsing or typing error. second loc is relative to the session file | *) |
| |
Parse_Or_Type_Error of |
(* |
| *) |
| |
File_Saved of |
(* | An error happened that could not be identified in server | *) |
| |
Error of |
|||
| |
Open_File_Error of |
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 |
Used to give colors to the parts of the source code that corresponds to the following property in the current task. For example, the code corresponding to the goal of the task will have Goal_color in the source code.
type
update_info =
| |
Proved of |
| |
Name_change of |
| |
Proof_status_change of |
type
notification =
| |
Reset_whole_tree |
|||
| |
New_node of |
(* | Notification of creation of new_node: New_node (new_node, parent_node, node_type, name, detached). | *) |
| |
Node_change of |
(* | inform that the data of the given node changed | *) |
| |
Remove of |
(* | the given node was removed | *) |
| |
Next_Unproven_Node_Id of |
(* | Next_Unproven_Node_Id (asked_id, next_unproved_id). Returns a node and the next unproven node from this node | *) |
| |
Initialized of |
(* | initial global data | *) |
| |
Saving_needed of |
(* | the session needs saving when argument is true | *) |
| |
Saved |
(* | the session was just saved on disk | *) |
| |
Message of |
(* | an informative message, can be an error message | *) |
| |
Dead of |
(* | server exited | *) |
| |
Task of |
(* |
| *) |
| |
File_contents of |
(* | File_contents (filename, contents, format, read_only) | *) |
| |
Source_and_ce of |
(* | Source interleaved with counterexamples: contents and list color loc, loc of the goal, format of the source | *) |
| |
Ident_notif_loc of |
(* | Answer the position where an ident is defined | *) |
type
next_unproved_node_strat =
| |
Prev |
| |
Next |
| |
Clever |
type
config_param =
| |
Max_tasks of |
| |
Timelimit of |
| |
Memlimit of |
type
ide_request =
| |
Command_req of |
|||
| |
Add_file_req of |
|||
| |
Set_config_param of |
|||
| |
Set_prover_policy of |
|||
| |
Get_file_contents of |
|||
| |
Get_task of |
(* |
| *) |
| |
Remove_subtree of |
|||
| |
Copy_paste of |
|||
| |
Save_file_req of |
(* |
| *) |
| |
Get_first_unproven_node of |
|||
| |
Find_ident_req of |
(* |
| *) |
| |
Unfocus_req |
|||
| |
Save_req |
|||
| |
Export_as_zip |
|||
| |
Reload_req |
|||
| |
Check_need_saving_req |
|||
| |
Exit_req |
|||
| |
Interrupt_req |
|||
| |
Reset_proofs_req |
(* | Remove all proofattempt and transformations even proved ones | *) |
| |
Get_global_infos |
val print_request : Stdlib.Format.formatter -> ide_request -> unit
val print_msg : Stdlib.Format.formatter -> message_notification -> unit
val print_notify : Stdlib.Format.formatter -> notification -> unit