X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaAutoGui.ml;h=588dc5fecd09363f7de821a80eecb261ed083624;hb=d8c297847d28b8648c1b3728d5763112ae6472ad;hp=a4d7ce85f1cc4d567123528f18231b7e7d36353d;hpb=5f3d564c7d5aa321a1a184ece75a5e1802a4fa2a;p=helm.git

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index a4d7ce85f..588dc5fec 100644
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -25,9 +25,9 @@
  *)
 
 type status = 
-  Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * 
+  Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * 
   (int * Cic.term * int) list *
-  Cic.term list
+  Cic.term Lazy.t list
 let fake_goal = Cic.Implicit None;;
 let fake_candidates = [];;
 
@@ -49,22 +49,24 @@ 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 "") ^
-    ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
-      max_int [] c t^(if size > 0 then "</span>" else "")
+  (MatitaGtkMisc.escape_pango_markup
+    (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
+      max_int [] c t))^
+  (if size > 0 then "</span>" else "")
 ;;
 let pp_goal context x = 
   if x == fake_goal then "" else pp context x
 ;;
-let pp_candidate context x = pp context x
-let pp_candidate_tip context x = pp ~size:0 context x
+let pp_candidate context x = pp context (Lazy.force x)
+let pp_candidate_tip context x = pp ~size:0 context (Lazy.force x)
 let pp_candidate_type context x = 
   try 
     let ty, _ = 
       CicTypeChecker.type_of_aux' [] ~subst:[] 
-       context x CicUniv.oblivion_ugraph
+       context (Lazy.force x) CicUniv.oblivion_ugraph
     in
       pp ~size:0 context ty
-  with CicUtil.Meta_not_found _ ->  pp ~size:0 context x
+  with CicUtil.Meta_not_found _ ->  pp ~size:0 context (Lazy.force x)
 ;;
 
 let sublist start len l = 
@@ -110,7 +112,7 @@ let cell_of_candidate height context ?(active=false) g id c =
 let cell_of_goal height win_width context goal = 
   GMisc.label 
     ~markup:(pp_goal context goal) ~xalign:0.0 
-    ~width:(min (win_width * 60 / 100) 500) 
+    ~width:(min (win_width * 30 / 100) 500) 
     ~line_wrap:false
     ~ellipsize:`END
     ~height
@@ -158,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
@@ -178,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); ()
 ;;
@@ -211,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 _ ->