X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=3567c33f0a14575c683a75384381cab7c82dca61;hb=a8d3be41b60e0720b32750243c1999c5083f4299;hp=47447e49eb77268cc2bfc13dfa5fbcea1fd927bf;hpb=86671ef183faa0ff4731d06d69349689fa4c084c;p=helm.git

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 47447e49e..3567c33f0 100644
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -23,10 +23,14 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 open GrafiteTypes
 
+exception AttemptToInsertAnAlias
+
 let pp_ast_statement =
   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
     ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
@@ -60,8 +64,11 @@ let run_script is eval_function  =
         HLog.debug ("Executing: ``" ^ stm ^ "''"))
   in
   try
-   let lexicon_status'', grafite_status'' =
-    eval_function lexicon_status' grafite_status' is cb
+   let grafite_status'', lexicon_status'' =
+    match eval_function lexicon_status' grafite_status' is cb with
+       [] -> assert false
+     | (s,None)::_ -> s
+     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
    in
     lexicon_status := Some lexicon_status'';
     grafite_status := Some grafite_status''
@@ -107,20 +114,25 @@ let rec interactive_loop () =
   let str = Ulexing.from_utf8_channel stdin in
   try
     run_script str 
-      (MatitaEngine.eval_from_stream ~prompt:true
+      (MatitaEngine.eval_from_stream ~first_statement_only:false ~prompt:true
       ~include_paths:(Helm_registry.get_list Helm_registry.string
         "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 () =
@@ -175,7 +187,7 @@ let main ~mode =
      Helm_registry.get_list Helm_registry.string "matita.includes" in
     (try
       run_script is 
-       (MatitaEngine.eval_from_stream ~include_paths
+       (MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
          ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")))
      with End_of_file -> ());
     let elapsed = Unix.time () -. time in
@@ -229,6 +241,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);