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)
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