X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaAutoGui.ml;h=588dc5fecd09363f7de821a80eecb261ed083624;hb=7e035682056388e730f03e214774d093e06ef650;hp=06b6b5f1e9e8696aaef3f78d976f7d1acf3ed8ca;hpb=57e3de08d963ff08d671c639c0e9990368b86f20;p=helm.git
diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index 06b6b5f1e..588dc5fec 100644
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -25,33 +25,49 @@
*)
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 = [];;
let start = ref 0;;
let len = ref 10;;
-let pp c t =
- (*
+
+let font_size = ref
+ (Helm_registry.get_opt_default Helm_registry.int
+ ~default:BuildTimeConf.default_font_size "matita.font_size")
+;;
+
+let set_font_size n = font_size := n;;
+
+let pp ?(size=(!font_size)) c t =
let t =
ProofEngineReduction.replace
~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
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:"?$1" txt_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
;;
-let pp_candidate context x = pp 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 (Lazy.force x) CicUniv.oblivion_ugraph
+ in
+ pp ~size:0 context ty
+ with CicUtil.Meta_not_found _ -> pp ~size:0 context (Lazy.force x)
+;;
let sublist start len l =
let rec aux pos len = function
@@ -68,16 +84,15 @@ let sublist start len l =
let cell_of_candidate height context ?(active=false) g id c =
let tooltip = GData.tooltips () in (* should be only one isn't it? *)
- let button =
- GButton.button
- ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*))
- ()
- in
+ let button = GButton.button () in
+ let l = GMisc.label ~markup:(pp_candidate context c) () in
+ button#add l#coerce;
button#misc#set_size_request ~height ();
if active then
button#misc#set_sensitive false;
let text =
- "Follow computation of "^pp_candidate context c^" on "^pp_goal context g
+ "Follow/Prune computation of\n"^pp_candidate_tip context c^": "^
+ pp_candidate_type context c
in
tooltip#set_tip ~text (button :> GObj.widget);
ignore(button#connect#clicked
@@ -97,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
@@ -145,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
@@ -158,13 +173,17 @@ let fill_win (win : MatitaGeneratedGui.autoWin) cb =
begin
old_displayed_status := displayed_status;
old_size := win_size;
+(*
win#labelLAST#set_text
(String.concat ";" (List.map (pp_candidate ctx) last_moves));
+*)
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); ()
;;
@@ -190,7 +209,16 @@ let auto_dialog elems =
Auto.step ();
win#toplevel#destroy ();
GMain.Main.quit ()));
- let redraw_callback _ = fill_win win elems;true in
+ 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
(fun _ ->