From: Claudio Sacerdoti Coen Date: Wed, 6 Nov 2002 12:18:21 +0000 (+0000) Subject: - big interface changes: open goals are now collected in a notebook X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1dd5176f6d6a6247ebf941a1f6319a909f43d5fc;p=helm.git - big interface changes: open goals are now collected in a notebook - the code is less functional than before ;-( Open bugs/features: - the notebook page is re-generated (and stylesheets are applied again) even if it was already full --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 88b6f9206..c6e8ac763 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -88,7 +88,19 @@ let current_scratch_infos = ref None;; let id_to_uris = ref ([],function _ -> None);; let check_term = ref (fun _ _ _ -> assert false);; -let rendering_window = ref None;; + +exception RenderingWindowsNotInitialized;; + +let set_rendering_window,rendering_window = + let rendering_window_ref = ref None in + (function rw -> rendering_window_ref := Some rw), + (function () -> + match !rendering_window_ref with + None -> raise RenderingWindowsNotInitialized + | Some rw -> rw + ) +;; +ref None;; (* COMMAND LINE OPTIONS *) @@ -210,11 +222,7 @@ let locate_one_id id = wrong_xpointer_format_from_wrong_xpointer_format' uri ) result in let html= "

Locate Query:

" ^ get_last_query result ^ "

" in - begin - match !rendering_window with - None -> assert false - | Some rw -> output_html rw#outputhtml html ; - end ; + output_html (rendering_window ())#outputhtml html ; let uris' = match uris with [] -> @@ -481,10 +489,17 @@ prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",met raise (RefreshProofException e) ;; -let refresh_sequent (proofw : GMathView.math_view) = +let refresh_sequent ?(empty_notebook=true) notebook = try match !ProofEngine.goal with - None -> proofw#unload + None -> + if empty_notebook then + begin + notebook#remove_all_pages ; + notebook#set_empty_page + end + else + notebook#proofw#unload | Some metano -> let metasenv = match !ProofEngine.proof with @@ -501,7 +516,13 @@ let refresh_sequent (proofw : GMathView.math_view) = let sequent_mml = applyStylesheets sequent_doc sequent_styles sequent_args in - proofw#load_tree ~dom:sequent_mml ; + if empty_notebook then + begin + notebook#remove_all_pages ; + List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; + end ; + notebook#set_current_page metano ; + notebook#proofw#load_tree ~dom:sequent_mml ; current_goal_infos := Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) with @@ -559,16 +580,16 @@ let mml_of_cic_term metano term = (* TACTICS *) (***********************) -let call_tactic tactic rendering_window () = - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in +let call_tactic tactic () = + let notebook = (rendering_window ())#notebook in + let output = ((rendering_window ())#output : GMathView.math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in begin try tactic () ; - refresh_sequent proofw ; + refresh_sequent notebook ; refresh_proof output with RefreshSequentException e -> @@ -577,14 +598,14 @@ let call_tactic tactic rendering_window () = "sequent: " ^ Printexc.to_string e ^ "") ; ProofEngine.proof := savedproof ; ProofEngine.goal := savedgoal ; - refresh_sequent proofw + refresh_sequent notebook | RefreshProofException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e ^ "

") ; ProofEngine.proof := savedproof ; ProofEngine.goal := savedgoal ; - refresh_sequent proofw ; + refresh_sequent notebook ; refresh_proof output | e -> output_html outputhtml @@ -594,11 +615,11 @@ let call_tactic tactic rendering_window () = end ;; -let call_tactic_with_input tactic rendering_window () = - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in +let call_tactic_with_input tactic () = + let notebook = (rendering_window ())#notebook in + let output = ((rendering_window ())#output : GMathView.math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let inputt = ((rendering_window ())#inputt : GEdit.text) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in (*CSC: Gran cut&paste da sotto... *) @@ -645,7 +666,7 @@ let call_tactic_with_input tactic rendering_window () = in ProofEngine.proof := Some (uri,metasenv',bo,ty) ; tactic expr ; - refresh_sequent proofw ; + refresh_sequent notebook ; refresh_proof output done with @@ -657,14 +678,14 @@ let call_tactic_with_input tactic rendering_window () = "sequent: " ^ Printexc.to_string e ^ "") ; ProofEngine.proof := savedproof ; ProofEngine.goal := savedgoal ; - refresh_sequent proofw + refresh_sequent notebook | RefreshProofException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e ^ "

No term selected

") ;; -let call_tactic_with_input_and_goal_input tactic rendering_window () = +let call_tactic_with_input_and_goal_input tactic () = let module L = LogicalOperations in let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in + let notebook = (rendering_window ())#notebook in + let output = ((rendering_window ())#output : GMathView.math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let inputt = ((rendering_window ())#inputt : GEdit.text) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in - match proofw#get_selection with + match notebook#proofw#get_selection with Some node -> let xpath = ((node : Gdome.element)#getAttributeNS @@ -794,7 +815,7 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = ProofEngine.proof := Some (uri,metasenv',bo,ty) ; tactic ~goal_input:(Hashtbl.find ids_to_terms id) ~input:expr ; - refresh_sequent proofw ; + refresh_sequent notebook ; refresh_proof output done with @@ -809,14 +830,14 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = "sequent: " ^ Printexc.to_string e ^ "") ; ProofEngine.proof := savedproof ; ProofEngine.goal := savedgoal ; - refresh_sequent proofw + refresh_sequent notebook | RefreshProofException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e ^ "

No term selected

") ;; -let call_tactic_with_hypothesis_input tactic rendering_window () = +let call_tactic_with_hypothesis_input tactic () = let module L = LogicalOperations in let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let notebook = (rendering_window ())#notebook in + let output = ((rendering_window ())#output : GMathView.math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in - match proofw#get_selection with + match notebook#proofw#get_selection with Some node -> let xpath = ((node : Gdome.element)#getAttributeNS @@ -889,8 +910,8 @@ let call_tactic_with_hypothesis_input tactic rendering_window () = Some (_,_,ids_to_hypotheses) -> let id = xpath in tactic (Hashtbl.find ids_to_hypotheses id) ; - refresh_sequent rendering_window#proofw ; - refresh_proof rendering_window#output + refresh_sequent notebook ; + refresh_proof output | None -> assert false (* "ERROR: No current term!!!" *) with RefreshSequentException e -> @@ -899,14 +920,14 @@ let call_tactic_with_hypothesis_input tactic rendering_window () = "sequent: " ^ Printexc.to_string e ^ "") ; ProofEngine.proof := savedproof ; ProofEngine.goal := savedgoal ; - refresh_sequent proofw + refresh_sequent notebook | RefreshProofException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e ^ "

") ; ProofEngine.proof := savedproof ; ProofEngine.goal := savedgoal ; - refresh_sequent proofw ; + refresh_sequent notebook ; refresh_proof output | e -> output_html outputhtml @@ -920,77 +941,29 @@ let call_tactic_with_hypothesis_input tactic rendering_window () = ;; -let intros rendering_window = call_tactic ProofEngine.intros rendering_window;; -let exact rendering_window = - call_tactic_with_input ProofEngine.exact rendering_window -;; -let apply rendering_window = - call_tactic_with_input ProofEngine.apply rendering_window -;; -let elimsimplintros rendering_window = - call_tactic_with_input ProofEngine.elim_simpl_intros rendering_window -;; -let elimtype rendering_window = - call_tactic_with_input ProofEngine.elim_type rendering_window -;; -let whd rendering_window = - call_tactic_with_goal_input ProofEngine.whd rendering_window -;; -let reduce rendering_window = - call_tactic_with_goal_input ProofEngine.reduce rendering_window -;; -let simpl rendering_window = - call_tactic_with_goal_input ProofEngine.simpl rendering_window -;; -let fold rendering_window = - call_tactic_with_input ProofEngine.fold rendering_window -;; -let cut rendering_window = - call_tactic_with_input ProofEngine.cut rendering_window -;; -let change rendering_window = - call_tactic_with_input_and_goal_input ProofEngine.change rendering_window -;; -let letin rendering_window = - call_tactic_with_input ProofEngine.letin rendering_window -;; -let ring rendering_window = call_tactic ProofEngine.ring rendering_window;; -let clearbody rendering_window = - call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window -;; -let clear rendering_window = - call_tactic_with_hypothesis_input ProofEngine.clear rendering_window -;; -let fourier rendering_window = - call_tactic ProofEngine.fourier rendering_window -;; -let rewritesimpl rendering_window = - call_tactic_with_input ProofEngine.rewrite_simpl rendering_window -;; -let reflexivity rendering_window = - call_tactic ProofEngine.reflexivity rendering_window -;; -let symmetry rendering_window = - call_tactic ProofEngine.symmetry rendering_window -;; -let transitivity rendering_window = - call_tactic_with_input ProofEngine.transitivity rendering_window -;; -let left rendering_window = - call_tactic ProofEngine.left rendering_window -;; -let right rendering_window = - call_tactic ProofEngine.right rendering_window -;; -let assumption rendering_window = - call_tactic ProofEngine.assumption rendering_window -;; -(* -let prova_tatticali rendering_window = - call_tactic ProofEngine.prova_tatticali rendering_window -;; -*) - +let intros = call_tactic ProofEngine.intros;; +let exact = call_tactic_with_input ProofEngine.exact;; +let apply = call_tactic_with_input ProofEngine.apply;; +let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;; +let elimtype = call_tactic_with_input ProofEngine.elim_type;; +let whd = call_tactic_with_goal_input ProofEngine.whd;; +let reduce = call_tactic_with_goal_input ProofEngine.reduce;; +let simpl = call_tactic_with_goal_input ProofEngine.simpl;; +let fold = call_tactic_with_input ProofEngine.fold;; +let cut = call_tactic_with_input ProofEngine.cut;; +let change = call_tactic_with_input_and_goal_input ProofEngine.change;; +let letin = call_tactic_with_input ProofEngine.letin;; +let ring = call_tactic ProofEngine.ring;; +let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;; +let clear = call_tactic_with_hypothesis_input ProofEngine.clear;; +let fourier = call_tactic ProofEngine.fourier;; +let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;; +let reflexivity = call_tactic ProofEngine.reflexivity;; +let symmetry = call_tactic ProofEngine.symmetry;; +let transitivity = call_tactic_with_input ProofEngine.transitivity;; +let left = call_tactic ProofEngine.left;; +let right = call_tactic ProofEngine.right;; +let assumption = call_tactic ProofEngine.assumption;; let whd_in_scratch scratch_window = call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch @@ -1014,7 +987,7 @@ let simpl_in_scratch scratch_window = exception OpenConjecturesStillThere;; exception WrongProof;; -let qed rendering_window () = +let qed () = match !ProofEngine.proof with None -> assert false | Some (uri,[],bo,ty) -> @@ -1034,7 +1007,7 @@ let qed rendering_window () = let mml = mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types in - (rendering_window#output : GMathView.math_view)#load_tree mml ; + ((rendering_window ())#output : GMathView.math_view)#load_tree mml ; current_cic_infos := Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures, @@ -1051,8 +1024,8 @@ let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";; *) let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";; -let save rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in +let save () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in match !ProofEngine.proof with None -> assert false | Some (uri, metasenv, bo, ty) -> @@ -1091,11 +1064,10 @@ let typecheck_loaded_proof metasenv bo ty = ignore (T.type_of_aux' metasenv [] bo) ;; -(*CSC: ancora da implementare *) -let load rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in +let load () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = ((rendering_window ())#output : GMathView.math_view) in + let notebook = (rendering_window ())#notebook in try let uri = UriManager.uri_of_string "cic:/dummy.con" in match CicParser.obj_of_xml prooffiletype (Some prooffile) with @@ -1109,7 +1081,7 @@ let load rendering_window () = | (metano,_,_)::_ -> Some metano ) ; refresh_proof output ; - refresh_sequent proofw ; + refresh_sequent notebook ; output_html outputhtml ("

Current proof type loaded from " ^ prooffiletype ^ "

") ; @@ -1131,11 +1103,13 @@ let load rendering_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -let proveit rendering_window () = +let proveit () = let module L = LogicalOperations in let module G = Gdome in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - match rendering_window#output#get_selection with + let notebook = (rendering_window ())#notebook in + let output = (rendering_window ())#output in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + match (rendering_window ())#output#get_selection with Some node -> let xpath = ((node : Gdome.element)#getAttributeNS @@ -1153,8 +1127,8 @@ let proveit rendering_window () = Some (ids_to_terms, ids_to_father_ids, _, _) -> let id = xpath in L.to_sequent id ids_to_terms ids_to_father_ids ; - refresh_proof rendering_window#output ; - refresh_sequent rendering_window#proofw + refresh_proof output ; + refresh_sequent notebook | None -> assert false (* "ERROR: No current term!!!" *) with RefreshSequentException e -> @@ -1172,11 +1146,12 @@ let proveit rendering_window () = | None -> assert false (* "ERROR: No selection!!!" *) ;; -let focus rendering_window () = +let focus () = let module L = LogicalOperations in let module G = Gdome in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - match rendering_window#output#get_selection with + let notebook = (rendering_window ())#notebook in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + match (rendering_window ())#output#get_selection with Some node -> let xpath = ((node : Gdome.element)#getAttributeNS @@ -1194,7 +1169,7 @@ let focus rendering_window () = Some (ids_to_terms, ids_to_father_ids, _, _) -> let id = xpath in L.focus id ids_to_terms ids_to_father_ids ; - refresh_sequent rendering_window#proofw + refresh_sequent notebook | None -> assert false (* "ERROR: No current term!!!" *) with RefreshSequentException e -> @@ -1215,45 +1190,19 @@ let focus rendering_window () = exception NoPrevGoal;; exception NoNextGoal;; -let prevgoal metasenv metano = - let rec aux = - function - [] -> assert false - | [(m,_,_)] -> raise NoPrevGoal - | (n,_,_)::(m,_,_)::_ when m=metano -> n - | _::tl -> aux tl - in - aux metasenv -;; - -let nextgoal metasenv metano = - let rec aux = - function - [] -> assert false - | [(m,_,_)] when m = metano -> raise NoNextGoal - | (m,_,_)::(n,_,_)::_ when m=metano -> n - | _::tl -> aux tl - in - aux metasenv -;; - -let prev_or_next_goal select_goal rendering_window () = +let setgoal metano = let module L = LogicalOperations in let module G = Gdome in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let notebook = (rendering_window ())#notebook in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let metasenv = match !ProofEngine.proof with None -> assert false | Some (_,metasenv,_,_) -> metasenv - in - let metano = - match !ProofEngine.goal with - None -> assert false - | Some m -> m in try - ProofEngine.goal := Some (select_goal metasenv metano) ; - refresh_sequent rendering_window#proofw + ProofEngine.goal := Some metano ; + refresh_sequent ~empty_notebook:false notebook ; with RefreshSequentException e -> output_html outputhtml @@ -1266,12 +1215,12 @@ let prev_or_next_goal select_goal rendering_window () = exception NotADefinition;; -let open_ rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let oldinputt = (rendering_window#oldinputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in +let open_ () = + let inputt = ((rendering_window ())#inputt : GEdit.text) in + let oldinputt = ((rendering_window ())#oldinputt : GEdit.text) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = ((rendering_window ())#output : GMathView.math_view) in + let notebook = (rendering_window ())#notebook in let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen in try @@ -1288,7 +1237,7 @@ let open_ rendering_window () = ProofEngine.proof := Some (uri, metasenv, bo, ty) ; ProofEngine.goal := None ; - refresh_sequent proofw ; + refresh_sequent notebook ; refresh_proof output ; inputt#delete_text 0 inputlen ; ignore(oldinputt#insert_text input oldinputt#length) @@ -1306,12 +1255,12 @@ let open_ rendering_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -let state rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let oldinputt = (rendering_window#oldinputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in +let state () = + let inputt = ((rendering_window ())#inputt : GEdit.text) in + let oldinputt = ((rendering_window ())#oldinputt : GEdit.text) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = ((rendering_window ())#output : GMathView.math_view) in + let notebook = (rendering_window ())#notebook in let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen ^ "\n" in (* Do something interesting *) @@ -1333,7 +1282,7 @@ let state rendering_window () = Some (UriManager.uri_of_string "cic:/dummy.con", (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; ProofEngine.goal := Some 1 ; - refresh_sequent proofw ; + refresh_sequent notebook ; refresh_proof output ; done with @@ -1366,9 +1315,9 @@ prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; raise e ;; -let check rendering_window scratch_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in +let check scratch_window () = + let inputt = ((rendering_window ())#inputt : GEdit.text) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen ^ "\n" in let curi,metasenv = @@ -1428,9 +1377,9 @@ let user_uri_choice ~title ~msg uris = String.sub uri 4 (String.length uri - 4) ;; -let locate rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in +let locate () = + let inputt = ((rendering_window ())#inputt : GEdit.text) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen in try @@ -1459,9 +1408,9 @@ let locate rendering_window () = ("

" ^ Printexc.to_string e ^ "

") ;; -let searchPattern rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in +let searchPattern () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let inputt = ((rendering_window ())#inputt : GEdit.text) in let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen in let level = int_of_string input in @@ -1712,81 +1661,14 @@ object(self) ignore(simplb#connect#clicked (simpl_in_scratch self)) end;; -(* Main window *) - -class rendering_window output proofw (label : GMisc.label) = - let window = - GWindow.window ~title:"MathML viewer" ~border_width:2 () in - let hbox0 = - GPack.hbox ~packing:window#add () in - let vbox = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in - let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in - let scrolled_window0 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~padding:5) () in - let _ = scrolled_window0#add output#coerce in - let hbox1 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let settingsb = - GButton.button ~label:"Settings" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let button_export_to_postscript = - GButton.button ~label:"export_to_postscript" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let qedb = - GButton.button ~label:"Qed" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let saveb = - GButton.button ~label:"Save" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let loadb = - GButton.button ~label:"Load" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let hbox2 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let proveitb = - GButton.button ~label:"Prove It" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let focusb = - GButton.button ~label:"Focus" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let prevgoalb = - GButton.button ~label:"<" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let nextgoalb = - GButton.button ~label:">" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 - ~packing:(vbox#pack ~padding:5) () in - let hbox4 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let stateb = - GButton.button ~label:"State" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let openb = - GButton.button ~label:"Open" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let locateb = - GButton.button ~label:"Locate" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let searchpatternb = - GButton.button ~label:"SearchPattern" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 - ~packing:(vbox#pack ~padding:5) () in - let vbox1 = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in +class page () = + let vbox1 = GPack.vbox () in let scrolled_window1 = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in - let _ = scrolled_window1#add proofw#coerce in + let proofw = + GMathView.math_view ~width:400 ~height:275 + ~packing:(scrolled_window1#add) () in let hbox3 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let exactb = @@ -1862,77 +1744,182 @@ class rendering_window output proofw (label : GMisc.label) = let assumptionb = GButton.button ~label:"Assumption" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in -(* - let prova_tatticalib = - GButton.button ~label:"Prova_tatticali" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in -*) +object + method proofw = proofw + method content = vbox1 + initializer + 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) ; + initializer + ignore(proofw#connect#selection_changed (choose_selection proofw)) ; +end +;; + +class notebook = +object(self) + val notebook = GPack.notebook () + val pages = ref [] + val mutable skip_switch_page_event = false + method notebook = notebook + method add_page n = + let new_page = new page () in + pages := !pages @ [n,new_page] ; + notebook#append_page + ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce) + new_page#content#coerce + method remove_all_pages = + List.iter (function _ -> notebook#remove_page 0) !pages ; + pages := [] ; + method set_current_page n = + let (_,page) = List.find (function (m,_) -> m=n) !pages in + let new_page = notebook#page_num page#content#coerce in + if new_page <> notebook#current_page then + skip_switch_page_event <- true ; + notebook#goto_page new_page + method set_empty_page = self#add_page (-1) + method proofw = + (snd (List.nth !pages notebook#current_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 = fst (List.nth !pages i) in + setgoal metano + with _ -> () + )) +end +;; + +(* Main window *) + +class rendering_window output (notebook : notebook) (label : GMisc.label) = + let window = + GWindow.window ~title:"MathML viewer" ~border_width:2 () in + let hbox0 = + GPack.hbox ~packing:window#add () in + let vbox = + GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in + let scrolled_window0 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~padding:5) () in + let _ = scrolled_window0#add output#coerce in + let hbox1 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let settingsb = + GButton.button ~label:"Settings" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let button_export_to_postscript = + GButton.button ~label:"export_to_postscript" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let qedb = + GButton.button ~label:"Qed" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let saveb = + GButton.button ~label:"Save" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let loadb = + GButton.button ~label:"Load" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let closeb = + GButton.button ~label:"Close" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let hbox2 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let proveitb = + GButton.button ~label:"Prove It" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let focusb = + GButton.button ~label:"Focus" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 + ~packing:(vbox#pack ~padding:5) () in + let hbox4 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let stateb = + GButton.button ~label:"State" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let openb = + GButton.button ~label:"Open" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let locateb = + GButton.button ~label:"Locate" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let searchpatternb = + GButton.button ~label:"SearchPattern" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 + ~packing:(vbox#pack ~padding:5) () in + let vboxl = + GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + vboxl#pack ~expand:false ~fill:false ~padding:5 notebook#notebook#coerce in let outputhtml = GHtml.xmhtml ~source:"" ~width:400 ~height: 200 - ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) + ~packing:(vboxl#pack ~expand:false ~fill:false ~padding:5) ~show:true () in let scratch_window = new scratch_window outputhtml in -object(self) +object method outputhtml = outputhtml method oldinputt = oldinputt method inputt = inputt method output = (output : GMathView.math_view) - method proofw = (proofw : GMathView.math_view) + method notebook = notebook method show = window#show initializer + notebook#set_empty_page ; button_export_to_postscript#misc#set_sensitive false ; check_term := (check_term_in_scratch scratch_window) ; (* signal handlers here *) ignore(output#connect#selection_changed - (function elem -> proofw#unload ; choose_selection output elem)) ; - ignore(proofw#connect#selection_changed (choose_selection proofw)) ; + (function elem -> notebook#proofw#unload ; choose_selection output elem)) ; ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ; let settings_window = new settings_window output scrolled_window0 button_export_to_postscript (choose_selection output) in ignore(settingsb#connect#clicked settings_window#show) ; ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; - ignore(qedb#connect#clicked (qed self)) ; - ignore(saveb#connect#clicked (save self)) ; - ignore(loadb#connect#clicked (load self)) ; - ignore(proveitb#connect#clicked (proveit self)) ; - ignore(focusb#connect#clicked (focus self)) ; - ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ; - ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ; + ignore(qedb#connect#clicked qed) ; + ignore(saveb#connect#clicked save) ; + ignore(loadb#connect#clicked load) ; + ignore(proveitb#connect#clicked proveit) ; + ignore(focusb#connect#clicked focus) ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - ignore(stateb#connect#clicked (state self)) ; - ignore(openb#connect#clicked (open_ self)) ; - ignore(checkb#connect#clicked (check self scratch_window)) ; - ignore(locateb#connect#clicked (locate self)) ; - ignore(searchpatternb#connect#clicked (searchPattern self)) ; - ignore(exactb#connect#clicked (exact self)) ; - ignore(applyb#connect#clicked (apply self)) ; - ignore(elimsimplintrosb#connect#clicked (elimsimplintros self)) ; - ignore(elimtypeb#connect#clicked (elimtype self)) ; - ignore(whdb#connect#clicked (whd self)) ; - ignore(reduceb#connect#clicked (reduce self)) ; - ignore(simplb#connect#clicked (simpl self)) ; - ignore(foldb#connect#clicked (fold self)) ; - ignore(cutb#connect#clicked (cut self)) ; - ignore(changeb#connect#clicked (change self)) ; - ignore(letinb#connect#clicked (letin self)) ; - ignore(ringb#connect#clicked (ring self)) ; - ignore(clearbodyb#connect#clicked (clearbody self)) ; - ignore(clearb#connect#clicked (clear self)) ; - ignore(fourierb#connect#clicked (fourier self)) ; - ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; - ignore(reflexivityb#connect#clicked (reflexivity self)) ; - ignore(symmetryb#connect#clicked (symmetry self)) ; - ignore(transitivityb#connect#clicked (transitivity self)) ; - ignore(leftb#connect#clicked (left self)) ; - ignore(rightb#connect#clicked (right self)) ; - ignore(assumptionb#connect#clicked (assumption self)) ; -(* - ignore(prova_tatticalib#connect#clicked (prova_tatticali self)) ; -*) - ignore(introsb#connect#clicked (intros self)) ; + ignore(stateb#connect#clicked state) ; + ignore(openb#connect#clicked open_) ; + ignore(checkb#connect#clicked (check scratch_window)) ; + ignore(locateb#connect#clicked locate) ; + ignore(searchpatternb#connect#clicked searchPattern) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) end;; @@ -1941,13 +1928,11 @@ end;; let initialize_everything () = let module U = Unix in - let output = GMathView.math_view ~width:350 ~height:280 () - and proofw = GMathView.math_view ~width:400 ~height:275 () - and label = GMisc.label ~text:"gTopLevel" () in - let rendering_window' = - new rendering_window output proofw label - in - rendering_window := Some rendering_window' ; + let output = GMathView.math_view ~width:350 ~height:280 () in + let notebook = new notebook in + let label = GMisc.label ~text:"gTopLevel" () in + let rendering_window' = new rendering_window output notebook label in + set_rendering_window rendering_window' ; rendering_window'#show () ; GMain.Main.main () ;;