New implementation for localized exceptions.

[helm.git] / helm / matita / matitacLib.ml

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 8552cbf8629ba98f72086fd58c11d67512bd9d49..872dccace16b0b25d2f8ee1ae6fa6a2ae3df1266 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -61,7 +61,7 @@ let run_script is eval_function  =
   | End_of_file
   | CicNotationParser.Parse_error _ as exn -> raise exn
   | exn -> 
-      MatitaLog.error (MatitaExcPp.to_string exn);
+      MatitaLog.error (snd (MatitaExcPp.to_string exn));
       raise exn
 
 let fname () =
@@ -107,8 +107,8 @@ let rec interactive_loop () =
   | End_of_file ->
      print_newline ();
      clean_exit (Some 0)
-  | CicNotationParser.Parse_error (floc,err) ->
-     let (x, y) = CicNotationPt.loc_of_floc floc in
+  | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+     let (x, y) = HExtlib.loc_of_floc floc in
      MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
      interactive_loop ()
   | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop ()
@@ -200,8 +200,8 @@ let main ~mode =
         clean_exit (Some 1)
       else 
         pp_ocaml_mode ()
-  | CicNotationParser.Parse_error (floc,err) ->
-     let (x, y) = CicNotationPt.loc_of_floc floc in
+  | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+     let (x, y) = HExtlib.loc_of_floc floc in
      MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
      if mode = `COMPILER then
        clean_exit (Some 1)