Commit 144d6ee3 authored by MARCHE Claude's avatar MARCHE Claude

fix reopened issue #36, introducing a new request Get_global_infos

parent 24e35c79
......@@ -573,7 +573,6 @@ let interpNotif (n: notification) =
PE.error_print_msg
(Format.asprintf "Query error on selected node: \"%s\"" s)
| Query_Info (_nid, s) -> PE.error_print_msg s
| Help s -> PE.error_print_msg s
| Information s -> PE.error_print_msg s
| Error s ->
PE.error_print_msg
......
......@@ -195,23 +195,6 @@ let env, gconfig = try
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(* Initialization of config, provers, task_driver and controller in the server *)
let () =
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:true files
with Invalid_argument s ->
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage spec usage_str
in
Server.init_server gconfig.config env dir;
Queue.iter (fun f -> send_request (Add_file_req f)) files
let () =
Debug.dprintf debug "Init the GTK interface...@?";
ignore (GtkMain.Main.init ());
Debug.dprintf debug " done.@.";
Gconfig.init ()
(********************************)
......@@ -377,6 +360,23 @@ let update_label_saved (label: GMisc.label) =
(* Graphical elements *)
(**********************)
let initialization_complete = ref false
let () =
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:true files
with Invalid_argument s ->
Format.eprintf "Error: %s@." s;
Whyconf.Args.exit_with_usage spec usage_str
in
Server.init_server gconfig.config env dir;
Queue.iter (fun f -> send_request (Add_file_req f)) files;
send_request Get_global_infos;
Debug.dprintf debug "Init the GTK interface...@?";
ignore (GtkMain.Main.init ());
Debug.dprintf debug " done.@.";
Gconfig.init ()
let main_window : GWindow.window =
let w = GWindow.window
......@@ -393,7 +393,8 @@ let main_window : GWindow.window =
(fun {Gtk.width=w;Gtk.height=h} ->
gconfig.window_height <- h;
gconfig.window_width <- w)
in w
in
w
(* the main window contains a vertical box, containing:
1. the menu [menubar]
......@@ -477,13 +478,6 @@ let provers_factory =
(****************************)
(***********************************)
(* connection of actions to signals *)
(***********************************)
......@@ -1591,8 +1585,6 @@ let (_ : GtkSignal.id) =
(* Notification Handling *)
(*************************)
let initialization_complete = ref false
let treat_message_notification msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) ->
......@@ -1625,11 +1617,7 @@ let treat_message_notification msg = match msg with
print_message ~kind:1 ~notif_kind:"Query_info" "%s" s
| Query_Error (_id, s) ->
print_message ~kind:1 ~notif_kind:"Query_error" "%s" s
| Help s ->
print_message ~kind:1 ~notif_kind:"Help" "%s" s
| Information s ->
if not !initialization_complete then main_window#show ();
initialization_complete := true;
print_message ~kind:1 ~notif_kind:"Information" "%s" s
| Task_Monitor (t, s, r) -> update_monitor t s r
| Open_File_Error s ->
......@@ -1637,7 +1625,6 @@ let treat_message_notification msg = match msg with
| Parse_Or_Type_Error (loc, rel_loc, s) ->
if gconfig.allow_source_editing || !initialization_complete then
begin
if not !initialization_complete then main_window#show ();
(* TODO find a new color *)
scroll_to_loc ~force_tab_switch:true (Some (rel_loc,0));
color_loc ~color:Goal_color rel_loc;
......@@ -2205,7 +2192,8 @@ let treat_notification n =
Hint.remove node_id_proved id;
Hint.remove node_id_pa id
| Initialized g_info ->
(* TODO: treat other *)
initialization_complete := true;
main_window#show ();
init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands;
| Saved ->
session_needs_saving := false;
......
......@@ -42,7 +42,6 @@ type message_notification =
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Parse_Or_Type_Error of Loc.position * Loc.position * string
......@@ -117,13 +116,15 @@ type ide_request =
| Reload_req
| Exit_req
| Interrupt_req
| Get_global_infos
(* Return true if the request modify the session *)
let modify_session (r: ide_request) =
match r with
| Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
| Reload_req -> true
| Set_config_param _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Save_req | Exit_req
| Save_req | Exit_req | Get_global_infos
| Interrupt_req | Focus_req _ | Unfocus_req -> false
......@@ -43,7 +43,6 @@ type message_notification =
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
(** General information *)
| Information of string
(** Number of task scheduled, running, etc *)
......@@ -134,6 +133,7 @@ type ide_request =
| Reload_req
| Exit_req
| Interrupt_req
| Get_global_infos
(* Return true if the request modify the session *)
val modify_session: ide_request -> bool
......@@ -273,6 +273,7 @@ let print_request fmt r =
| Reload_req -> fprintf fmt "reload"
| Exit_req -> fprintf fmt "exit"
| Interrupt_req -> fprintf fmt "interrupt"
| Get_global_infos -> fprintf fmt "get_global_infos"
let print_msg fmt m =
match m with
......@@ -282,7 +283,6 @@ let print_msg fmt m =
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
| Query_Error (_ids, s) -> fprintf fmt "query error %s" s
| Help _s -> fprintf fmt "help"
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Parse_Or_Type_Error (_, _, s) -> fprintf fmt "parse_or_type_error:\n %s" s
......@@ -384,6 +384,7 @@ let () =
send_source: bool;
(* If true the server is parametered to send source mlw files as
notifications *)
global_infos : Itp_communication.global_information;
}
let server_data = ref None
......@@ -944,7 +945,7 @@ end
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
| Some _ -> P.notify (Message (Open_File_Error ("File already in session: " ^ fn)))
| Some _ -> P.notify (Message (Information ("File already in session: " ^ fn)))
(* ------------ init server ------------ *)
......@@ -954,13 +955,6 @@ end
let ses,use_shapes = Session_itp.load_session f in
Debug.dprintf debug "creating controller@.";
let c = create_controller config env ses in
(* let task_driver = task_driver config env in*)
server_data := Some
{ (* task_driver = task_driver; *)
cont = c;
send_source = send_source;
};
let d = get_server_data () in
let shortcuts =
Mstr.fold
(fun s p acc -> Whyconf.Mprover.add p s acc)
......@@ -989,9 +983,13 @@ end
Hstr.fold (fun c _ acc -> c :: acc) commands_table []
}
in
Debug.dprintf debug "sending initialization infos@.";
P.notify (Initialized infos);
server_data := Some
{ cont = c;
send_source = send_source;
global_infos = infos;
};
Debug.dprintf debug "reloading source files@.";
let d = get_server_data () in
let x = reload_files d.cont ~use_shapes in
reset_and_send_the_whole_tree ();
(* After initial sending, we don't check anymore that there is a need to
......@@ -1276,7 +1274,8 @@ end
let request_is_valid r =
match r with
| Save_req | Reload_req | Unfocus_req | Get_file_contents _ | Save_file_req _
| Interrupt_req | Add_file_req _ | Set_config_param _ | Exit_req -> true
| Interrupt_req | Add_file_req _ | Set_config_param _ | Exit_req
| Get_global_infos -> true
| Get_first_unproven_node ni ->
Hint.mem model_any ni
| Focus_req nid ->
......@@ -1313,7 +1312,11 @@ end
end
else
try (
match r with
match r with
| Get_global_infos ->
let d= get_server_data () in
Debug.dprintf debug "sending initialization infos@.";
P.notify (Initialized d.global_infos)
| Save_req -> save_session ()
| Reload_req -> reload_session ()
| Get_first_unproven_node ni ->
......@@ -1361,7 +1364,7 @@ end
| Replay valid_only -> replay ~valid_only snid
| Clean -> clean snid
| Mark_Obsolete -> mark_obsolete snid
| Help_message s -> P.notify (Message (Help s))
| Help_message s -> P.notify (Message (Information s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
P.notify (Message (Information ("Unknown command: "^s)))
......
......@@ -157,6 +157,7 @@ let convert_request_constructor (r: ide_request) =
| Reload_req -> String "Reload_req"
| Exit_req -> String "Exit_req"
| Interrupt_req -> String "Interrupt_req"
| Get_global_infos -> String "Get_global_infos"
let print_request_to_json (r: ide_request): Json_base.json =
let cc = convert_request_constructor in
......@@ -194,16 +195,13 @@ let print_request_to_json (r: ide_request): Json_base.json =
| Focus_req id ->
convert_record ["ide_request", cc r;
"node_ID", Int id]
| Unfocus_req ->
convert_record ["ide_request", cc r]
| Save_req ->
convert_record ["ide_request", cc r]
| Reload_req ->
convert_record ["ide_request", cc r]
| Exit_req ->
convert_record ["ide_request", cc r]
| Interrupt_req ->
convert_record ["ide_request", cc r])
| Unfocus_req
| Save_req
| Reload_req
| Exit_req
| Interrupt_req
| Get_global_infos ->
convert_record ["ide_request", cc r])
let convert_constructor_message (m: message_notification) =
match m with
......@@ -213,7 +211,6 @@ let convert_constructor_message (m: message_notification) =
| Replay_Info _ -> String "Replay_Info"
| Query_Info _ -> String "Query_Info"
| Query_Error _ -> String "Query_Error"
| Help _ -> String "Help"
| Information _ -> String "Information"
| Task_Monitor _ -> String "Task_Monitor"
| Parse_Or_Type_Error _ -> String "Parse_Or_Type_Error"
......@@ -258,9 +255,6 @@ let convert_message (m: message_notification) =
convert_record ["mess_notif", cc m;
"node_ID", Int nid;
"qerror", String s]
| Help s ->
convert_record ["mess_notif", cc m;
"qhelp", String s]
| Information s ->
convert_record ["mess_notif", cc m;
"information", String s]
......@@ -620,10 +614,6 @@ let parse_message constr j =
let s = get_string (get_field j "qerror") in
Query_Error (nid, s)
| "Help" ->
let s = get_string (get_field j "qhelp") in
Help s
| "Information" ->
let s = get_string (get_field j "information") in
Information s
......
......@@ -112,11 +112,13 @@ let treat_message_notification fmt msg = match msg with
| Query_Info (_id, s) -> fprintf fmt "%s@." s
| Query_Error (_id, s) -> fprintf fmt "%s@." s
| File_Saved s -> fprintf fmt "%s@." s
(*
| Help s -> fprintf fmt "%s@. Additionally for shell:\n\
goto n -> focuse on n\n\
ng -> next node\n\
g -> print the current task\n\
p -> print the session@." s
*)
| Information s -> fprintf fmt "%s@." s
| Task_Monitor (_t, _s, _r) -> () (* TODO do we want to print something for this? *)
| Parse_Or_Type_Error (_, _, s) -> fprintf fmt "%s@." s
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment