- predefined_virtuals: nwe characters

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

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 7bce06884ae091378d6d228811e2c1b474fae28c..144250fb9b55e634312523693f15f1c309d8add5 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -63,16 +63,39 @@ let clean_exit baseuri exn =
   raise (FailureCompiling (baseuri,exn))
 ;;
 
+let cut prefix s = 
+  let lenp = String.length prefix in
+  let lens = String.length s in
+  assert (lens > lenp);
+  assert (String.sub s 0 lenp = prefix);
+  String.sub s lenp (lens-lenp)
+;;
+
+let print_string = 
+ let indent = ref 0 in
+ let print_string ~right_justify s =
+  let ss =
+   match right_justify with
+      None -> ""
+    | Some (ss,len_ss) ->
+       let i = 80 - !indent - len_ss - String.length s in
+       if i > 0 then String.make i ' ' ^ ss else ss
+  in
+   assert (!indent >=0);
+   print_string (String.make !indent ' ' ^ s ^ ss) in
+ fun enter ?right_justify s ->
+  if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)
+;;
 
-let pp_times fname rc big_bang big_bang_u big_bang_s = 
+let pp_times ss fname rc big_bang big_bang_u big_bang_s = 
   if not (Helm_registry.get_bool "matita.verbose") then
     let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
     let r = Unix.gettimeofday () -. big_bang in
     let u = u -. big_bang_u in
     let s = s -. big_bang_s in
     let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
-    let rc,rcascii = 
-      if rc then "\e[0;32mOK\e[0m","Ok" else "\e[0;31mFAIL\e[0m","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
@@ -83,20 +106,12 @@ let pp_times fname rc big_bang big_bang_u big_bang_s =
       in
       Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
     in
-    let s = Printf.sprintf "%-4s %s %s" rc times extra in
-    print_endline s;
+    let s = Printf.sprintf "%-14s %s %s\n" rc times extra in
+    print_string false ~right_justify:(s,31) ss;
     flush stdout;
     HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
 ;;
 
-let cut prefix s = 
-  let lenp = String.length prefix in
-  let lens = String.length s in
-  assert (lens > lenp);
-  assert (String.sub s 0 lenp = prefix);
-  String.sub s lenp (lens-lenp)
-;;
-
 let activate_extraction baseuri fname =
   ()
   (* MATITA 1.0
@@ -216,7 +231,8 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
         let str =
          match ast with
             (GrafiteAst.Executable
-              (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,_)))) ->
+              (_,GrafiteAst.NCommand
+                (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
               GrafiteParser.parsable_statement status
                (GrafiteParser.strm_of_parsable str)
           | _ -> str
@@ -244,6 +260,11 @@ and compile ~compiling ~asserted ~include_paths fname =
     Unix.times () 
   in
   let time = Unix.time () in
+  let cc = 
+   let rex = Str.regexp ".*opt$" in
+   if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
+   else "matitac" in
+  let s = Printf.sprintf "%s %s" cc (cut (root^"/") fname) in
   try
     (* cleanup of previously compiled objects *)
     if (not (Http_getter_storage.is_empty ~local:true baseuri))
@@ -254,13 +275,7 @@ and compile ~compiling ~asserted ~include_paths fname =
     end;
     HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
     if not (Helm_registry.get_bool "matita.verbose") then
-      (let cc = 
-        let rex = Str.regexp ".*opt$" in
-        if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
-        else "matitac" 
-      in
-      let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
-      print_string s; flush stdout);
+     (print_string true (s ^ "\n"); flush stdout);
     (* we dalay this error check until we print 'matitac file ' *)
     assert (Http_getter_storage.is_empty ~local:true baseuri);
     (* create dir for XML files *)
@@ -296,7 +311,7 @@ and compile ~compiling ~asserted ~include_paths fname =
      in
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
-     pp_times fname true big_bang big_bang_u big_bang_s;
+     pp_times s fname true big_bang big_bang_u big_bang_s;
      asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
@@ -308,7 +323,7 @@ and compile ~compiling ~asserted ~include_paths fname =
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
        LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
  *       *)
-      pp_times fname false big_bang big_bang_u big_bang_s;
+      pp_times s fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
 and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =