Commit 1623cb5f authored by MARCHE Claude's avatar MARCHE Claude

attempt to show again warnings in IDE (issue #32)

need some improvement before clsing the issue
parent 144d6ee3
......@@ -361,8 +361,15 @@ let update_label_saved (label: GMisc.label) =
(**********************)
let initialization_complete = ref false
let warnings = Queue.create ()
let record_warning ?loc msg =
Format.eprintf "%awarning: %s@."
(Pp.print_option Loc.report_position) loc msg;
Queue.push (loc,msg) warnings
let () =
Warning.set_hook record_warning;
let dir =
try
Server_utils.get_session_dir ~allow_mkdir:true files
......@@ -997,12 +1004,47 @@ let print_message ~kind ~notif_kind fmt =
add_to_log notif_kind s;
if kind>0 then
begin
message_zone#buffer#set_text s;
message_zone#buffer#insert (s ^ "\n");
messages_notebook#goto_page error_page
end)
str_formatter
fmt
let display_warnings () =
if Queue.is_empty warnings then () else
begin
let nwarn = ref 0 in
begin try
Queue.iter
(fun (loc,msg) ->
if !nwarn = 4 then
begin
Format.fprintf Format.str_formatter "[%d more warnings. See stderr for details]@\n" (Queue.length warnings - !nwarn);
raise Exit
end
else
begin
incr nwarn;
match loc with
| None ->
Format.fprintf Format.str_formatter "%s@\n@\n" msg
| Some l ->
(* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
Format.fprintf Format.str_formatter "%a: %s@\n@\n"
Loc.gen_report_position l msg
end) warnings;
with Exit -> ();
end;
Queue.clear warnings;
let msg =
Format.flush_str_formatter ()
in
print_message ~kind:1 ~notif_kind:"warning" "%s" msg
end
let () =
Warning.set_hook (fun ?loc s -> record_warning ?loc s; display_warnings ())
(**** Monitor *****)
......@@ -2194,6 +2236,7 @@ let treat_notification n =
| Initialized g_info ->
initialization_complete := true;
main_window#show ();
display_warnings ();
init_completion g_info.provers g_info.transformations g_info.strategies g_info.commands;
| Saved ->
session_needs_saving := false;
......
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