X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=872dccace16b0b25d2f8ee1ae6fa6a2ae3df1266;hb=7c123bfb1568f90f37cd667332fbf60d4423b983;hp=a10594ab2a68ebf3f0f909d4140ce2ae165c86c5;hpb=595d77eece3202a799e786ac5996b6b1e25fac6e;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index a10594ab2..872dccace 100644
--- 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 ()
@@ -140,6 +140,7 @@ let main ~mode =
   in
   if Helm_registry.get_bool "matita.quiet" then
     MatitaLog.set_log_callback newcb;
+  let matita_debug = Helm_registry.get_bool "matita.debug" in
   try
     let time = Unix.time () in
     if Helm_registry.get_bool "matita.quiet" then
@@ -181,7 +182,7 @@ let main ~mode =
      end
     else
      begin
-       let moo_fname = MatitaMisc.obj_file_of_script fname in
+       let moo_fname = MatitacleanLib.obj_file_of_script fname in
        MatitaMoo.save_moo moo_fname moo_content_rev;
        MatitaLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
@@ -199,15 +200,15 @@ 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)
      else
        pp_ocaml_mode ()
   | exn ->
-      if Helm_registry.get_bool "matita.debug" then raise exn;
+      if matita_debug then raise exn;
       if mode = `COMPILER then 
         clean_exit (Some 3)
       else