~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 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
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
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); ()
;;
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 _ ->