From: Stefano Zacchiroli Date: Thu, 3 Feb 2005 10:43:04 +0000 (+0000) Subject: snapshot, notably: X-Git-Tag: V_0_1_0~61 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7deafec4fd4b2eebf4d4061f21ee5c47bd15b062;p=helm.git snapshot, notably: - refactoring of modules and classes: added a lot more of constructors and singleton instances so that objects that are really singleton (e.g. disambiguator, parser, db handle, ...) are not passed between functions Note that objects that are dependent on whether we are running matita or matitac (like the console) can't be made singleton --- diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index fd460dd24..728a87112 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -413,44 +413,6 @@ - - Matita: current proof - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - 700 - 525 - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - - - - True - True - False - - - - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - - - - - - - 10 Select File @@ -1821,45 +1783,6 @@ Copyright (C) 2004, - - 300 - 200 - Matita: check term - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - - - - True - True - False - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - - - - - - - Matita: script GTK_WINDOW_TOPLEVEL @@ -1882,140 +1805,177 @@ Copyright (C) 2004, False - + True - True - True - True - GTK_POS_BOTTOM - False - False + False + 0 - + True - False - 0 + GTK_SHADOW_OUT + GTK_POS_LEFT + GTK_POS_TOP - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + False + 0 - + True - True - True - False + restart + True + GTK_RELIEF_NORMAL + True - + True - go back 1 phrase - True - GTK_RELIEF_NORMAL - True - - - - True - gtk-go-back - 4 - 0.5 - 0.5 - 0 - 0 - - + gtk-goto-top + 4 + 0.5 + 0.5 + 0 + 0 + 0 False - False + False - + True - True - True - False + go back 1 phrase + True + GTK_RELIEF_NORMAL + True - + True - execute til cursor - True - GTK_RELIEF_NORMAL - True + gtk-undo + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + - - - True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 - - + + + True + execute until point + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + 0 False - False + False - + True - True - True - False + go forward 1 phrase + True + GTK_RELIEF_NORMAL + True - + True - go forward 1 phrase - True - GTK_RELIEF_NORMAL - True + gtk-redo + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + - - - True - gtk-go-forward - 4 - 0.5 - 0.5 - 0 - 0 - - + + + True + execute all + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-goto-bottom + 4 + 0.5 + 0.5 + 0 + 0 + 0 False - False + False - - 0 - False - False - + + + 0 + False + True + + + + + + True + True + True + True + GTK_POS_BOTTOM + False + False @@ -2047,79 +2007,79 @@ Copyright (C) 2004, - 0 - True - True + False + True - - - False - True - - - - - True - script - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - tab - - - - - - True - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT + + + True + script + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + - + True True - False - False - False - True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + False + True + - - - False - True - - - - - True - outline - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + + + True + outline + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + - tab + 0 + True + True @@ -2276,228 +2236,243 @@ Copyright (C) 2004, 0 - + True - False - 0 + GTK_SHADOW_OUT + GTK_POS_LEFT + GTK_POS_TOP - + True - True - True - GTK_RELIEF_NORMAL - True + False + 0 - + True - gtk-new - 4 - 0.5 - 0.5 - 0 - 0 + new browser win + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-new + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - - 0 - False - False - - - - - - True - True - True - GTK_RELIEF_NORMAL - True - + True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 + history back + True + True + GTK_RELIEF_NORMAL + True - + True - False - 2 + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 - + True - gtk-go-back - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - + False + 2 - - - True - - True - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + + + True + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + - - 0 - False - False - + + 0 + False + False + - - - 0 - False - False - - - - - - True - True - True - GTK_RELIEF_NORMAL - True - + True - gtk-go-forward - 4 - 0.5 - 0.5 - 0 - 0 + history forward + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - - 0 - False - False - - - - - - True - True - True - GTK_RELIEF_NORMAL - True - + True - gtk-refresh - 4 - 0.5 - 0.5 - 0 - 0 + refresh + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-refresh + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - - 0 - False - False - - - - - True - True - True - GTK_RELIEF_NORMAL - True + + + True + home + True + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-home + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + - + True - gtk-home + gtk-jump-to 4 0.5 0.5 0 0 + + 0 + False + True + - - - 0 - False - False - - - - - - True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - True - - - - - True - True - True - True - 0 - - True - * - False + + + True + cic uri + True + True + True + 0 + + True + * + False + + + 0 + True + True + + - - 0 - True - True - diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 6e57c2e8f..40f2077cf 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -51,8 +51,7 @@ let disambiguator = ~chooseInterp:(interactive_interp_choice ~gui) () -let currentProof = new MatitaProof.currentProof - +let currentProof = MatitaProof.instance () let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () let sequents_viewer = let set_goal goal = @@ -83,15 +82,10 @@ let _ = (* attach observers to proof status *) false); currentProof#connect `Abort (fun () -> sequents_viewer#reset; false) -let currentProof = (currentProof :> MatitaTypes.currentProof) -let mathViewer = - MatitaMathView.mathViewer ~disambiguator - ~currentProof:(currentProof :> MatitaTypes.currentProof) () +let mathViewer = MatitaMathView.mathViewer ~disambiguator () let interpreter = - let console = (gui#console :> MatitaTypes.console) in - new MatitaInterpreter.interpreter - ~disambiguator ~currentProof:(currentProof :> MatitaTypes.currentProof) - ~console ~mathViewer ~dbd () + let console = gui#console in + MatitaInterpreter.interpreter ~disambiguator ~console ~mathViewer () let _ = let href_callback uri = let term = CicAst.Uri (UriManager.string_of_uri uri, None) in @@ -159,8 +153,7 @@ let _ = "Don't know what to do with file: %s\nUnrecognized file format." f))); ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ -> - let currentProof = (currentProof :> MatitaTypes.currentProof) in - ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ()))); + ignore (MatitaMathView.cicBrowser ~disambiguator ()))); connect_button gui#script#scriptWinForwardButton script_forward; connect_button gui#script#scriptWinBackButton script_back; connect_button gui#script#scriptWinJumpButton script_jump; @@ -226,9 +219,14 @@ let _ = load_script Sys.argv.(1) with Invalid_argument _ -> ()); *) - if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin - ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ()) - end else begin + if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin (* cicbrowser *) + let browser = MatitaMathView.cicBrowser ~disambiguator () in + Helm_registry.set "matita.mode" "cicbrowser"; + try + browser#loadUri Sys.argv.(1) + with Invalid_argument _ -> () + end else begin (* matita *) + Helm_registry.set "matita.mode" "matita"; gui#main#mainWin#show (); gui#toolbar#toolBarWin#show (); gui#console#show () diff --git a/helm/matita/matitaCicMisc.ml b/helm/matita/matitaCicMisc.ml index e6cda3024..dbb80c791 100644 --- a/helm/matita/matitaCicMisc.ml +++ b/helm/matita/matitaCicMisc.ml @@ -60,7 +60,7 @@ let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~currentProof ast = end else disambiguator#disambiguateTermAst ast -let get_context_and_metasenv ~(currentProof:MatitaTypes.currentProof) = +let get_context_and_metasenv ~(currentProof:#MatitaTypes.currentProof) = if currentProof#onGoing () then let proof = currentProof#proof in let metasenv = proof#metasenv in diff --git a/helm/matita/matitaCicMisc.mli b/helm/matita/matitaCicMisc.mli index 61111aaf1..3d0de435f 100644 --- a/helm/matita/matitaCicMisc.mli +++ b/helm/matita/matitaCicMisc.mli @@ -37,12 +37,12 @@ val canonical_context: int -> (int * 'a * 'b) list -> 'a * metasenv as needed *) val disambiguate : disambiguator:MatitaTypes.disambiguator -> - currentProof:MatitaTypes.currentProof -> + currentProof:#MatitaTypes.currentProof -> DisambiguateTypes.term -> DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph val get_context_and_metasenv: - currentProof:MatitaTypes.currentProof -> + currentProof:#MatitaTypes.currentProof -> Cic.context * Cic.metasenv diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index b192fd732..11d5dcb9e 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -185,31 +185,6 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = toplevel#destroy () method check_widgets () = () end -class proofWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"ProofWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val proofWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata)) - method proofWin = proofWin - val proofWinEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"ProofWinEventBox" ~info:"GtkEventBox" xmldata)) - method proofWinEventBox = proofWinEventBox - val scrolledProof = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledProof" ~info:"GtkScrolledWindow" xmldata)) - method scrolledProof = scrolledProof - method reparent parent = - proofWinEventBox#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = let xmldata = Glade.create ~file ~root:"FileSelectionWin" ?domain () in object (self) @@ -622,31 +597,6 @@ class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = toplevel#destroy () method check_widgets () = () end -class checkWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"CheckWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val checkWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata)) - method checkWin = checkWin - val checkWinEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"CheckWinEventBox" ~info:"GtkEventBox" xmldata)) - method checkWinEventBox = checkWinEventBox - val scrolledCheck = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledCheck" ~info:"GtkScrolledWindow" xmldata)) - method scrolledCheck = scrolledCheck - method reparent parent = - checkWinEventBox#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = let xmldata = Glade.create ~file ~root:"ScriptWin" ?domain () in object (self) @@ -663,18 +613,26 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.event_box (GtkBin.EventBox.cast (Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata)) method scriptWinEventBox = scriptWinEventBox - val scriptNotebook = - new GPack.notebook (GtkPack.Notebook.cast - (Glade.get_widget_msg ~name:"scriptNotebook" ~info:"GtkNotebook" xmldata)) - method scriptNotebook = scriptNotebook - val vbox4 = + val vbox7 = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox4" ~info:"GtkVBox" xmldata)) - method vbox4 = vbox4 - val toolbar1 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar1" ~info:"GtkToolbar" xmldata)) - method toolbar1 = toolbar1 + (Glade.get_widget_msg ~name:"vbox7" ~info:"GtkVBox" xmldata)) + method vbox7 = vbox7 + val handlebox2 = + new GBin.handle_box (GtkBin.HandleBox.cast + (Glade.get_widget_msg ~name:"handlebox2" ~info:"GtkHandleBox" xmldata)) + method handlebox2 = handlebox2 + val hbox8 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"hbox8" ~info:"GtkHBox" xmldata)) + method hbox8 = hbox8 + val scriptWinTopButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"ScriptWinTopButton" ~info:"GtkButton" xmldata)) + method scriptWinTopButton = scriptWinTopButton + val image235 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image235" ~info:"GtkImage" xmldata)) + method image235 = image235 val scriptWinBackButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata)) @@ -699,6 +657,18 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMisc.image (GtkMisc.Image.cast (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata)) method image135 = image135 + val scriptWinBottomButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"ScriptWinBottomButton" ~info:"GtkButton" xmldata)) + method scriptWinBottomButton = scriptWinBottomButton + val image236 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image236" ~info:"GtkImage" xmldata)) + method image236 = image236 + val scriptNotebook = + new GPack.notebook (GtkPack.Notebook.cast + (Glade.get_widget_msg ~name:"ScriptNotebook" ~info:"GtkNotebook" xmldata)) + method scriptNotebook = scriptNotebook val scrolledScript = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (Glade.get_widget_msg ~name:"ScrolledScript" ~info:"GtkScrolledWindow" xmldata)) @@ -711,10 +681,10 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMisc.label (GtkMisc.Label.cast (Glade.get_widget_msg ~name:"label7" ~info:"GtkLabel" xmldata)) method label7 = label7 - val scrolledwindow3 = + val scrolledOutline = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"scrolledwindow3" ~info:"GtkScrolledWindow" xmldata)) - method scrolledwindow3 = scrolledwindow3 + (Glade.get_widget_msg ~name:"ScrolledOutline" ~info:"GtkScrolledWindow" xmldata)) + method scrolledOutline = scrolledOutline val treeview1 = new GTree.view (GtkTree.TreeView.cast (Glade.get_widget_msg ~name:"treeview1" ~info:"GtkTreeView" xmldata)) @@ -793,6 +763,10 @@ class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata)) method browserVBox = browserVBox + val handlebox1 = + new GBin.handle_box (GtkBin.HandleBox.cast + (Glade.get_widget_msg ~name:"handlebox1" ~info:"GtkHandleBox" xmldata)) + method handlebox1 = handlebox1 val hbox7 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata)) @@ -882,9 +856,6 @@ let check_all ?(show=false) () = let scriptWin = new scriptWin () in if show then scriptWin#toplevel#show (); scriptWin#check_widgets (); - let checkWin = new checkWin () in - if show then checkWin#toplevel#show (); - checkWin#check_widgets (); let emptyDialog = new emptyDialog () in if show then emptyDialog#toplevel#show (); emptyDialog#check_widgets (); @@ -906,9 +877,6 @@ let check_all ?(show=false) () = let fileSelectionWin = new fileSelectionWin () in if show then fileSelectionWin#toplevel#show (); fileSelectionWin#check_widgets (); - let proofWin = new proofWin () in - if show then proofWin#toplevel#show (); - proofWin#check_widgets (); let mainWin = new mainWin () in if show then mainWin#toplevel#show (); mainWin#check_widgets (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 26b487b88..8fb25564d 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -98,26 +98,6 @@ class mainWin : method viewMenu_menu : GMenu.menu method xml : Glade.glade_xml Gtk.obj end -class proofWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val proofWin : GWindow.window - val proofWinEventBox : GBin.event_box - val scrolledProof : GBin.scrolled_window - val toplevel : GWindow.window - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method proofWin : GWindow.window - method proofWinEventBox : GBin.event_box - method reparent : GObj.widget -> unit - method scrolledProof : GBin.scrolled_window - method toplevel : GWindow.window - method xml : Glade.glade_xml Gtk.obj - end class fileSelectionWin : ?file:string -> ?domain:string -> @@ -377,56 +357,45 @@ class emptyDialog : method toplevel : GWindow.dialog_any method xml : Glade.glade_xml Gtk.obj end -class checkWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val checkWin : GWindow.window - val checkWinEventBox : GBin.event_box - val scrolledCheck : GBin.scrolled_window - val toplevel : GWindow.window - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method checkWin : GWindow.window - method checkWinEventBox : GBin.event_box - method check_widgets : unit -> unit - method reparent : GObj.widget -> unit - method scrolledCheck : GBin.scrolled_window - method toplevel : GWindow.window - method xml : Glade.glade_xml Gtk.obj - end class scriptWin : ?file:string -> ?domain:string -> ?autoconnect:bool -> unit -> object + val handlebox2 : GBin.handle_box + val hbox8 : GPack.box val image133 : GMisc.image val image134 : GMisc.image val image135 : GMisc.image + val image235 : GMisc.image + val image236 : GMisc.image val label7 : GMisc.label val label8 : GMisc.label val scriptNotebook : GPack.notebook val scriptTextView : GText.view val scriptWin : GWindow.window val scriptWinBackButton : GButton.button + val scriptWinBottomButton : GButton.button val scriptWinEventBox : GBin.event_box val scriptWinForwardButton : GButton.button val scriptWinJumpButton : GButton.button + val scriptWinTopButton : GButton.button + val scrolledOutline : GBin.scrolled_window val scrolledScript : GBin.scrolled_window - val scrolledwindow3 : GBin.scrolled_window - val toolbar1 : GButton.toolbar val toplevel : GWindow.window val treeview1 : GTree.view - val vbox4 : GPack.box + val vbox7 : GPack.box val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit + method handlebox2 : GBin.handle_box + method hbox8 : GPack.box method image133 : GMisc.image method image134 : GMisc.image method image135 : GMisc.image + method image235 : GMisc.image + method image236 : GMisc.image method label7 : GMisc.label method label8 : GMisc.label method reparent : GObj.widget -> unit @@ -434,15 +403,16 @@ class scriptWin : method scriptTextView : GText.view method scriptWin : GWindow.window method scriptWinBackButton : GButton.button + method scriptWinBottomButton : GButton.button method scriptWinEventBox : GBin.event_box method scriptWinForwardButton : GButton.button method scriptWinJumpButton : GButton.button + method scriptWinTopButton : GButton.button + method scrolledOutline : GBin.scrolled_window method scrolledScript : GBin.scrolled_window - method scrolledwindow3 : GBin.scrolled_window - method toolbar1 : GButton.toolbar method toplevel : GWindow.window method treeview1 : GTree.view - method vbox4 : GPack.box + method vbox7 : GPack.box method xml : Glade.glade_xml Gtk.obj end class textDialog : @@ -492,6 +462,7 @@ class browserWin : val browserWin : GWindow.window val browserWinEventBox : GBin.event_box val frame1 : GBin.frame + val handlebox1 : GBin.handle_box val hbox6 : GPack.box val hbox7 : GPack.box val image187 : GMisc.image @@ -517,6 +488,7 @@ class browserWin : method browserWinEventBox : GBin.event_box method check_widgets : unit -> unit method frame1 : GBin.frame + method handlebox1 : GBin.handle_box method hbox6 : GPack.box method hbox7 : GPack.box method image187 : GMisc.image diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index fef22143a..04d52cd9e 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -35,12 +35,10 @@ class gui file = let main = new mainWin ~file () in let about = new aboutWin ~file () in let fileSel = new fileSelectionWin ~file () in - let proof = new proofWin ~file () in - let check = new checkWin ~file () in let script = new scriptWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) - [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox; - check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox ] + [ toolbar#toolBarEventBox; main#mainWinEventBox; + script#scriptWinEventBox; main#consoleEventBox ] in let console = MatitaConsole.console ~evbox:main#consoleEventBox @@ -62,7 +60,7 @@ class gui file = (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in - [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]); + [ c about; c fileSel; c main; c toolbar; c script ]); (* key bindings *) List.iter (* global key bindings *) (fun (key, callback) -> self#addKeyBinding key callback) @@ -121,11 +119,9 @@ class gui file = console#misc#grab_focus (); method about = about - method check = check method console = console method fileSel = fileSel method main = main - method proof = proof method script = script method toolbar = toolbar diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 1d3f1220b..acc244aa9 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -34,10 +34,8 @@ class gui : (** {2 Access to singleton instances of lower-level GTK widgets} *) method about : MatitaGeneratedGui.aboutWin - method check : MatitaGeneratedGui.checkWin method fileSel : MatitaGeneratedGui.fileSelectionWin method main : MatitaGeneratedGui.mainWin - method proof : MatitaGeneratedGui.proofWin method script: MatitaGeneratedGui.scriptWin method toolbar : MatitaGeneratedGui.toolBarWin diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 78d30c4cd..640b7406e 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -64,9 +64,12 @@ class virtual interpreterState = (* static values, shared by all states inheriting this class *) let loc = ref None in let history = ref [] in - fun ~(console: MatitaTypes.console) -> + fun ~(console: #MatitaTypes.console) -> object (self) + val dbd = MatitaMisc.dbd_instance () + val currentProof = MatitaProof.instance () + (** eval a toplevel phrase in the current state and return the new state *) method parsePhrase s = @@ -103,10 +106,8 @@ class virtual interpreterState = (** Implements phrases that should be accepted in all states *) class sharedState ~(disambiguator: MatitaTypes.disambiguator) - ~(currentProof: MatitaTypes.currentProof) - ~(console: MatitaTypes.console) + ~(console: #MatitaTypes.console) ?(mathViewer: MatitaTypes.mathViewer option) - ~(dbd: Mysql.dbd) () = object (self) @@ -307,7 +308,7 @@ let * - save object to disk in xml format * - register uri to the getter * - save universe file *) -let add_constant_to_world ~(console:MatitaTypes.console) +let add_constant_to_world ~(console: #MatitaTypes.console) ~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph () = let suri = UriManager.string_of_uri uri in @@ -324,7 +325,7 @@ let add_constant_to_world ~(console:MatitaTypes.console) console#echo_message (sprintf "%s constant defined" suri) end -let add_inductive_def_to_world ~(console:MatitaTypes.console) +let add_inductive_def_to_world ~(console: #MatitaTypes.console) ~dbd ~uri ~indTypes ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph () = let suri = UriManager.string_of_uri uri in @@ -360,15 +361,11 @@ let add_inductive_def_to_world ~(console:MatitaTypes.console) (** Implements phrases that should be accepted only in Command state *) class commandState ~(disambiguator: MatitaTypes.disambiguator) - ~(currentProof: MatitaTypes.currentProof) - ~(console: MatitaTypes.console) + ~(console: #MatitaTypes.console) ?mathViewer - ~(dbd: Mysql.dbd) () = - let shared = - new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () - in + let shared = new sharedState ~disambiguator ~console ?mathViewer () in object (self) inherit interpreterState ~console @@ -519,67 +516,64 @@ let namer_of names = * tacticals *) class proofState ~(disambiguator: MatitaTypes.disambiguator) - ~(currentProof: MatitaTypes.currentProof) - ~(console: MatitaTypes.console) + ~(console: #MatitaTypes.console) ?mathViewer - ~(dbd: Mysql.dbd) () = - let disambiguate ast = - let (_, _, term, _) = - MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast - in - term - in - (** tactic AST -> ProofEngineTypes.tactic *) - let rec lookup_tactic = function - | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic - | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *) - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.Reflexivity -> Tactics.reflexivity - | TacticAst.Assumption -> Tactics.assumption - | TacticAst.Contradiction -> Tactics.contradiction - | TacticAst.Exists -> Tactics.exists - | TacticAst.Fourier -> Tactics.fourier - | TacticAst.Left -> Tactics.left - | TacticAst.Right -> Tactics.right - | TacticAst.Ring -> Tactics.ring - | TacticAst.Split -> Tactics.split - | TacticAst.Symmetry -> Tactics.symmetry - | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term) - | TacticAst.Apply term -> Tactics.apply (disambiguate term) - | TacticAst.Absurd term -> Tactics.absurd (disambiguate term) - | TacticAst.Exact term -> Tactics.exact (disambiguate term) - | TacticAst.Cut term -> Tactics.cut (disambiguate term) - | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *) - Tactics.elim_intros_simpl (disambiguate term) - | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term) - | TacticAst.Replace (what, with_what) -> - Tactics.replace ~what:(disambiguate what) - ~with_what:(disambiguate with_what) - | TacticAst.Auto -> Tactics.auto_new ~dbd - (* - (* TODO Zack a lot more of tactics to be implemented here ... *) - | TacticAst.Change of 'term * 'term * 'ident option - | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option - | TacticAst.Decompose of 'ident * 'ident list - | TacticAst.Discriminate of 'ident - | TacticAst.Fold of reduction_kind * 'term - | TacticAst.Injection of 'ident - | TacticAst.LetIn of 'term * 'ident - | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option - | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option - *) - | _ -> - MatitaTypes.not_implemented "some tactic" - in - let shared = - new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () - in + let shared = new sharedState ~disambiguator ~console ?mathViewer () in object (self) inherit interpreterState ~console + method private disambiguate ast = + let (_, _, term, _) = + MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast + in + term + + (** tactic AST -> ProofEngineTypes.tactic *) + method private lookup_tactic = function + | TacticAst.LocatedTactic (_, tactic) -> self#lookup_tactic tactic + | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *) + PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) + () + | TacticAst.Reflexivity -> Tactics.reflexivity + | TacticAst.Assumption -> Tactics.assumption + | TacticAst.Contradiction -> Tactics.contradiction + | TacticAst.Exists -> Tactics.exists + | TacticAst.Fourier -> Tactics.fourier + | TacticAst.Left -> Tactics.left + | TacticAst.Right -> Tactics.right + | TacticAst.Ring -> Tactics.ring + | TacticAst.Split -> Tactics.split + | TacticAst.Symmetry -> Tactics.symmetry + | TacticAst.Transitivity term -> + Tactics.transitivity (self#disambiguate term) + | TacticAst.Apply term -> Tactics.apply (self#disambiguate term) + | TacticAst.Absurd term -> Tactics.absurd (self#disambiguate term) + | TacticAst.Exact term -> Tactics.exact (self#disambiguate term) + | TacticAst.Cut term -> Tactics.cut (self#disambiguate term) + | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *) + Tactics.elim_intros_simpl (self#disambiguate term) + | TacticAst.ElimType term -> Tactics.elim_type (self#disambiguate term) + | TacticAst.Replace (what, with_what) -> + Tactics.replace ~what:(self#disambiguate what) + ~with_what:(self#disambiguate with_what) + | TacticAst.Auto -> Tactics.auto_new ~dbd + (* + (* TODO Zack a lot more of tactics to be implemented here ... *) + | TacticAst.Change of 'term * 'term * 'ident option + | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option + | TacticAst.Decompose of 'ident * 'ident list + | TacticAst.Discriminate of 'ident + | TacticAst.Fold of reduction_kind * 'term + | TacticAst.Injection of 'ident + | TacticAst.LetIn of 'term * 'ident + | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option + | TacticAst.Replace_pattern of 'term pattern * 'term + | TacticAst.Rewrite of direction * 'term * 'ident option + *) + | _ -> MatitaTypes.not_implemented "some tactic" + method evalTactical = function | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical | TacticAst.Command TacticAst.Abort -> @@ -616,7 +610,7 @@ class proofState List.iter (fun t -> ignore (self#evalTactical t)) tacticals; New_state Proof | TacticAst.Tactic tactic_phrase -> - let tactic = lookup_tactic tactic_phrase in + let tactic = self#lookup_tactic tactic_phrase in currentProof#proof#apply_tactic tactic; New_state Proof | tactical -> shared#evalTactical tactical @@ -624,18 +618,12 @@ class proofState class interpreter ~(disambiguator: MatitaTypes.disambiguator) - ~(currentProof: MatitaTypes.currentProof) - ~(console: MatitaTypes.console) + ~(console: #MatitaTypes.console) ?mathViewer - ~(dbd: Mysql.dbd) () = - let commandState = - new commandState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () - in - let proofState = - new proofState ~disambiguator ~currentProof ~console ?mathViewer ~dbd () - in + let commandState = new commandState ~disambiguator ~console ?mathViewer () in + let proofState = new proofState ~disambiguator ~console ?mathViewer () in object (self) val mutable state = commandState @@ -661,3 +649,11 @@ class interpreter method evalAst ast = self#eval (fun () -> state#evalAst ast) end +let interpreter + ~(disambiguator: MatitaTypes.disambiguator) + ~(console: #MatitaTypes.console) + ?mathViewer + () += + new interpreter ~disambiguator ~console ?mathViewer () + diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli index 7886a564a..2b0ad56da 100644 --- a/helm/matita/matitaInterpreter.mli +++ b/helm/matita/matitaInterpreter.mli @@ -25,12 +25,10 @@ exception Command_error of string -class interpreter: +val interpreter: disambiguator:MatitaTypes.disambiguator -> - currentProof:MatitaTypes.currentProof -> - console:MatitaTypes.console -> + console:#MatitaTypes.console -> ?mathViewer:MatitaTypes.mathViewer -> - dbd:Mysql.dbd -> unit -> MatitaTypes.interpreter diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 7bf464a9d..626e45634 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -267,7 +267,6 @@ let cicBrowsers = ref [] class cicBrowser ~(disambiguator:MatitaTypes.disambiguator) - ~(currentProof:MatitaTypes.currentProof) ~(history:string MatitaMisc.history) () = @@ -286,24 +285,33 @@ class cicBrowser with exn -> fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn)) in + let handle_error' f = fun () -> handle_error f in (* used in callbacks *) object (self) initializer - ignore (win#browserUri#connect#activate (fun () -> - self#_loadUri win#browserUri#text)); - ignore (win#browserHomeButton#connect#clicked (fun () -> - self#_loadUri current_proof_uri)); - ignore (win#browserRefreshButton#connect#clicked self#refresh); - ignore (win#browserBackButton#connect#clicked self#back); - ignore (win#browserForwardButton#connect#clicked self#forward); + ignore (win#browserUri#connect#activate (handle_error' (fun () -> + self#_loadUri win#browserUri#text))); + ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> + self#_loadUri current_proof_uri))); + ignore (win#browserRefreshButton#connect#clicked + (handle_error' self#refresh)); + ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); + ignore (win#browserForwardButton#connect#clicked + (handle_error' self#forward)); ignore (win#toplevel#event#connect#delete (fun _ -> let my_id = Oo.id self in cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; + if !cicBrowsers = [] && + Helm_registry.get "matita.mode" = "cicbrowser" + then + GMain.quit (); false)); mathView#set_href_callback (Some (fun uri -> handle_error (fun () -> self#_loadUri (UriManager.string_of_uri uri)))); self#_loadUri ~add_to_history:false blank_uri; toplevel#show (); + val currentProof = MatitaProof.instance () + val mutable current_uri = "" val mutable current_infos = None val mutable current_mathml = None @@ -418,10 +426,10 @@ let sequents_viewer ~(notebook:GPack.notebook) = new sequents_viewer ~notebook ~sequent_viewer ~set_goal () -let cicBrowser ~disambiguator ~currentProof () = +let cicBrowser ~disambiguator () = let size = BuildTimeConf.browser_history_size in let rec aux history = - let browser = new cicBrowser ~disambiguator ~currentProof ~history () in + let browser = new cicBrowser ~disambiguator ~history () in let win = browser#win in ignore (win#browserNewButton#connect#clicked (fun () -> let history = @@ -442,13 +450,12 @@ let cicBrowser ~disambiguator ~currentProof () = let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers -class mathViewer ~disambiguator ~currentProof = +class mathViewer ~disambiguator = object method checkTerm (src:MatitaTypes.term_source) = - let browser = cicBrowser ~disambiguator ~currentProof () in + let browser = cicBrowser ~disambiguator () in browser#loadTerm src end -let mathViewer ~disambiguator ~currentProof () = - new mathViewer ~disambiguator ~currentProof +let mathViewer ~disambiguator () = new mathViewer ~disambiguator diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index de8edc855..cdc9a8d65 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -85,7 +85,6 @@ val sequents_viewer: val cicBrowser: disambiguator:MatitaTypes.disambiguator -> - currentProof:MatitaTypes.currentProof -> unit -> MatitaTypes.cicBrowser @@ -93,7 +92,6 @@ val refresh_all_browsers: unit -> unit val mathViewer: disambiguator:MatitaTypes.disambiguator -> - currentProof:MatitaTypes.currentProof -> unit -> MatitaTypes.mathViewer diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index c3b83fd47..dd84abcbd 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -130,3 +130,13 @@ class ['a] browser_history ?memento size init = method save = (Array.copy data, hd, tl, cur) end +let dbd_instance = + let dbd = lazy ( + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + ()) + in + fun () -> Lazy.force dbd + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index afaa631a0..36318dc1f 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -66,3 +66,6 @@ class shell_history : int -> [string] history * @param first element in history (this history is never empty) *) class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history + (** {2 db handling} *) +val dbd_instance: unit -> Mysql.dbd + diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index 54ebdf6cf..9afb90a71 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -151,4 +151,7 @@ let proof ?uri ~metasenv ~typ () = new proof ~typ ~metasenv ~body ?uri () let currentProof () = new currentProof +let instance = + let currentProof = lazy (currentProof ()) in + fun () -> Lazy.force currentProof diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli index 566777fc1..9ed622191 100644 --- a/helm/matita/matitaProof.mli +++ b/helm/matita/matitaProof.mli @@ -36,7 +36,7 @@ val proof: MatitaTypes.proof (** current proof handler *) -class currentProof: +class type currentProof = object inherit MatitaTypes.currentProof @@ -52,3 +52,8 @@ class currentProof: method connect: [`Abort|`Quit] -> (unit -> bool) -> unit end +val currentProof: unit -> currentProof + + (** currentProof singleton instance *) +val instance: unit -> currentProof + diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index bb796db1e..87c30cfea 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -78,10 +78,7 @@ let disambiguator = ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback () let console = new tty_console -let currentProof = (new MatitaProof.currentProof :> MatitaTypes.currentProof) -let interpreter = - new MatitaInterpreter.interpreter - ~disambiguator ~currentProof ~console ~dbd () +let interpreter = MatitaInterpreter.interpreter ~disambiguator ~console () let run_script fname = message (sprintf "execution of %s started:" fname);