1. Macros are now handled using an execption that is caught by matitacLib

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

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 7150c6f775cb57fecf8340070db8d3c659c8d424..eeac8d6c92fba2c44a51280e6a575f05b6d7d74d 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -117,15 +117,20 @@ let rec interactive_loop () =
         "matita.includes"))
   with 
   | GrafiteEngine.Drop -> pp_ocaml_mode ()
+  | GrafiteEngine.Macro (floc,_) ->
+     let x, y = HExtlib.loc_of_floc floc in
+      HLog.error
+       (sprintf "A macro has been found in a script at %d-%d" x y);
+      interactive_loop ()
   | Sys.Break -> HLog.error "user break!"; interactive_loop ()
   | GrafiteTypes.Command_error _ -> interactive_loop ()
   | End_of_file ->
      print_newline ();
      clean_exit (Some 0)
   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
-     let (x, y) = HExtlib.loc_of_floc floc in
-     HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
-     interactive_loop ()
+     let x, y = HExtlib.loc_of_floc floc in
+      HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+      interactive_loop ()
   | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
 
 let go () =
@@ -234,6 +239,14 @@ let main ~mode =
         clean_exit (Some 1)
       else 
         pp_ocaml_mode ()
+  | GrafiteEngine.Macro (floc,_) ->
+     let x, y = HExtlib.loc_of_floc floc in
+      HLog.error
+       (sprintf "A macro has been found in a script at %d-%d" x y);
+      if mode = `COMPILER then 
+        clean_exit (Some 1)
+      else 
+        pp_ocaml_mode ()
   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
      let (x, y) = HExtlib.loc_of_floc floc in
      HLog.error (sprintf "Parse error at %d-%d: %s" x y err);