X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaAutoGui.ml;h=d01cac5d14a698166a25637fcd379f0aadc4c9f7;hb=f75a636a0f3d548bcf485df9b51ac72ed4759c97;hp=a4d7ce85f1cc4d567123528f18231b7e7d36353d;hpb=5f3d564c7d5aa321a1a184ece75a5e1802a4fa2a;p=helm.git diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml index a4d7ce85f..d01cac5d1 100644 --- a/helm/software/matita/matitaAutoGui.ml +++ b/helm/software/matita/matitaAutoGui.ml @@ -49,8 +49,10 @@ let pp ?(size=(!font_size)) c t = ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t in (if size > 0 then "" else "") ^ - ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false - max_int [] c t^(if size > 0 then "" else "") + (MatitaGtkMisc.escape_pango_markup + (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false + max_int [] c t))^ + (if size > 0 then "" else "") ;; let pp_goal context x = if x == fake_goal then "" else pp context x @@ -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 _ ->