let len = ref 10;;
let pp c t =
- (*
let t =
ProofEngineReduction.replace
~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
in
ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
max_int [] c t
- *)
- let names = List.map (function None -> None | Some (x,_) -> Some x) c in
- let txt_t = CicPp.pp t names in
- Pcre.replace ~pat:"\\?(\\d+)\\[[^]]*\\]" ~templ:"?<sub>$1</sub>" txt_t
;;
let pp_goal context x =
if x == fake_goal then "" else pp context x
Auto.step ();
win#toplevel#destroy ();
GMain.Main.quit ()));
+ ignore(win#toplevel#event#connect#delete
+ (fun _ ->
+ Auto.pause false;
+ Auto.step ();
+ win#toplevel#destroy ();
+ GMain.Main.quit ();true));
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