X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=de78194f0254f0592642d8b90ad40c3ccd183fde;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=6a03e3538652c379234d31e76197627ab8d51a1a;hpb=f811e07f481b135bd7c621c2d10a268dc35d599b;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 6a03e3538..de78194f0 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -145,7 +145,11 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
         try List.assoc "depth" a
         with Not_found -> ""
       in
-      let trace = "/"^(if int_of_string depth > 1 then depth else "")^" by " in
+      let width = 
+        try List.assoc "width" a
+        with Not_found -> ""
+      in
+      let trace = "/"^(if int_of_string depth > 1 then depth ^ " width=" ^ width else "")^" by " in
       let thms = 
         match !trace_ref with
         | [] -> ""
@@ -776,7 +780,10 @@ object (self)
       buffer#move_mark mark mark_position;
       source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
      end;
-    while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+    let time0 = Unix.gettimeofday () in
+    GtkThread.sync (fun () -> while Glib.Main.pending () do ignore(Glib.Main.iteration false); done) ();
+    let time1 = Unix.gettimeofday () in
+    HLog.debug ("... refresh done in " ^ string_of_float (time1 -. time0) ^ "s")
 
   method clean_dirty_lock =
     let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in