X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaAutoGui.ml;h=9ba6dd89828052a7e084cc0a42e9ec3e54f3122c;hb=a5bfa65b18a876fca982270f673c686a7d124f65;hp=e3a5bff187d758d8a674a0a08617961bdf478fcd;hpb=a1c4c601850c71e094a4703af00f02ca2026d8ed;p=helm.git
diff --git a/matita/matitaAutoGui.ml b/matita/matitaAutoGui.ml
index e3a5bff18..9ba6dd898 100644
--- a/matita/matitaAutoGui.ml
+++ b/matita/matitaAutoGui.ml
@@ -25,7 +25,8 @@
*)
type status =
- Cic.context * (Cic.term * (int * Cic.term) list) list * Cic.term list *
+ Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
+ (int * Cic.term * int) list *
Cic.term list
let fake_goal = Cic.Implicit None;;
let fake_candidates = [];;
@@ -34,13 +35,18 @@ let start = ref 0;;
let len = ref 10;;
let pp c t =
- let names = List.map (function None -> None | Some (n,_) -> Some n) c in
+ (*
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
- CicPp.pp t names
+ 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
;;
let pp_goal context x =
if x == fake_goal then "" else pp context x
@@ -50,7 +56,8 @@ let pp_candidate context x = pp context x
let sublist start len l =
let rec aux pos len = function
| [] when pos < start -> aux (pos+1) len []
- | [] when len > 0 -> (fake_goal, fake_candidates) :: aux (pos+1) (len-1) []
+ | [] when len > 0 ->
+ (0,fake_goal, false, 0, fake_candidates) :: aux (pos+1) (len-1) []
| [] (* when len <= 0 *) -> []
| he::tl when pos < start -> aux (pos+1) len tl
| he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl
@@ -59,12 +66,14 @@ let sublist start len l =
aux 0 len l
;;
-let cell_of_candidate context ?(active=false) g id c =
+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*)) ()
+ ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*))
+ ()
in
+ button#misc#set_size_request ~height ();
if active then
button#misc#set_sensitive false;
let text =
@@ -72,46 +81,67 @@ let cell_of_candidate 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 win_width context goal =
- GMisc.label ~text:(pp_goal context goal) ~xalign:0.0 ()
+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)
+ ~line_wrap:false
+ ~ellipsize:`END
+ ~height
+ ()
;;
-let cell_of_int n =
- GMisc.label ~text:(string_of_int n)
- ~line_wrap:true ~justify:`RIGHT ()
+let cell_of_row_header height n k id =
+ GMisc.label
+ ~markup:("" ^ string_of_int n ^ "(" ^
+ string_of_int id ^ "|" ^ string_of_int k ^ ")")
+ ~line_wrap:true ~justify:`LEFT ~height ~width:80 ()
;;
-let cell_of_candidates context goal cads =
+let cell_of_candidates height grey context goal cads =
let hbox = GPack.hbox () in
match cads with
| [] -> hbox
| (id,c)::tl ->
hbox#pack
- (cell_of_candidate ~active:true context goal id c :> GObj.widget);
+ (cell_of_candidate height ~active:grey
+ context goal id c :> GObj.widget);
List.iter
(fun (id,c) ->
- hbox#pack (cell_of_candidate context goal id c :> GObj.widget)) tl;
+ hbox#pack (cell_of_candidate height context goal id c :> GObj.widget)) tl;
hbox
;;
-let elems_to_rows context win_width (table : GPack.table) (or_list) =
+let elems_to_rows height context win_width (table : GPack.table) (or_list) =
+ let height = height / ((List.length or_list) + 1) in
let _ =
List.fold_left
- (fun position (goal, candidates) ->
+ (fun position (goal_id, goal, grey, depth, candidates) ->
table#attach ~left:0 ~top:position
- (cell_of_int (position + !start) :> GObj.widget);
- table#attach ~left:1 ~top:position ~expand:`BOTH ~fill:`BOTH
- (cell_of_goal win_width context goal :> GObj.widget);
+ (cell_of_row_header height (position + !start)
+ depth goal_id :> GObj.widget);
+ table#attach ~left:1 ~top:position ~fill:`BOTH
+ (cell_of_goal height win_width context goal :> GObj.widget);
table#attach ~left:2 ~top:position
- (cell_of_candidates context goal candidates :> GObj.widget);
+ (cell_of_candidates height grey context goal candidates :> GObj.widget);
position+1)
0 or_list
in
()
;;
-let old_displayed_status = ref ([]);;
+let old_displayed_status = ref [];;
let old_size = ref 0;;
let fill_win (win : MatitaGeneratedGui.autoWin) cb =
@@ -121,7 +151,8 @@ let fill_win (win : MatitaGeneratedGui.autoWin) cb =
let win_size = win#toplevel#misc#allocation.Gtk.width in
let ctx, or_list, and_list, last_moves = status in
let displayed_status =
- sublist !start !len (or_list @ (List.map (fun x -> x,[]) and_list))
+ sublist !start !len
+ (or_list @ (List.map (fun (id,x,d) -> id,x,false,d,[]) and_list))
in
if displayed_status <> !old_displayed_status || !old_size <> win_size then
begin
@@ -130,7 +161,8 @@ let fill_win (win : MatitaGeneratedGui.autoWin) cb =
win#labelLAST#set_text
(String.concat ";" (List.map (pp_candidate ctx) last_moves));
List.iter win#table#remove win#table#children;
- elems_to_rows ctx win_size win#table displayed_status;
+ 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
@@ -139,6 +171,11 @@ let fill_win (win : MatitaGeneratedGui.autoWin) cb =
let auto_dialog elems =
let win = new MatitaGeneratedGui.autoWin () in
+ let width = Gdk.Screen.width () in
+ let height = Gdk.Screen.height () in
+ let main_w = width * 70 / 100 in
+ let main_h = height * 60 / 100 in
+ win#toplevel#resize ~width:main_w ~height:main_h;
win#check_widgets ();
win#table#set_columns 3;
win#table#set_col_spacings 6;
@@ -148,15 +185,35 @@ let auto_dialog elems =
ignore(win#buttonDOWN#connect#clicked
(fun _ -> incr start; fill_win win elems));
ignore(win#buttonCLOSE#connect#clicked
- (fun _ -> win#toplevel#destroy ();GMain.Main.quit ()));
+ (fun _ ->
+ Auto.pause false;
+ 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
- (fun _ -> Auto.pause true));
+ (fun _ ->
+ Auto.pause true;
+ win#buttonPLAY#misc#set_sensitive true;
+ win#buttonPAUSE#misc#set_sensitive false;));
ignore(win#buttonPLAY#connect#clicked
- (fun _ -> Auto.pause false;Auto.step ()));
+ (fun _ ->
+ Auto.pause false;
+ Auto.step ();
+ win#buttonPLAY#misc#set_sensitive false;
+ win#buttonPAUSE#misc#set_sensitive true;));
ignore(win#buttonNEXT#connect#clicked
(fun _ -> Auto.step ()));
+ Auto.pause true;
+ win#buttonPLAY#misc#set_sensitive true;
+ win#buttonPAUSE#misc#set_sensitive false;
fill_win win elems;
win#toplevel#show ();
GtkThread.main ();