*)
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 = [];;
~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:"<"
- (Pcre.replace ~pat:">" ~templ:">"
+ (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 =
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 =
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 _ ->