LAMBDA-TYPES: refactored

[helm.git] / matita / matitacLib.ml

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 844d4f5d854dd723ba1f3390d6b449674596608f..52ad776e71d3a2fe91a07c5107b28dea21baa3ff 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -31,9 +31,13 @@ open GrafiteTypes
 
 exception AttemptToInsertAnAlias
 
+let out = ref ignore 
+
+let set_callback f = out := f
+
 let pp_ast_statement =
   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
-    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
+    ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term)
 
 (** {2 Initialization} *)
 
@@ -63,21 +67,21 @@ let run_script is eval_function  =
         in
         HLog.debug ("Executing: ``" ^ stm ^ "''"))
   in
+  let matita_debug = Helm_registry.get_bool "matita.debug" in
   try
-   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''
+   match eval_function lexicon_status' grafite_status' is cb with
+      [] -> raise End_of_file
+    | ((grafite_status'',lexicon_status''),None)::_ ->
+       lexicon_status := Some lexicon_status'';
+       grafite_status := Some grafite_status''
+    | (s,Some _)::_ -> raise AttemptToInsertAnAlias
   with
   | GrafiteEngine.Drop  
   | End_of_file
   | CicNotationParser.Parse_error _ as exn -> raise exn
   | exn -> 
-      HLog.error (snd (MatitaExcPp.to_string exn));
+      if not matita_debug then
+       HLog.error (snd (MatitaExcPp.to_string exn)) ;
       raise exn
 
 let fname () =
@@ -126,8 +130,14 @@ let rec interactive_loop () =
         "matita.includes"))
   with 
   | GrafiteEngine.Drop -> pp_ocaml_mode ()
-  | GrafiteEngine.Macro (floc,_) ->
-     let x, y = HExtlib.loc_of_floc floc in
+  | GrafiteEngine.Macro (floc, f) ->
+      begin match snd (f []) with 
+       | GrafiteAst.Inline (_, style, suri, prefix) ->
+         let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+         !out str
+       | _ -> ()
+      end;
+      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 ()
@@ -173,7 +183,7 @@ let pp_times fname bench_mode rc big_bang =
         else 
           "matitac" 
       in
-      let rc = if rc then "OK" else "FAIL" in
+      let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
       let times = 
         let fmt t = 
           let seconds = int_of_float t in
@@ -275,7 +285,7 @@ let main ~mode =
      end
     else
      begin
-       let baseuri =
+       let baseuri, _fullpathforfname =
         DependenciesParser.baseuri_of_script ~include_paths fname in
        let moo_fname = 
          LibraryMisc.obj_file_of_baseuri 
@@ -298,7 +308,8 @@ let main ~mode =
        exit 0
      end
   with 
-  | Sys.Break ->
+  | Sys.Break as exn ->
+     if matita_debug then raise exn;
       HLog.error "user break!";
       pp_times fname bench_mode false big_bang;
       if mode = `COMPILER then