Commit b28e2653 authored by MARCHE Claude's avatar MARCHE Claude

fix blocking issue #48

improve the startup sequence at the same time

in particular, when source editing is disabled and there is a
syntax or typing error, the GTK window does not 'blink' briefly before
printing the error in the console
parent 7b1261df
......@@ -55,6 +55,7 @@ let debug_json = Debug.register_flag "json_proto"
(* server protocol *)
(*******************)
module Protocol_why3ide = struct
let debug_proto = Debug.register_flag "ide_proto"
......@@ -1471,6 +1472,8 @@ 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) ->
......@@ -1506,13 +1509,16 @@ let treat_message_notification msg = match msg with
| 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 ->
print_message ~kind:0 ~notif_kind:"Open_File_Error" "%s" s
| Parse_Or_Type_Error (loc, rel_loc, s) ->
if gconfig.allow_source_editing then
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;
......@@ -2136,5 +2142,4 @@ let () =
main_window#add_accel_group accel_group;
main_window#set_icon (Some !Gconfig.why_icon);
message_zone#buffer#set_text "Welcome to Why3 IDE\ntype 'help' for help";
main_window#show ();
GMain.main ()
......@@ -624,15 +624,6 @@ end
with Invalid_argument s ->
P.notify (Message (Error s))
(* Send all source files from the controller session to the IDE *)
let load_files_session () =
let d = get_server_data () in
let s = d.cont.controller_session in
let files = Session_itp.get_files s in
Stdlib.Hstr.iter (fun _ f ->
Debug.dprintf debug "load_files_session: loading '%s'@." (file_name f);
read_and_send (file_name f)) files
let relativize_location s loc =
let f, l, b, e = Loc.get loc in
let f = Sysutil.relativize_filename (Session_itp.get_dir s) f in
......@@ -998,7 +989,6 @@ end
in
Debug.dprintf debug "sending initialization infos@.";
P.notify (Initialized infos);
load_files_session ();
Debug.dprintf debug "reloading source files@.";
let x = reload_files d.cont ~use_shapes in
reset_and_send_the_whole_tree ();
......@@ -1007,7 +997,7 @@ end
get_focused_label := None;
match x with
| [] ->
P.notify (Message (Information "Session initialized succesfully"))
P.notify (Message (Information "Session initialized successfully"))
| l ->
List.iter
(function (loc,rel_loc,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