IDE: warnings displayed in one shot

src/ide/gmain.ml

@@ -798,24 +798,33 @@ let info_window ?(callback=(fun () -> ())) mt s =
 let file_info = GMisc.label ~text:""
   ~packing:(right_hb#pack ~fill:true) ()
 
-let warning_window ?loc msg =
-  begin
-    match loc with
-    | None ->
-      Format.fprintf Format.str_formatter "%s" msg
-    | Some l ->
-      (* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
-      Format.fprintf Format.str_formatter "%a: %s"
-        Loc.gen_report_position l msg
-  end;
-  let msg =
-    Format.flush_str_formatter ()
-  in
-  file_info#set_text msg;
-  info_window `WARNING msg
+let warnings = Queue.create ()
 
-let () = Warning.set_hook warning_window
+let record_warning ?loc msg = Queue.push (loc,msg) warnings
 
+let () = Warning.set_hook record_warning
+
+
+let display_warnings () =
+  if Queue.is_empty warnings then () else
+    begin
+      Queue.iter 
+        (fun (loc,msg) ->
+          match loc with
+            | None ->
+              Format.fprintf Format.str_formatter "%s@\n" msg
+            | Some l ->
+            (* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
+              Format.fprintf Format.str_formatter "%a: %s@\n"
+                Loc.gen_report_position l msg)
+        warnings;
+      Queue.clear warnings;
+      let msg =
+        Format.flush_str_formatter ()
+      in
+  (* file_info#set_text msg; *)
+      info_window `WARNING msg
+    end  
 
 (* check if provers are present *)
 let () =
@@ -867,7 +876,8 @@ let () =
         else
           try
             Debug.dprintf debug "[Info] adding file %s in database@." fn;
-            ignore (M.add_file (env_session()) ?format:!opt_parser fn)
+            ignore (M.add_file (env_session()) ?format:!opt_parser fn);
+            display_warnings ()
           with e ->
             eprintf "@[Error while reading file@ '%s':@ %a@.@]" fn
               Exn_printer.exn_printer e;
@@ -1122,7 +1132,8 @@ let select_file () =
               let f = Sysutil.relativize_filename project_dir f in
               Debug.dprintf debug "Adding file '%s'@." f;
               try
-                ignore (M.add_file (env_session()) f)
+                ignore (M.add_file (env_session()) f);
+                display_warnings ()
               with e ->
                 fprintf str_formatter
                   "@[Error while reading file@ '%s':@ %a@]" f

src/session/termcode.ml

@@ -281,7 +281,7 @@ module type S = sig
   val name       : t -> Ident.ident
 end
 
-
+(*
 module type Sold = sig
   type t
   val checksum : t -> string
@@ -289,7 +289,9 @@ module type Sold = sig
   val id       : t -> Ident.ident
 (* .goal_name *)
 end
+*)
 
+(*
 module type Snew = sig
   type t
   val checksum : t -> string
@@ -311,6 +313,7 @@ module type Snew = sig
 
 
 end
+*)
 
 
 (*************************************************************)

src/transform/eliminate_definition.ml

@@ -195,7 +195,7 @@ type bisect_step =
 
 type rem = { rem_pr : Spr.t; rem_ls : Sls.t; rem_ts : Sts.t }
 
-let print_rem fmt rem = Format.fprintf fmt
+let _print_rem fmt rem = Format.fprintf fmt
   "@[rem_pr:@[%a@]@\nrem_ls:@[%a@]@\nrem_ts:@[%a@]@\n"
   (Pp.print_iter1 Spr.iter Pp.comma Pretty.print_pr) rem.rem_pr
   (Pp.print_iter1 Sls.iter Pp.comma Pretty.print_ls) rem.rem_ls
@@ -228,7 +228,7 @@ let add_rem rem decl =
   | Dind (_,l) -> List.fold_left (fun rem (ls,_) -> remove_ls rem ls) rem l
   | Dprop (_,pr,_) -> remove_pr rem pr
 
-let union_rem rem1 rem2 =
+let _union_rem rem1 rem2 =
   { rem_ts = Sts.union rem1.rem_ts rem2.rem_ts;
     rem_ls = Sls.union rem1.rem_ls rem2.rem_ls;
     rem_pr = Spr.union rem1.rem_pr rem2.rem_pr;

tests/test-claude.why

@@ -219,4 +219,12 @@ inductive p (x:int) =
   | C2 : let x=0 in p x
 end
 
+theory TestWarnings
 
+  type t
+
+  lemma L1 : forall x:t. true
+
+  lemma L2 : exists x:t. x=x -> false
+
+end