+ let sequent_viewer =
+ TermViewer.sequent_viewer
+ ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
+object(self)
+ val mutable term = Cic.Rel 1 (* dummy value *)
+ val mutable context = ([] : Cic.context) (* dummy value *)
+ val mutable metasenv = ([] : Cic.metasenv) (* dummy value *)
+ method sequent_viewer = sequent_viewer
+ method show () = window#misc#hide () ; window#show ()
+ method term = term
+ method set_term t = term <- t
+ method context = context
+ method set_context t = context <- t
+ method metasenv = metasenv
+ method set_metasenv t = metasenv <- t
+ initializer
+ ignore
+ (sequent_viewer#connect#selection_changed (choose_selection sequent_viewer));
+ ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
+ ignore(whdb#connect#clicked InvokeTactics'.whd_in_scratch) ;
+ ignore(reduceb#connect#clicked InvokeTactics'.reduce_in_scratch) ;
+ ignore(simplb#connect#clicked InvokeTactics'.simpl_in_scratch)
+end;;
+
+let open_contextual_menu_for_selected_terms mmlwidget infos =
+ let button = GdkEvent.Button.button infos in
+ let terms_selected = List.length mmlwidget#get_selections > 0 in
+ if button = 3 then
+ begin
+ let time = GdkEvent.Button.time infos in
+ let menu = GMenu.menu () in
+ let f = new GMenu.factory menu in
+ let whd_menu_item =
+ f#add_item "Whd" ~key:GdkKeysyms._W ~callback:InvokeTactics'.whd in
+ let reduce_menu_item =
+ f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:InvokeTactics'.reduce in
+ let simpl_menu_item =
+ f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:InvokeTactics'.simpl in
+ let _ = f#add_separator () in
+ let generalize_menu_item =
+ f#add_item "Generalize"
+ ~key:GdkKeysyms._G ~callback:InvokeTactics'.generalize in
+ let _ = f#add_separator () in
+ let clear_menu_item =
+ f#add_item "Clear" ~key:GdkKeysyms._C ~callback:InvokeTactics'.clear in
+ let clearbody_menu_item =
+ f#add_item "ClearBody"
+ ~key:GdkKeysyms._B ~callback:InvokeTactics'.clearbody
+ in
+ whd_menu_item#misc#set_sensitive terms_selected ;
+ reduce_menu_item#misc#set_sensitive terms_selected ;
+ simpl_menu_item#misc#set_sensitive terms_selected ;
+ generalize_menu_item#misc#set_sensitive terms_selected ;
+ clear_menu_item#misc#set_sensitive terms_selected ;
+ clearbody_menu_item#misc#set_sensitive terms_selected ;
+ menu#popup ~button ~time
+ end ;
+ true
+;;
+
+class page () =
+ let vbox1 = GPack.vbox () in
+object(self)
+ val mutable proofw_ref = None
+ val mutable compute_ref = None
+ method proofw =
+ Lazy.force self#compute ;
+ match proofw_ref with
+ None -> assert false
+ | Some proofw -> proofw
+ method content = vbox1
+ method compute =
+ match compute_ref with
+ None -> assert false
+ | Some compute -> compute
+ initializer
+ compute_ref <-
+ Some (lazy (
+ let scrolled_window1 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox1#pack ~expand:true ~padding:5) () in
+ let proofw =
+ TermViewer.sequent_viewer ~width:400 ~height:275
+ ~packing:(scrolled_window1#add) () in
+ let _ = proofw_ref <- Some proofw in
+ let hbox3 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let ringb =
+ GButton.button ~label:"Ring"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let fourierb =
+ GButton.button ~label:"Fourier"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let reflexivityb =
+ GButton.button ~label:"Reflexivity"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let symmetryb =
+ GButton.button ~label:"Symmetry"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let assumptionb =
+ GButton.button ~label:"Assumption"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let contradictionb =
+ GButton.button ~label:"Contradiction"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let autob=
+ GButton.button ~label:"Auto"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox4 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let existsb =
+ GButton.button ~label:"Exists"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let splitb =
+ GButton.button ~label:"Split"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let leftb =
+ GButton.button ~label:"Left"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let rightb =
+ GButton.button ~label:"Right"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let searchpatternb =
+ GButton.button ~label:"SearchPattern_Apply"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox5 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let exactb =
+ GButton.button ~label:"Exact"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let introsb =
+ GButton.button ~label:"Intros"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let applyb =
+ GButton.button ~label:"Apply"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let elimintrossimplb =
+ GButton.button ~label:"ElimIntrosSimpl"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let elimtypeb =
+ GButton.button ~label:"ElimType"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let foldwhdb =
+ GButton.button ~label:"Fold_whd"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let foldreduceb =
+ GButton.button ~label:"Fold_reduce"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox6 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let foldsimplb =
+ GButton.button ~label:"Fold_simpl"
+ ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+ let cutb =
+ GButton.button ~label:"Cut"
+ ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+ let changeb =
+ GButton.button ~label:"Change"
+ ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+ let letinb =
+ GButton.button ~label:"Let ... In"
+ ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+ let rewritesimplb =
+ GButton.button ~label:"RewriteSimpl ->"
+ ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+ let rewritebacksimplb =
+ GButton.button ~label:"RewriteSimpl <-"
+ ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox7 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let absurdb =
+ GButton.button ~label:"Absurd"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let decomposeb =
+ GButton.button ~label:"Decompose"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let transitivityb =
+ GButton.button ~label:"Transitivity"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let replaceb =
+ GButton.button ~label:"Replace"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let injectionb =
+ GButton.button ~label:"Injection"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let discriminateb =
+ GButton.button ~label:"Discriminate"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+(* Zack: spostare in una toolbar
+ let generalizeb =
+ GButton.button ~label:"Generalize"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearbodyb =
+ GButton.button ~label:"ClearBody"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearb =
+ GButton.button ~label:"Clear"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let whdb =
+ GButton.button ~label:"Whd"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let reduceb =
+ GButton.button ~label:"Reduce"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let simplb =
+ GButton.button ~label:"Simpl"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+*)
+
+ ignore(exactb#connect#clicked InvokeTactics'.exact) ;
+ ignore(applyb#connect#clicked InvokeTactics'.apply) ;
+ ignore(elimintrossimplb#connect#clicked InvokeTactics'.elimintrossimpl) ;
+ ignore(elimtypeb#connect#clicked InvokeTactics'.elimtype) ;
+ ignore(foldwhdb#connect#clicked InvokeTactics'.fold_whd) ;
+ ignore(foldreduceb#connect#clicked InvokeTactics'.fold_reduce) ;
+ ignore(foldsimplb#connect#clicked InvokeTactics'.fold_simpl) ;
+ ignore(cutb#connect#clicked InvokeTactics'.cut) ;
+ ignore(changeb#connect#clicked InvokeTactics'.change) ;
+ ignore(letinb#connect#clicked InvokeTactics'.letin) ;
+ ignore(ringb#connect#clicked InvokeTactics'.ring) ;
+ ignore(fourierb#connect#clicked InvokeTactics'.fourier) ;
+ ignore(rewritesimplb#connect#clicked InvokeTactics'.rewritesimpl) ;
+ ignore(rewritebacksimplb#connect#clicked InvokeTactics'.rewritebacksimpl) ;
+ ignore(replaceb#connect#clicked InvokeTactics'.replace) ;
+ ignore(reflexivityb#connect#clicked InvokeTactics'.reflexivity) ;
+ ignore(symmetryb#connect#clicked InvokeTactics'.symmetry) ;
+ ignore(transitivityb#connect#clicked InvokeTactics'.transitivity) ;
+ ignore(existsb#connect#clicked InvokeTactics'.exists) ;
+ ignore(splitb#connect#clicked InvokeTactics'.split) ;
+ ignore(leftb#connect#clicked InvokeTactics'.left) ;
+ ignore(rightb#connect#clicked InvokeTactics'.right) ;
+ ignore(assumptionb#connect#clicked InvokeTactics'.assumption) ;
+ ignore(absurdb#connect#clicked InvokeTactics'.absurd) ;
+ ignore(contradictionb#connect#clicked InvokeTactics'.contradiction) ;
+ ignore(introsb#connect#clicked InvokeTactics'.intros) ;
+ ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ;
+ ignore(searchpatternb#connect#clicked searchPattern) ;
+ ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
+ ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
+ ignore(autob#connect#clicked InvokeTactics'.auto) ;
+(* Zack: spostare in una toolbar
+ ignore(whdb#connect#clicked whd) ;
+ ignore(reduceb#connect#clicked reduce) ;
+ ignore(simplb#connect#clicked simpl) ;
+ ignore(clearbodyb#connect#clicked clearbody) ;
+ ignore(clearb#connect#clicked clear) ;
+ ignore(generalizeb#connect#clicked generalize) ;
+*)
+ ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+ ignore
+ ((new GObj.event_ops proofw#as_widget)#connect#button_press
+ (open_contextual_menu_for_selected_terms proofw)) ;
+ ))
+end
+;;
+
+class empty_page =
+ let vbox1 = GPack.vbox () in