]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitaAutoGui.ml
Concrete spaces do form a category, after all :-)
[helm.git] / helm / software / matita / matitaAutoGui.ml
index 23905905bf73b11f16aa1a2a05e7aa40572e399c..d01cac5d14a698166a25637fcd379f0aadc4c9f7 100644 (file)
@@ -49,10 +49,9 @@ let pp ?(size=(!font_size)) c t =
       ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
   in
   (if size > 0 then "<span font_desc=\""^string_of_int size^"\">" else "") ^
-  (Pcre.replace ~pat:"<" ~templ:"&lt;"
-   (Pcre.replace ~pat:">" ~templ:"&gt;"
+  (MatitaGtkMisc.escape_pango_markup
     (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
-      max_int [] c t)))^
+      max_int [] c t))^
   (if size > 0 then "</span>" else "")
 ;;
 let pp_goal context x = 
@@ -161,7 +160,7 @@ let old_displayed_status = ref [];;
 let old_size = ref 0;;
 
 let fill_win (win : MatitaGeneratedGui.autoWin) cb =
-  let init = Unix.gettimeofday () in
+(*   let init = Unix.gettimeofday () in *)
     try 
       let (status : status) = cb () in
       let win_size = win#toplevel#misc#allocation.Gtk.width in
@@ -181,8 +180,10 @@ let fill_win (win : MatitaGeneratedGui.autoWin) cb =
           List.iter win#table#remove win#table#children;
           let height = win#viewportAREA#misc#allocation.Gtk.height in
           elems_to_rows height ctx win_size win#table displayed_status;
+(*
           Printf.eprintf 
             "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -.  init);
+*)
         end
     with exn -> prerr_endline (Printexc.to_string exn); ()
 ;;
@@ -214,7 +215,10 @@ let auto_dialog elems =
       Auto.step ();
       win#toplevel#destroy ();
       GMain.Main.quit ();true));
-  let redraw_callback _ = fill_win win elems;true in
+  let redraw_callback _ = 
+    fill_win win elems;
+    true 
+  in
   let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
   ignore(win#buttonPAUSE#connect#clicked 
     (fun _ ->