New formulation of finite_enumerable_SemiGroups to allow the \iota notation

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

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 73a4d668f7b381dcc8630a9c434743e0a10cae7f..3567c33f0a14575c683a75384381cab7c82dca61 100644 (file)
--- 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,14 +187,12 @@ 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
     let tm = Unix.gmtime elapsed in
-    let sec = 
-      if tm.Unix.tm_sec > 0 then (string_of_int tm.Unix.tm_sec ^ "''") else "" 
-    in
+    let sec = string_of_int tm.Unix.tm_sec ^ "''" in
     let min = 
       if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min ^ "' ") else "" 
     in
@@ -231,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);