added support for font scaling to autogui

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index c7b06645b45cfe4948e63303897b4633b20ba6a0..a4d7ce85f1cc4d567123528f18231b7e7d36353d 100644 (file)
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -34,19 +34,38 @@ 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
+  (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
+      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_type context x = 
+  try 
+    let ty, _ = 
+      CicTypeChecker.type_of_aux' [] ~subst:[] 
+       context x CicUniv.oblivion_ugraph
+    in
+      pp ~size:0 context ty
+  with CicUtil.Meta_not_found _ ->  pp ~size:0 context x
+;;
 
 let sublist start len l = 
   let rec aux pos len = function
@@ -63,16 +82,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 
@@ -153,8 +171,10 @@ 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;

diff --git a/helm/software/matita/matitaAutoGui.mli b/helm/software/matita/matitaAutoGui.mli
index 6715298e2b7097a324ca9cb63cf2b97238133ea8..896886a02ee6231f1cac61026536a5b72c008969 100644 (file)
--- a/helm/software/matita/matitaAutoGui.mli
+++ b/helm/software/matita/matitaAutoGui.mli
@@ -30,3 +30,4 @@ type status =
     (int * Cic.term * bool * int * (int * Cic.term) list) list *
     (int * Cic.term * int) list * Cic.term list
 val auto_dialog : (unit -> status) -> unit
+val set_font_size: int -> unit

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index a77800c1e05192395e141aa075a5e361dde61944..96cd079e9dbf2d462c8724b632e0b5aac19ac784 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -1232,7 +1232,8 @@ class gui () =
 
     method private updateFontSize () =
       self#sourceView#misc#modify_font_by_name
-        (sprintf "%s %d" BuildTimeConf.script_font font_size)
+        (sprintf "%s %d" BuildTimeConf.script_font font_size);
+      MatitaAutoGui.set_font_size font_size
 
     method increaseFontSize () =
       font_size <- font_size + 1;