X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=ee09258e07bad2f80fd62af05a1a1810c5e26267;hb=f28480139ee72d092a9405619c3bdf6d4ff155ee;hp=7150c6f775cb57fecf8340070db8d3c659c8d424;hpb=a229a988dceead9ffe3ea593fcf98e68a16582cf;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 7150c6f77..ee09258e0 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 open GrafiteTypes
@@ -117,15 +119,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 () =
@@ -134,7 +141,9 @@ let go () =
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
   LibraryDb.create_owner_environment ();
   CicEnvironment.set_trust (* environment trust *)
-    (let trust = Helm_registry.get_bool "matita.environment_trust" in
+    (let trust =
+      Helm_registry.get_opt_default Helm_registry.get_bool
+        ~default:true "matita.environment_trust" in
      fun _ -> trust);
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
@@ -234,6 +243,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);