+ let vbox =
+ GPack.vbox ~packing:window#add () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let whdb =
+ GButton.button ~label:"Whd"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let reduceb =
+ GButton.button ~label:"Reduce"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let simplb =
+ GButton.button ~label:"Simpl"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox#pack ~expand:true ~padding:5) () in
+ let mmlwidget =
+ GMathView.math_view
+ ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
+object(self)
+ method mmlwidget = mmlwidget
+ method show () = window#misc#hide () ; window#show ()
+ initializer
+ ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
+ ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
+ ignore(whdb#connect#clicked (whd_in_scratch self)) ;
+ ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
+ ignore(simplb#connect#clicked (simpl_in_scratch self))
+end;;
+
+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 =
+ GMathView.math_view ~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 exactb =
+ GButton.button ~label:"Exact"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let introsb =
+ GButton.button ~label:"Intros"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let applyb =
+ GButton.button ~label:"Apply"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let elimsimplintrosb =
+ GButton.button ~label:"ElimSimplIntros"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let elimtypeb =
+ GButton.button ~label:"ElimType"
+ ~packing:(hbox3#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
+ let foldb =
+ GButton.button ~label:"Fold"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let cutb =
+ GButton.button ~label:"Cut"
+ ~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 changeb =
+ GButton.button ~label:"Change"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let letinb =
+ GButton.button ~label:"Let ... In"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let ringb =
+ GButton.button ~label:"Ring"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearbodyb =
+ GButton.button ~label:"ClearBody"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearb =
+ GButton.button ~label:"Clear"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let fourierb =
+ GButton.button ~label:"Fourier"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let rewritesimplb =
+ GButton.button ~label:"RewriteSimpl ->"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let reflexivityb =
+ GButton.button ~label:"Reflexivity"
+ ~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 symmetryb =
+ GButton.button ~label:"Symmetry"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let transitivityb =
+ GButton.button ~label:"Transitivity"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let leftb =
+ GButton.button ~label:"Left"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let rightb =
+ GButton.button ~label:"Right"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let assumptionb =
+ GButton.button ~label:"Assumption"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ let searchpatternb =
+ GButton.button ~label:"SearchPattern_Apply"
+ ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
+ ignore(exactb#connect#clicked exact) ;
+ ignore(applyb#connect#clicked apply) ;
+ ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
+ ignore(elimtypeb#connect#clicked elimtype) ;
+ ignore(whdb#connect#clicked whd) ;
+ ignore(reduceb#connect#clicked reduce) ;
+ ignore(simplb#connect#clicked simpl) ;
+ ignore(foldb#connect#clicked fold) ;
+ ignore(cutb#connect#clicked cut) ;
+ ignore(changeb#connect#clicked change) ;
+ ignore(letinb#connect#clicked letin) ;
+ ignore(ringb#connect#clicked ring) ;
+ ignore(clearbodyb#connect#clicked clearbody) ;
+ ignore(clearb#connect#clicked clear) ;
+ ignore(fourierb#connect#clicked fourier) ;
+ ignore(rewritesimplb#connect#clicked rewritesimpl) ;
+ ignore(reflexivityb#connect#clicked reflexivity) ;
+ ignore(symmetryb#connect#clicked symmetry) ;
+ ignore(transitivityb#connect#clicked transitivity) ;
+ ignore(leftb#connect#clicked left) ;
+ ignore(rightb#connect#clicked right) ;
+ ignore(assumptionb#connect#clicked assumption) ;
+ ignore(introsb#connect#clicked intros) ;
+ ignore(searchpatternb#connect#clicked searchPattern) ;
+ ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+ ))
+end
+;;
+
+class empty_page =
+ let vbox1 = GPack.vbox () in
+ let scrolled_window1 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox1#pack ~expand:true ~padding:5) () in
+ let proofw =
+ GMathView.math_view ~width:400 ~height:275
+ ~packing:(scrolled_window1#add) () in
+object(self)
+ method proofw = (assert false : GMathView.math_view)
+ method content = vbox1
+ method compute = (assert false : unit)
+end
+;;
+
+let empty_page = new empty_page;;
+
+class notebook =
+object(self)
+ val notebook = GPack.notebook ()
+ val pages = ref []
+ val mutable skip_switch_page_event = false
+ val mutable empty = true
+ method notebook = notebook
+ method add_page n =
+ let new_page = new page () in
+ empty <- false ;
+ pages := !pages @ [n,lazy (setgoal n),new_page] ;
+ notebook#append_page
+ ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
+ new_page#content#coerce
+ method remove_all_pages ~skip_switch_page_event:skip =
+ if empty then
+ notebook#remove_page 0 (* let's remove the empty page *)
+ else
+ List.iter (function _ -> notebook#remove_page 0) !pages ;
+ pages := [] ;
+ skip_switch_page_event <- skip
+ method set_current_page ~may_skip_switch_page_event n =
+ let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
+ let new_page = notebook#page_num page#content#coerce in
+ if may_skip_switch_page_event && new_page <> notebook#current_page then
+ skip_switch_page_event <- true ;
+ notebook#goto_page new_page
+ method set_empty_page =
+ empty <- true ;
+ pages := [] ;
+ notebook#append_page
+ ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
+ empty_page#content#coerce
+ method proofw =
+ let (_,_,page) = List.nth !pages notebook#current_page in
+ page#proofw
+ initializer
+ ignore
+ (notebook#connect#switch_page
+ (function i ->
+ let skip = skip_switch_page_event in
+ skip_switch_page_event <- false ;
+ if not skip then
+ try
+ let (metano,setgoal,page) = List.nth !pages i in
+ ProofEngine.goal := Some metano ;
+ Lazy.force (page#compute) ;
+ Lazy.force setgoal
+ with _ -> ()
+ ))
+end
+;;
+
+(* Main window *)
+
+class rendering_window output (notebook : notebook) =
+ let scratch_window = new scratch_window in
+ let window =
+ GWindow.window ~title:"MathML viewer" ~border_width:0
+ ~allow_shrink:false () in
+ let vbox_for_menu = GPack.vbox ~packing:window#add () in
+ (* menus *)
+ let handle_box = GBin.handle_box ~border_width:2
+ ~packing:(vbox_for_menu#pack ~padding:0) () in
+ let menubar = GMenu.menu_bar ~packing:handle_box#add () in
+ let factory0 = new GMenu.factory menubar in
+ let accel_group = factory0#accel_group in
+ (* file menu *)
+ let file_menu = factory0#add_submenu "File" in
+ let factory1 = new GMenu.factory file_menu ~accel_group in
+ let export_to_postscript_menu_item =
+ begin
+ let _ =
+ factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
+ ~callback:new_proof
+ in
+ let reopen_menu_item =
+ factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
+ ~callback:open_
+ in
+ let qed_menu_item =
+ factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
+ ignore (factory1#add_separator ()) ;
+ ignore
+ (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
+ ~callback:load) ;
+ let save_menu_item =
+ factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
+ in
+ ignore
+ (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
+ ignore (!save_set_sensitive false);
+ ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
+ ignore (!qed_set_sensitive false);
+ ignore (factory1#add_separator ()) ;
+ let export_to_postscript_menu_item =
+ factory1#add_item "Export to PostScript..."
+ ~callback:(export_to_postscript output) in
+ ignore (factory1#add_separator ()) ;
+ ignore
+ (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
+ export_to_postscript_menu_item
+ end in
+ (* edit menu *)
+ let edit_menu = factory0#add_submenu "Edit Current Proof" in
+ let factory2 = new GMenu.factory edit_menu ~accel_group in
+ let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
+ let proveit_menu_item =
+ factory2#add_item "Prove It" ~key:GdkKeysyms._I
+ ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
+ in
+ let focus_menu_item =
+ factory2#add_item "Focus" ~key:GdkKeysyms._F
+ ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
+ in
+ let _ =
+ focus_and_proveit_set_sensitive :=
+ function b ->
+ proveit_menu_item#misc#set_sensitive b ;
+ focus_menu_item#misc#set_sensitive b
+ in
+ let _ = !focus_and_proveit_set_sensitive false in
+ (* edit term menu *)
+ let edit_term_menu = factory0#add_submenu "Edit Term" in
+ let factory5 = new GMenu.factory edit_term_menu ~accel_group in
+ let check_menu_item =
+ factory5#add_item "Check Term" ~key:GdkKeysyms._C
+ ~callback:(check scratch_window) in
+ let _ = check_menu_item#misc#set_sensitive false in
+ (* search menu *)
+ let settings_menu = factory0#add_submenu "Search" in
+ let factory4 = new GMenu.factory settings_menu ~accel_group in
+ let _ =
+ factory4#add_item "Locate..." ~key:GdkKeysyms._T
+ ~callback:locate in
+ let show_menu_item =
+ factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
+ in
+ (* settings menu *)
+ let settings_menu = factory0#add_submenu "Settings" in
+ let factory3 = new GMenu.factory settings_menu ~accel_group in
+ let _ =
+ factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
+ ~callback:edit_aliases in
+ let _ = factory3#add_separator () in
+ let _ =
+ factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
+ ~callback:(function _ -> (settings_window ())#show ()) in
+ (* accel group *)
+ let _ = window#add_accel_group accel_group in
+ (* end of menus *)