severe bug found in parallel zeta

[helm.git] / helm / software / matita / matitaAutoGui.ml

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index 0436c206dbb3827b52b5f083c1a46644bdab4e94..588dc5fecd09363f7de821a80eecb261ed083624 100644 (file)
--- 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:"?<sub>$1</sub>" txt_t
+  (if size > 0 then "<span font_desc=\""^string_of_int size^"\">" else "") ^
+  (MatitaGtkMisc.escape_pango_markup
+    (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
+      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 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,26 +84,35 @@ 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 
-    (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 = 
   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
@@ -114,7 +139,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) ->
@@ -135,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
@@ -148,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); ()
 ;;
@@ -180,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 _ ->