X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaAutoGui.ml;h=c7b06645b45cfe4948e63303897b4633b20ba6a0;hb=c5cee90d95a54db8897a688f0bade4c503d82e15;hp=0436c206dbb3827b52b5f083c1a46644bdab4e94;hpb=a180bddcd4a8f35de3d7292162ba05d0077723aa;p=helm.git

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index 0436c206d..c7b06645b 100644
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -35,7 +35,6 @@ let start = ref 0;;
 let len = ref 10;;
 
 let pp c t =
-  (*
   let t = 
     ProofEngineReduction.replace 
       ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) 
@@ -43,10 +42,6 @@ let pp c 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:"?<sub>$1</sub>" txt_t
 ;;
 let pp_goal context x = 
   if x == fake_goal then "" else pp context x
@@ -81,7 +76,17 @@ let cell_of_candidate height context ?(active=false) g id c =
   in
   tooltip#set_tip ~text (button :> GObj.widget);
   ignore(button#connect#clicked 
-    (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
+    (fun _ -> 
+      let menu = GMenu.menu () in
+      let follow = GMenu.menu_item ~label:"Follow" () in
+      let prune = GMenu.menu_item ~label:"Prune" () in
+      ignore (follow#connect#activate 
+        (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
+      ignore (prune#connect#activate 
+        (fun _ -> HLog.warn (string_of_int id); Auto.give_prune_hint id));
+      menu#append follow;
+      menu#append prune;
+      menu#popup 0 (GtkMain.Main.get_current_event_time ())));
   button
 ;;
 let cell_of_goal height win_width context goal = 
@@ -114,7 +119,7 @@ let cell_of_candidates height grey context goal cads =
 ;;
 
 let elems_to_rows height context win_width (table : GPack.table) (or_list) =
-  let height = height / (List.length or_list) in
+  let height = height / ((List.length or_list) + 1) in
   let _ = 
    List.fold_left 
     (fun position (goal_id, goal, grey, depth, candidates) ->
@@ -180,6 +185,12 @@ let auto_dialog elems =
       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