in case of syntax error on reload, do not exit abruptly but displays a message...

in case of syntax error on reload, do not exit abruptly but displays a message and scroll to loc of the error

Makefile.in

@@ -445,8 +445,8 @@ install_local: bin/why3config
 
 ifeq (@enable_ide@,yes)
 
-IDE_FILES = xml session gconfig db gmain
-# IDE_FILES = xml session gconfig newmain
+# IDE_FILES = xml session gconfig db gmain
+IDE_FILES = xml session gconfig newmain
 
 IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
 

src/ide/newmain.ml

@@ -508,13 +508,9 @@ let () =
     M.maximum_running_proofs := gconfig.max_running_processes;
     eprintf " done@."
   with e ->
-    eprintf "Error while opening session with database '%s'@." project_dir;
-    eprintf "Aborting...@.";
-    raise e
-
-
-
-
+    eprintf "@[Error while opening session:@ %a@.@]" 
+      Exn_printer.exn_printer e;
+    exit 1
 
 
 let info_window ?(callback=(fun () -> ())) mt s =
@@ -1051,18 +1047,20 @@ let color_loc (v:GSourceView2.source_view) l b e =
   let stop = start#forward_chars (e-b) in
   buf#apply_tag ~start ~stop orange_bg
 
+let scroll_to_loc loc =
+  let (f,l,b,e) = Loc.get loc in
+  if f <> !current_file then
+    begin
+      source_view#source_buffer#set_text (source_text f);
+      set_current_file f;
+    end;
+  move_to_line source_view (l-1);
+  erase_color_loc source_view;
+  color_loc source_view l b e
+
 let scroll_to_id id =
   match id.Ident.id_loc with
-    | Some loc ->
-        let (f,l,b,e) = Loc.get loc in
-        if f <> !current_file then
-          begin
-            source_view#source_buffer#set_text (source_text f);
-            set_current_file f;
-          end;
-        move_to_line source_view (l-1);
-        erase_color_loc source_view;
-        color_loc source_view l b e
+    | Some loc -> scroll_to_loc loc
     | None ->
         source_view#source_buffer#set_text
           "Non-localized ident (no position available)\n";
@@ -1190,6 +1188,24 @@ let () =
     b#connect#pressed ~callback:replay_obsolete_proofs
   in ()
 
+let reload () =
+  try
+    M.reload_all gconfig.provers;
+    current_file := ""
+  with
+    | Loc.Located(loc,Parsing.Parse_error) -> 
+	fprintf str_formatter
+	  "@[Syntax error:@ %a@]" Loc.gen_report_position loc;
+	let msg = flush_str_formatter () in
+	scroll_to_loc loc;
+	info_window `ERROR msg	
+    | e ->
+	fprintf str_formatter
+	  "@[Error while reading file:@ %a@]" Exn_printer.exn_printer e;
+	let msg = flush_str_formatter () in
+	info_window `ERROR msg
+
+ 
 let () =
   let b = GButton.button ~packing:tools_box#add ~label:"Reload" () in
   b#misc#set_tooltip_markup "Reloads the files";
@@ -1197,9 +1213,7 @@ let () =
   let i = GMisc.image ~pixbuf:(!image_reload) () in
   let () = b#set_image i#coerce in
   let (_ : GtkSignal.id) =
-    b#connect#pressed ~callback:(fun () -> 
-                                   current_file := "";
-                                   M.reload_all gconfig.provers)
+    b#connect#pressed ~callback:reload
   in ()
 
 (*************)

src/ide/session.ml

@@ -862,9 +862,6 @@ let reload_root_goal ~provers mth tname old_goals t : goal =
   let id = (Task.task_goal t).Decl.pr_name in
   let gname = id.Ident.id_string in
   let sum = task_checksum t in
-(*
-  let goal = raw_add_goal (Parent_theory mth) gname expl sum (Some t) in
-*)
   let old_goal, goal_obsolete =
     try
       let old_goal = Util.Mstr.find gname old_goals in
@@ -903,7 +900,8 @@ let reload_theory ~provers mfile old_theories (_,tname,th) =
 
 
 (* reloads a file *)
-let reload_file ~provers mf =
+let reload_file ~provers mf theories =
+(*
   eprintf "[Reload] file '%s'@." mf.file_name;
   let theories = 
     try
@@ -914,6 +912,7 @@ let reload_file ~provers mf =
       (* TODO: do something clever than that! *)
       exit 1
   in
+*)
   let new_mf = raw_add_file mf.file_name in
   let old_theories = List.fold_left
     (fun acc t -> Util.Mstr.add t.theory_name t acc)
@@ -931,9 +930,15 @@ let reload_file ~provers mf =
 (* reloads all files *)
 let reload_all provers =
   let files = !all_files in
+  let all_theories =
+    List.map (fun mf -> 
+		eprintf "[Reload] file '%s'@." mf.file_name;
+		(mf,read_file mf.file_name)) 
+      files
+  in
   all_files := [];
   O.reset ();
-  List.iter (reload_file ~provers) files
+  List.iter (fun (mf,ths) -> reload_file ~provers mf ths) all_theories
 
 (****************************)
 (*     session opening      *)

src/ide/session.mli

@@ -223,8 +223,9 @@ module Make(O: OBSERVER) : sig
 
   val reload_all: prover_data Util.Mstr.t -> unit
     (** reloads all the files 
-        If for a given file, the parsing or typing fails, then
-        then old version is kept, but marked obsolete
+        If for one of the file, the parsing or typing fails, then
+        the complete old session state is kept, and an exception
+	is raised
     *)
 (*
 TODO

tests/test-claude.why

@@ -16,7 +16,7 @@ theory TestInt
 
    use import int.Int
 
-   goal Test1: 2+2 = 5
+   goal Test1: 2+2 = 
 
    goal Test2: forall x:int. x*x >= 0