X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaEngine.ml;h=144250fb9b55e634312523693f15f1c309d8add5;hb=d32efcc40e6de8a337e61864dab00305ba30b334;hp=2d0a03b20da91e058f0f522cc7e0ad8fcadf1e65;hpb=6a2985ee4de00c81115d0c008baa6aba05bca6bc;p=helm.git

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 2d0a03b20..144250fb9 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -71,15 +71,17 @@ let cut prefix s =
   String.sub s lenp (lens-lenp)
 ;;
 
-let print_string =
+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) ->
-       String.make (80 - !indent - len_ss - String.length s) ' ' ^ 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)
@@ -292,7 +294,7 @@ and compile ~compiling ~asserted ~include_paths fname =
       if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
       else pp_ast_statement
     in
-    let asserted, times, status =
+    let asserted, status =
      eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin