From: Stefano Zacchiroli Date: Fri, 4 Feb 2005 11:10:52 +0000 (+0000) Subject: snapshot, notably: X-Git-Tag: V_0_1_0~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6187b40af194fb960d91653682a0eb2096f20f3b;p=helm.git snapshot, notably: - even more singleton instances: disambiguator is now common to matita and matitac, but matita set different callbacks which uses gtk - getter now embedded in matita (no longer use remote getter) - use onwerization of tables --- diff --git a/helm/matita/.depend b/helm/matita/.depend index 18f464afd..483301181 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,54 +1,56 @@ -matita.cmo: buildTimeConf.cmo matitaDb.cmi matitaDisambiguator.cmi \ - matitaGtkMisc.cmi matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi \ - matitaMisc.cmi matitaProof.cmi matitaTypes.cmi -matita.cmx: buildTimeConf.cmx matitaDb.cmx matitaDisambiguator.cmx \ - matitaGtkMisc.cmx matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx \ - matitaMisc.cmx matitaProof.cmx matitaTypes.cmx matitaCicMisc.cmo: matitaTypes.cmi matitaCicMisc.cmi matitaCicMisc.cmx: matitaTypes.cmx matitaCicMisc.cmi -matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaMisc.cmi \ - matitaTypes.cmi matitaConsole.cmi -matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaMisc.cmx \ - matitaTypes.cmx matitaConsole.cmi -matitaDb.cmo: matitaDb.cmi -matitaDb.cmx: matitaDb.cmi -matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi -matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi +matitac.cmo: matitaTypes.cmi matitaMisc.cmi matitaInterpreter.cmi \ + buildTimeConf.cmo +matitac.cmx: matitaTypes.cmx matitaMisc.cmx matitaInterpreter.cmx \ + buildTimeConf.cmx +matitaConsole.cmo: matitaTypes.cmi matitaMisc.cmi matitaGtkMisc.cmi \ + buildTimeConf.cmo matitaConsole.cmi +matitaConsole.cmx: matitaTypes.cmx matitaMisc.cmx matitaGtkMisc.cmx \ + buildTimeConf.cmx matitaConsole.cmi +matitaDb.cmo: matitaMisc.cmi matitaDb.cmi +matitaDb.cmx: matitaMisc.cmx matitaDb.cmi +matitaDisambiguator.cmo: matitaTypes.cmi matitaMisc.cmi \ + matitaDisambiguator.cmi +matitaDisambiguator.cmx: matitaTypes.cmx matitaMisc.cmx \ + matitaDisambiguator.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi -matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmi matitaGtkMisc.cmi -matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi -matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \ - matitaGtkMisc.cmi matitaMisc.cmi matitaGui.cmi -matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \ - matitaGtkMisc.cmx matitaMisc.cmx matitaGui.cmi -matitaInterpreter.cmo: matitaCicMisc.cmi matitaMisc.cmi matitaProof.cmi \ - matitaTypes.cmi matitaInterpreter.cmi -matitaInterpreter.cmx: matitaCicMisc.cmx matitaMisc.cmx matitaProof.cmx \ - matitaTypes.cmx matitaInterpreter.cmi -matitaMathView.cmo: buildTimeConf.cmo matitaCicMisc.cmi matitaGtkMisc.cmi \ - matitaGui.cmi matitaMisc.cmi matitaProof.cmi matitaTypes.cmi \ - matitaMathView.cmi -matitaMathView.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaGtkMisc.cmx \ - matitaGui.cmx matitaMisc.cmx matitaProof.cmx matitaTypes.cmx \ - matitaMathView.cmi +matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi +matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi +matitaGui.cmo: matitaMisc.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi \ + matitaConsole.cmi buildTimeConf.cmo matitaGui.cmi +matitaGui.cmx: matitaMisc.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ + matitaConsole.cmx buildTimeConf.cmx matitaGui.cmi +matitaInterpreter.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi \ + matitaDisambiguator.cmi matitaCicMisc.cmi matitaInterpreter.cmi +matitaInterpreter.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx \ + matitaDisambiguator.cmx matitaCicMisc.cmx matitaInterpreter.cmi +matitaMathView.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi \ + matitaGui.cmi matitaGtkMisc.cmi matitaDisambiguator.cmi matitaCicMisc.cmi \ + buildTimeConf.cmo matitaMathView.cmi +matitaMathView.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx \ + matitaGui.cmx matitaGtkMisc.cmx matitaDisambiguator.cmx matitaCicMisc.cmx \ + buildTimeConf.cmx matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi -matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmi matitaTypes.cmi \ - matitaProof.cmi -matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \ - matitaProof.cmi +matita.cmo: matitaTypes.cmi matitaProof.cmi matitaMisc.cmi matitaMathView.cmi \ + matitaInterpreter.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaProof.cmx matitaMisc.cmx matitaMathView.cmx \ + matitaInterpreter.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx +matitaProof.cmo: matitaTypes.cmi matitaMisc.cmi matitaCicMisc.cmi \ + buildTimeConf.cmo matitaProof.cmi +matitaProof.cmx: matitaTypes.cmx matitaMisc.cmx matitaCicMisc.cmx \ + buildTimeConf.cmx matitaProof.cmi matitaTypes.cmo: buildTimeConf.cmo matitaTypes.cmi matitaTypes.cmx: buildTimeConf.cmx matitaTypes.cmi -matitac.cmo: buildTimeConf.cmo matitaDb.cmi matitaDisambiguator.cmi \ - matitaInterpreter.cmi matitaTypes.cmi -matitac.cmx: buildTimeConf.cmx matitaDb.cmx matitaDisambiguator.cmx \ - matitaInterpreter.cmx matitaTypes.cmx matitaCicMisc.cmi: matitaTypes.cmi matitaConsole.cmi: matitaTypes.cmi matitaDisambiguator.cmi: matitaTypes.cmi -matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmi -matitaGui.cmi: matitaConsole.cmi matitaGeneratedGui.cmi matitaTypes.cmi +matitaGtkMisc.cmi: matitaTypes.cmi matitaGeneratedGui.cmi +matitaGui.cmi: matitaTypes.cmi matitaGeneratedGui.cmi matitaConsole.cmi matitaInterpreter.cmi: matitaTypes.cmi matitaMathView.cmi: matitaTypes.cmi matitaProof.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index aadfd26ad..0ca62ff70 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -19,6 +19,7 @@ OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) CMOS = \ buildTimeConf.cmo \ matitaMisc.cmo \ + matitaDb.cmo \ matitaGeneratedGui.cmo \ matitaTypes.cmo \ matitaCicMisc.cmo \ @@ -33,6 +34,7 @@ CMOS = \ CCMOS = \ buildTimeConf.cmo \ matitaMisc.cmo \ + matitaDb.cmo \ matitaTypes.cmo \ matitaCicMisc.cmo \ matitaProof.cmo \ @@ -54,10 +56,8 @@ opt: endif matita: $(LIB_DEPS) $(CMOS) matita.ml - rm -f cicbrowser $(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml - rm -f cicbrowser.opt $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml matitac: $(LIB_DEPS) $(CCMOS) matitac.ml @@ -66,9 +66,9 @@ matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml cicbrowser: matita - test -f $@ || ln -s $< $@ + @test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt - test -f $@ || ln -s $< $@ + @test -f $@ || ln -s $< $@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade $(LABLGLADECC) $< > matitaGeneratedGui.ml diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index 9035d2a78..61ab2d8d6 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -1,22 +1,27 @@ -
- mowgli.cs.unibo.it - -
matita.glade true + true + cic:/matita/ + .matita/xml zack
- $(prefs.server) + + mowgli.cs.unibo.it helm - mowgli - + + matita
- remote - http://$(prefs.server):58081/ + + file:///projects/helm/library/coq_contribs + + .matita/getter/cache + .matita/getter/maps + /projects/helm/xml/dtd +
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 728a87112..74a68bee4 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -3,13 +3,89 @@ - - Matita + + Matita: about + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + <b>Matita @VERSION@</b> + +<tt>http://helm.cs.unibo.it</tt> + +Copyright (C) 2004, +<i>the HELM team</i> + False + True + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 5 + 5 + + + 0 + False + False + + + + + + + + 400 + 500 + True + Cic browser GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE False - 800 - 600 True False True @@ -19,264 +95,253 @@ GDK_GRAVITY_NORTH_WEST - + True True False - + True False 0 - + True + GTK_SHADOW_OUT + GTK_POS_LEFT + GTK_POS_TOP - + True - _File - True + False + 0 - + + True + new browser win + True + True + GTK_RELIEF_NORMAL + True - + True - _New - True + gtk-new + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + - - - True - gtk-new - 1 - 0.5 - 0.5 - 0 - 0 - - + + + True + history back + True + True + GTK_RELIEF_NORMAL + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 - + + True + False + 2 - + True - _Proof or definition ... - True + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + 0 + False + False + - + True - (Co)Inductive _definitions ... + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + 0 + False + False + + + + 0 + False + False + + + + + + True + history forward + True + True + GTK_RELIEF_NORMAL + True - + True - _Open... - True - - - - - True - gtk-open - 1 - 0.5 - 0.5 - 0 - 0 - - + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + refresh + True + True + GTK_RELIEF_NORMAL + True - + True - _Save - True - - - - - True - gtk-save - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - True - Save _As ... - True - - - - True - gtk-save-as - 1 - 0.5 - 0.5 - 0 - 0 - - - - - - - - True - - - - - - True - _Quit - True - - - - - True - gtk-quit - 1 - 0.5 - 0.5 - 0 - 0 - - + gtk-refresh + 4 + 0.5 + 0.5 + 0 + 0 + + 0 + False + False + - - - - - - True - _Edit - True - - - - - - True - _View - True - - - - - True - Show Button Bar - True - True - - - - - - True - New Cic Browser - True - - - - - - - True - Show Script Window - True - False - - - - - - - True - - + + True + home + True + True + GTK_RELIEF_NORMAL + True - + True - Toggle console - True - + gtk-home + 4 + 0.5 + 0.5 + 0 + 0 + + 0 + False + False + - - - - - - True - Debug - True - - - - - True - - + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + 0 + False + True + - - - - - - True - _Help - True - - - - - True - About... - True - - + + True + cic uri + True + True + True + 0 + + True + * + False + + 0 + True + True + @@ -284,130 +349,210 @@ 0 False - False + True - + True - True - 450 + 0 + 0 + GTK_SHADOW_NONE - + True True - True - True - GTK_POS_TOP - False - False - - - True - False - - - - - - True - True - False + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT - - True - False - 0 + + + + + + + 0 + True + True + + + + + + + - - - True - False - 0 + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True - - - True - Hide console - True - GTK_RELIEF_NORMAL - True + + + True + False + 0 - - - True - gtk-close - 4 - 0.5 - 0.5 - 0 - 0 - - - - - 0 - False - False - - - - - 0 - False - False - - + + + True + GTK_BUTTONBOX_END - - - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + - - - - - - 0 - True - True - - - - - - - True - False - - + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + True + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 - - 0 - True - True - - + True - True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 - - 0 - False - False - + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + @@ -449,118 +594,98 @@ - - 155 - 450 - Tactics + + 200 + Interpretation choice GTK_WINDOW_TOPLEVEL GTK_WIN_POS_NONE - False - False + True + True False True False False - GDK_WINDOW_TYPE_HINT_TOOLBAR + GDK_WINDOW_TYPE_HINT_DIALOG GDK_GRAVITY_NORTH_WEST + True - - + + True - True - False + False + 0 - - + + True - False - 0 + GTK_BUTTONBOX_END - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Intros - True - intros - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + True + True + gtk-help + True + GTK_RELIEF_NORMAL + True + -11 + + - - - True - True - True - False + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + - - - 50 - True - Apply - True - apply - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + - - - True - True - True - False + + + True + False + 0 - - - 50 - True - Exact - True - exact - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 0 @@ -570,182 +695,318 @@ - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 50 - True - Elim - True - elim - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT - + True - True - True - False - - - - 50 - True - ElimType - True - elimTy - True - GTK_RELIEF_NORMAL - True - - + True + False + False + False + True - - False - False - 0 - False - False + True + True + + + 0 + True + True + + + + + + + + Matita + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + 800 + 600 + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + True + True + False + + + + True + False + 0 - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - + True - True - True - False - + _File + True + - - 50 - True - Split - True - split - True - GTK_RELIEF_NORMAL - True + + + + + True + _New + True + + + + True + gtk-new + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + + True + _Proof or definition ... + True + + + + + + True + (Co)Inductive _definitions ... + True + + + + + + + + + + True + _Open... + True + + + + + True + gtk-open + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Save + True + + + + + True + gtk-save + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Save _As ... + True + + + + True + gtk-save-as + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + _Quit + True + + + + + True + gtk-quit + 1 + 0.5 + 0.5 + 0 + 0 + + + + - - False - False - - + True - True - True - False + _Edit + True + + + + + + True + _View + True - - 25 - True - Left - True - L - True - GTK_RELIEF_NORMAL - True + + + + + True + Show Button Bar + True + True + + + + + + True + New Cic Browser + True + + + + + + + True + Show Script Window + True + False + + + + + + + True + + + + + + True + Toggle console + True + + + - - False - False - - + True - True - True - False + Debug + True - - 25 - True - Right - True - R - True - GTK_RELIEF_NORMAL - True + + + + + True + + - - False - False - - + True - True - True - False + _Help + True - - 25 - True - Exists - True - ∃ - True - GTK_RELIEF_NORMAL - True + + + + + True + About... + True + + - - False - False - @@ -756,322 +1017,427 @@ - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + True + 450 - + True - True - True - False + True + True + True + GTK_POS_TOP + False + False + + + True + False + + + + + + True + True + False - - 50 + True - Reflexivity - True - refl - True - GTK_RELIEF_NORMAL - True + False + 0 + + + + True + False + 0 + + + + True + Hide console + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-close + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + 0 + False + False + + + + + + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + + + + 0 + True + True + + - False - False + True + False + + + 0 + True + True + + + + + + True + True + + + 0 + False + False + + + + + + + + + + Matita: script + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + 450 + 800 + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + True + True + False + + + + True + False + 0 + + + + True + GTK_SHADOW_OUT + GTK_POS_LEFT + GTK_POS_TOP - + True - True - True - False + False + 0 - - - 50 + + True - Symmetry + restart True - sym - True GTK_RELIEF_NORMAL True + + + + True + gtk-goto-top + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - - False - False - - - - - - True - True - True - False - - 50 + True - Transitivity + go back 1 phrase True - trans - True GTK_RELIEF_NORMAL True + + + + True + gtk-go-up + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - 50 + True - Simplify + execute until point True - simpl - True GTK_RELIEF_NORMAL True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - - False - False - - - - - - True - True - True - False - - 50 + True - Reduce + go forward 1 phrase True - red - True GTK_RELIEF_NORMAL True + + + + True + gtk-go-down + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - - False - False - - - - - - True - True - True - False - - 50 + True - Whd + execute all True - whd - True GTK_RELIEF_NORMAL True + + + + True + gtk-goto-bottom + 4 + 0.5 + 0.5 + 0 + 0 + + + + 0 + False + False + - - False - False - 0 False - False + True - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + True + True + True + GTK_POS_BOTTOM + False + False - + True - True - True - False + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT - - 50 + True - Assumption True - asum - True - GTK_RELIEF_NORMAL - True + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + - False - False - - - - - - True - True - True - False - - - - 50 - True - Auto - True - auto - True - GTK_RELIEF_NORMAL - True - - + False + True + + + + + + True + script + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 - False - False + tab - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - + True - True - True - False + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT - - 50 + True - Cut True - cut - True - GTK_RELIEF_NORMAL - True + False + False + False + True - False - False + False + True - + True - True - True - False - - - - 50 - True - Replace - True - repl - True - GTK_RELIEF_NORMAL - True - - + outline + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 - False - False + tab 0 - False - False + True + True @@ -1080,12 +1446,12 @@ - + DUMMY GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - False + GTK_WIN_POS_NONE + False + True False True False @@ -1095,18 +1461,18 @@ True - + True False 0 - + True GTK_BUTTONBOX_END - + True True True @@ -1119,7 +1485,7 @@ - + True True True @@ -1140,12 +1506,12 @@ - + True DUMMY False False - GTK_JUSTIFY_CENTER + GTK_JUSTIFY_LEFT False False 0.5 @@ -1159,307 +1525,225 @@ False - - - - - - Matita: about - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - False - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - + + True - GTK_BUTTONBOX_END + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT - + True - True True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -5 + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + 0 - False + True True - GTK_PACK_END - - - - - - True - <b>Matita @VERSION@</b> - -<tt>http://helm.cs.unibo.it</tt> - -Copyright (C) 2004, -<i>the HELM team</i> - False - True - GTK_JUSTIFY_CENTER - False - False - 0.5 - 0.5 - 5 - 5 - - - 0 - False - False - - 280 - Uri choice + + 155 + 450 + Tactics GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - True + GTK_WIN_POS_NONE + False + False False True False False - GDK_WINDOW_TYPE_HINT_DIALOG + GDK_WINDOW_TYPE_HINT_TOOLBAR GDK_GRAVITY_NORTH_WEST - True - - + + True - False - 0 + True + False - - + + True - GTK_BUTTONBOX_END + False + 0 - + True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - - - True - True - True - GTK_RELIEF_NORMAL - True - 0 + + + True + True + True + False + + + + 50 + True + Intros + True + intros + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + - + True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 + True + True + False - + + 50 True - False - 2 + Apply + True + apply + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + - - - True - gtk-index - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - + + + True + True + True + False - - - True - Try _Selected - True - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - + + + 50 + True + Exact + True + exact + True + GTK_RELIEF_NORMAL + True + + False + False + + + 0 + False + False + - - True - False - True - True - Try Constants - True - GTK_RELIEF_NORMAL - True - 0 - - - - - + True - True - True - GTK_RELIEF_NORMAL - True - 0 + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 + True + True + False - + + 50 True - False - 2 - - - - True - gtk-ok - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - _Auto - True - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - + Elim + True + elim + True + GTK_RELIEF_NORMAL + True + + False + False + - - - - - 0 - False - True - GTK_PACK_END - - - - - True - False - 0 + + + True + True + True + False - - - True - some informative message here ... - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + + + 50 + True + ElimType + True + elimTy + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + 0 @@ -1469,617 +1753,441 @@ Copyright (C) 2004, - + True - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - True - False - False - False - True + True + True + False + + + + 50 + True + Split + True + split + True + GTK_RELIEF_NORMAL + True + + + + False + False + - - - 0 - True - True - - - - - - True - False - 0 - + True - URI: - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + True + True + False + + + + 25 + True + Left + True + L + True + GTK_RELIEF_NORMAL + True + + - 0 False - False + False - + True - True - True - True - 0 - - True - * - False + True + True + False + + + + 25 + True + Right + True + R + True + GTK_RELIEF_NORMAL + True + + - 0 - True - True + False + False - - - 0 - False - True - - - - - 0 - True - True - - - - - - - - 200 - Interpretation choice - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - True - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-help - True - GTK_RELIEF_NORMAL - True - -11 - - - - - - True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - - - - - True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - True - False - 0 - - - - True - some informative message here ... - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - + True - True - False - False - False - True + True + True + False + + + + 25 + True + Exists + True + ∃ + True + GTK_RELIEF_NORMAL + True + + + + False + False + 0 - True - True + False + False - - - 0 - True - True - - - - - - - - True - DUMMY - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - - + True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - True - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - True - DUMMY - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - - - - - - - Matita: script - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - 450 - 800 - True - False - True - False - False - GDK_WINDOW_TYPE_HINT_NORMAL - GDK_GRAVITY_NORTH_WEST - - - - True - True - False + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - - - True - False - 0 + + + True + True + True + False - - - True - GTK_SHADOW_OUT - GTK_POS_LEFT - GTK_POS_TOP + + + 50 + True + Reflexivity + True + refl + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + - + True - False - 0 + True + True + False - + + 50 True - restart + Symmetry True + sym + True GTK_RELIEF_NORMAL True - - - - True - gtk-goto-top - 4 - 0.5 - 0.5 - 0 - 0 - - - - 0 - False - False - + + + False + False + + + + + + True + True + True + False - + + 50 True - go back 1 phrase + Transitivity True + trans + True GTK_RELIEF_NORMAL True - - - - True - gtk-undo - 4 - 0.5 - 0.5 - 0 - 0 - - - - 0 - False - False - + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False - + + 50 True - execute until point + Simplify True + simpl + True GTK_RELIEF_NORMAL True - - - - True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 - - - - 0 - False - False - + + + False + False + + + + + + True + True + True + False - + + 50 True - go forward 1 phrase + Reduce True + red + True GTK_RELIEF_NORMAL True - - - - True - gtk-redo - 4 - 0.5 - 0.5 - 0 - 0 - - - - 0 - False - False - + + + False + False + + + + + + True + True + True + False - + + 50 True - execute all + Whd True + whd + True GTK_RELIEF_NORMAL True - - - - True - gtk-goto-bottom - 4 - 0.5 - 0.5 - 0 - 0 - - - - 0 - False - False - + + False + False + 0 False - True + False - + True - True - True - True - GTK_POS_BOTTOM - False - False + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT + True + True + False - + + 50 True + Assumption True - True - False - True - GTK_JUSTIFY_LEFT - GTK_WRAP_NONE - True - 0 - 0 - 0 - 0 - 0 - 0 - + asum + True + GTK_RELIEF_NORMAL + True - False - True + False + False - + True - script - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + True + True + False + + + + 50 + True + Auto + True + auto + True + GTK_RELIEF_NORMAL + True + + - tab + False + False + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True - + True - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT + True + True + False - + + 50 True + Cut True - False - False - False - True + cut + True + GTK_RELIEF_NORMAL + True - False - True + False + False - + True - outline - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 + True + True + False + + + + 50 + True + Replace + True + repl + True + GTK_RELIEF_NORMAL + True + + - tab + False + False 0 - True - True + False + False @@ -2088,11 +2196,12 @@ Copyright (C) 2004, - - DUMMY + + 280 + Uri choice GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False + GTK_WIN_POS_CENTER + True True False True @@ -2103,18 +2212,18 @@ Copyright (C) 2004, True - + True False 0 - + True GTK_BUTTONBOX_END - + True True True @@ -2127,380 +2236,213 @@ Copyright (C) 2004, - + True True True - gtk-ok - True GTK_RELIEF_NORMAL True - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - True - DUMMY - False - False - GTK_JUSTIFY_LEFT - False - False - 0.5 - 0.5 - 0 - 0 - - - 0 - False - False - - - - - - True - True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - True - True - True - False - True - GTK_JUSTIFY_LEFT - GTK_WRAP_NONE - True - 0 - 0 - 0 - 0 - 0 - 0 - - - - - - 0 - True - True - - - - - - - - 400 - 500 - True - Cic browser - 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 - False - 0 - - - - True - GTK_SHADOW_OUT - GTK_POS_LEFT - GTK_POS_TOP + 0 - + True - False - 0 + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 - + True - new browser win - True - True - GTK_RELIEF_NORMAL - True + False + 2 - + True - gtk-new + gtk-index 4 0.5 0.5 0 0 + + 0 + False + False + - - - 0 - False - False - - - - - - True - history back - True - True - GTK_RELIEF_NORMAL - True - - - - True - 0.5 - 0.5 - 0 - 0 - 0 - 0 - 0 - 0 - - - - True - False - 2 - - - - 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 - - - - - - True - history forward - True - True - GTK_RELIEF_NORMAL - True - + True - gtk-go-forward - 4 + Try _Selected + True + False + GTK_JUSTIFY_LEFT + False + False 0.5 0.5 0 0 + + 0 + False + False + - - 0 - False - False - + + + + + + + + True + False + True + True + Try Constants + True + GTK_RELIEF_NORMAL + True + 0 + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + 0 + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 - + True - refresh - True - True - GTK_RELIEF_NORMAL - True + False + 2 - + True - gtk-refresh + gtk-ok 4 0.5 0.5 0 0 + + 0 + False + False + - - - 0 - False - False - - - - - - True - home - True - True - GTK_RELIEF_NORMAL - True - + True - gtk-home - 4 + _Auto + True + False + GTK_JUSTIFY_LEFT + False + False 0.5 0.5 0 0 + + 0 + False + False + - - 0 - False - False - - - - - - True - gtk-jump-to - 4 - 0.5 - 0.5 - 0 - 0 - - - 0 - False - True - - - - - - True - cic uri - True - True - True - 0 - - True - * - False - - - 0 - True - True - + + + + 0 + False + True + GTK_PACK_END + + + + + + True + False + 0 + + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + 0 False - True + False - + True - 0 - 0 + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT - + True True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - + False + False + False + True @@ -2510,7 +2452,65 @@ Copyright (C) 2004, True + + + + True + False + 0 + + + + True + URI: + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + True + True + 0 + + True + * + False + + + 0 + True + True + + + + + 0 + False + True + + + + 0 + True + True + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 6b7af6983..b62587e1d 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -32,29 +32,23 @@ open MatitaMisc (** {2 Initialization} *) let _ = - Helm_registry.load_from "matita.conf.xml"; - GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; - GMain.Main.init () - -let parserr = new MatitaDisambiguator.parserr () -let dbd = - Mysql.quick_connect - ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") - ~database:(Helm_registry.get "db.database") - () - -let owner = (Helm_registry.get "matita.owner") ;; -let _ = MetadataTypes.ownerize_tables owner ;; -let _ = MatitaDb.clean_owner_environment dbd owner ;; -let _ = MatitaDb.create_owner_environment dbd owner ;; + Helm_registry.load_from "matita.conf.xml"; (* read conf *) + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment (); + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; (* loads gtk rc files *) + ignore (GMain.Main.init ()) let gui = MatitaGui.instance () -let disambiguator = - new MatitaDisambiguator.disambiguator ~parserr ~dbd - ~chooseUris:(interactive_user_uri_choice ~gui) - ~chooseInterp:(interactive_interp_choice ~gui) - () +let _ = (* set disambiguator callbacks *) + let disambiguator = MatitaDisambiguator.instance () in + disambiguator#setChooseUris (interactive_user_uri_choice ~gui); + disambiguator#setChooseInterp (interactive_interp_choice ~gui) +let _ = (* environment trust *) + CicEnvironment.set_trust + (let trust = Helm_registry.get_bool "matita.environment_trust" in + fun _ -> trust) let currentProof = MatitaProof.instance () @@ -89,10 +83,9 @@ let _ = (* attach observers to proof status *) false); currentProof#connect `Abort (fun () -> sequents_viewer#reset; false) -let mathViewer = MatitaMathView.mathViewer ~disambiguator () let interpreter = - let console = gui#console in - MatitaInterpreter.interpreter ~disambiguator ~console ~mathViewer () + let mathViewer = MatitaMathView.mathViewer () in + MatitaInterpreter.interpreter ~console:gui#console ~mathViewer () let _ = let href_callback uri = let term = CicAst.Uri (UriManager.string_of_uri uri, None) in @@ -160,7 +153,7 @@ let _ = "Don't know what to do with file: %s\nUnrecognized file format." f))); ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ -> - ignore (MatitaMathView.cicBrowser ~disambiguator ()))); + ignore (MatitaMathView.cicBrowser ()))); connect_button gui#script#scriptWinForwardButton script_forward; connect_button gui#script#scriptWinBackButton script_back; connect_button gui#script#scriptWinJumpButton script_jump; @@ -200,11 +193,6 @@ let _ = in ignore (item#connect#activate callback) in - addDebugItem "toggle auto disambiguation" (fun _ -> - Helm_registry.set_bool "matita.auto_disambiguation" - (not (Helm_registry.get_bool "matita.auto_disambiguation"))); - addDebugItem "dump proof status to stdout" (fun _ -> - print_endline (currentProof#proof#toString)); addDebugItem "dump environment to \"env.dump\"" (fun _ -> let oc = open_out "env.dump" in CicEnvironment.dump_to_channel oc; @@ -214,21 +202,24 @@ let _ = List.iter (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t))) sequent_viewer#get_selected_terms); - addDebugItem "refresh all browsers" MatitaMathView.refresh_all_browsers; + addDebugItem "dump getter settings" (fun _ -> + prerr_endline (Http_getter_env.env_to_string ())); + addDebugItem "getter: update" Http_getter.update; + addDebugItem "getter: getalluris" (fun _ -> + List.iter prerr_endline (Http_getter.getalluris ())); end (** *) let _ = -(* CicEnvironment.set_trust (fun _ -> false); *) (* (try load_script Sys.argv.(1) with Invalid_argument _ -> ()); *) - if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin (* cicbrowser *) - let browser = MatitaMathView.cicBrowser ~disambiguator () in + if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *) Helm_registry.set "matita.mode" "cicbrowser"; + let browser = MatitaMathView.cicBrowser () in try browser#loadUri Sys.argv.(1) with Invalid_argument _ -> () diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index a6eb73ded..b2c97789d 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -25,7 +25,11 @@ open Printf ;; -let clean_owner_environment dbd owner = +let xpointer_RE = Pcre.regexp "#.*$" + +let clean_owner_environment () = + let dbd = MatitaMisc.dbd_instance () in + let owner = (Helm_registry.get "matita.owner") in let obj_tbl = MetadataTypes.obj_tbl () in let sort_tbl = MetadataTypes.sort_tbl () in let rel_tbl = MetadataTypes.rel_tbl () in @@ -50,28 +54,34 @@ DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no); DROP INDEX no_concl_hyp_source ON no_concl_hyp (source); DROP INDEX no_concl_hyp_no ON no_concl_hyp (no); *) - (try - MetadataDb.clean ~dbd - with - exn -> - match Mysql.errno dbd with - | Mysql.No_such_table -> () - | _ -> raise exn - | _ -> () - ); + let owned_uris = + try + MetadataDb.clean ~dbd + with Mysql.Error _ as exn -> + match Mysql.errno dbd with + | Mysql.No_such_table -> [] + | _ -> raise exn + in + List.iter + (fun uri -> + let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in + List.iter + (fun suffix -> Http_getter.unregister (uri ^ suffix)) + [""; ".body"; ".types"]) + owned_uris; List.iter (fun statement -> try ignore (Mysql.exec dbd statement) - with - exn -> - match Mysql.errno dbd with - | Mysql.No_such_table -> () - | _ -> raise exn - | _ -> () - ) statements + with Mysql.Error _ as exn -> + match Mysql.errno dbd with + | Mysql.Bad_table_error -> () + | _ -> raise exn + ) statements; ;; -let create_owner_environment dbd owner = +let create_owner_environment () = + let dbd = MatitaMisc.dbd_instance () in + let owner = (Helm_registry.get "matita.owner") in let obj_tbl = MetadataTypes.obj_tbl () in let sort_tbl = MetadataTypes.sort_tbl () in let rel_tbl = MetadataTypes.rel_tbl () in diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli index b470ec596..32b816000 100644 --- a/helm/matita/matitaDb.mli +++ b/helm/matita/matitaDb.mli @@ -23,6 +23,6 @@ * http://helm.cs.unibo.it/ *) -val clean_owner_environment : Mysql.dbd -> string -> unit -val create_owner_environment : Mysql.dbd -> string -> unit +val clean_owner_environment : unit -> unit +val create_owner_environment : unit -> unit diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 15f21e509..178c7d8c7 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -31,10 +31,12 @@ class parserr () = method parseTactical = CicTextualParser2.parse_tactical end -class disambiguator - ~parserr ~dbd ~(chooseUris: MatitaTypes.choose_uris_callback) - ~(chooseInterp: MatitaTypes.choose_interp_callback) () - = +let parserr () = new parserr () +let parserr_instance = MatitaMisc.singleton parserr + +class disambiguator () = + let _chooseUris = ref mono_uris_callback in + let _chooseInterp = ref mono_interp_callback in let disambiguate_term = let module Callbacks = struct @@ -42,15 +44,16 @@ class disambiguator ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - chooseUris ~selection_mode ~title ~msg + !_chooseUris ~selection_mode ~title ~msg ~nonvars_button:enable_button_for_non_vars uris - let interactive_interpretation_choice = chooseInterp + let interactive_interpretation_choice interp = !_chooseInterp interp + let input_or_locate_uri ~(title:string) ?id = (* Zack: I try to avoid using this callback. I therefore assume that * the presence of an identifier that can't be resolved via "locate" * query is a syntax error *) - let msg = match id with Some id -> id | _ -> "" in + let msg = match id with Some id -> id | _ -> "_" in raise (Unbound_identifier msg) end in @@ -58,14 +61,21 @@ class disambiguator Disambiguator.disambiguate_term in object (self) - val mutable parserr: parserr = parserr - method parserr = parserr - method setParserr p = parserr <- p - val mutable _env = DisambiguateTypes.Environment.empty method env = _env method setEnv e = _env <- e + method chooseUris = !_chooseUris + method setChooseUris f = _chooseUris := f + + method chooseInterp = !_chooseInterp + method setChooseInterp f = _chooseInterp := f + + val parserr = parserr_instance () + method parserr = parserr + + val dbd = MatitaMisc.dbd_instance () + method disambiguateTermAst ?(context = []) ?(metasenv = []) ?env termAst = let (save_state, env) = match env with @@ -91,3 +101,6 @@ class disambiguator (parserr#parseTerm stream) end +let disambiguator () = new disambiguator () +let instance = MatitaMisc.singleton disambiguator + diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli index 5b7bbc880..7def4dc70 100644 --- a/helm/matita/matitaDisambiguator.mli +++ b/helm/matita/matitaDisambiguator.mli @@ -23,13 +23,12 @@ * http://helm.cs.unibo.it/ *) -class parserr: unit -> MatitaTypes.parserr +val parserr: unit -> MatitaTypes.parserr +val disambiguator: unit -> MatitaTypes.disambiguator -class disambiguator: - parserr:MatitaTypes.parserr -> (** parser *) - dbd:Mysql.dbd -> - chooseUris:MatitaTypes.choose_uris_callback -> - chooseInterp:MatitaTypes.choose_interp_callback -> - unit -> - MatitaTypes.disambiguator + (** singleton parser instance *) +val parserr_instance: unit -> MatitaTypes.parserr + + (** singleton disambiguator instance *) +val instance: unit -> MatitaTypes.disambiguator diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 11d5dcb9e..c7d13dfbd 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -1,378 +1,5 @@ (* Automatically generated from matita.glade by lablgladecc *) -class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"MainWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val mainWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata)) - method mainWin = mainWin - val mainWinEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata)) - method mainWinEventBox = mainWinEventBox - val mainWinShape = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata)) - method mainWinShape = mainWinShape - val mainMenuBar = - new GMenu.menu_shell (GtkMenu.MenuBar.cast - (Glade.get_widget_msg ~name:"MainMenuBar" ~info:"GtkMenuBar" xmldata)) - method mainMenuBar = mainMenuBar - val fileMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"FileMenu" ~info:"GtkMenuItem" xmldata)) - method fileMenu = fileMenu - val fileMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"FileMenu_menu" ~info:"GtkMenu" xmldata)) - method fileMenu_menu = fileMenu_menu - val newMenu = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata)) - method newMenu = newMenu - val image224 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata)) - method image224 = image224 - val newMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata)) - method newMenu_menu = newMenu_menu - val newProofMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata)) - method newProofMenuItem = newProofMenuItem - val newDefsMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata)) - method newDefsMenuItem = newDefsMenuItem - val openMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method openMenuItem = openMenuItem - val image225 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata)) - method image225 = image225 - val saveMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method saveMenuItem = saveMenuItem - val image226 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata)) - method image226 = image226 - val saveAsMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method saveAsMenuItem = saveAsMenuItem - val image227 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata)) - method image227 = image227 - val separator1 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata)) - method separator1 = separator1 - val quitMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method quitMenuItem = quitMenuItem - val image228 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata)) - method image228 = image228 - val editMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) - method editMenu = editMenu - val viewMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"ViewMenu" ~info:"GtkMenuItem" xmldata)) - method viewMenu = viewMenu - val viewMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"ViewMenu_menu" ~info:"GtkMenu" xmldata)) - method viewMenu_menu = viewMenu_menu - val showToolBarMenuItem = - new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast - (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata)) - method showToolBarMenuItem = showToolBarMenuItem - val newCicBrowserMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata)) - method newCicBrowserMenuItem = newCicBrowserMenuItem - val showScriptMenuItem = - new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast - (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata)) - method showScriptMenuItem = showScriptMenuItem - val separator3 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata)) - method separator3 = separator3 - val showConsoleMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata)) - method showConsoleMenuItem = showConsoleMenuItem - val debugMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata)) - method debugMenu = debugMenu - val debugMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata)) - method debugMenu_menu = debugMenu_menu - val separator2 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata)) - method separator2 = separator2 - val helpMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata)) - method helpMenu = helpMenu - val helpMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"HelpMenu_menu" ~info:"GtkMenu" xmldata)) - method helpMenu_menu = helpMenu_menu - val aboutMenuItem = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"AboutMenuItem" ~info:"GtkMenuItem" xmldata)) - method aboutMenuItem = aboutMenuItem - val mainVPanes = - new GPack.paned (GtkPack.Paned.cast - (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata)) - method mainVPanes = mainVPanes - val sequentsNotebook = - new GPack.notebook (GtkPack.Notebook.cast - (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata)) - method sequentsNotebook = sequentsNotebook - val consoleEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata)) - method consoleEventBox = consoleEventBox - val consoleHBox = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata)) - method consoleHBox = consoleHBox - val vbox6 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata)) - method vbox6 = vbox6 - val hideConsoleButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata)) - method hideConsoleButton = hideConsoleButton - val image169 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata)) - method image169 = image169 - val scrolledConsole = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata)) - method scrolledConsole = scrolledConsole - val mainStatusBar = - new GMisc.statusbar (GtkMisc.Statusbar.cast - (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata)) - method mainStatusBar = mainStatusBar - method reparent parent = - mainWinEventBox#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) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.file_selection (GtkWindow.FileSelection.cast - (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata)) - method toplevel = toplevel - val fileSelectionWin = - new GWindow.file_selection (GtkWindow.FileSelection.cast - (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata)) - method fileSelectionWin = fileSelectionWin - val fileSelCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata)) - method fileSelCancelButton = fileSelCancelButton - val fileSelOkButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata)) - method fileSelOkButton = fileSelOkButton - method check_widgets () = () - end -class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"ToolBarWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val toolBarWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata)) - method toolBarWin = toolBarWin - val toolBarEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata)) - method toolBarEventBox = toolBarEventBox - val toolBarVBox = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata)) - method toolBarVBox = toolBarVBox - val toolbar2 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata)) - method toolbar2 = toolbar2 - val introsButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata)) - method introsButton = introsButton - val applyButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata)) - method applyButton = applyButton - val exactButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata)) - method exactButton = exactButton - val toolbar3 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata)) - method toolbar3 = toolbar3 - val elimButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata)) - method elimButton = elimButton - val elimTypeButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata)) - method elimTypeButton = elimTypeButton - val toolbar4 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata)) - method toolbar4 = toolbar4 - val splitButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata)) - method splitButton = splitButton - val leftButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata)) - method leftButton = leftButton - val rightButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata)) - method rightButton = rightButton - val existsButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata)) - method existsButton = existsButton - val toolbar5 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata)) - method toolbar5 = toolbar5 - val reflexivityButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata)) - method reflexivityButton = reflexivityButton - val symmetryButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata)) - method symmetryButton = symmetryButton - val transitivityButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata)) - method transitivityButton = transitivityButton - val toolbar8 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata)) - method toolbar8 = toolbar8 - val simplifyButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata)) - method simplifyButton = simplifyButton - val reduceButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata)) - method reduceButton = reduceButton - val whdButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata)) - method whdButton = whdButton - val toolbar6 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata)) - method toolbar6 = toolbar6 - val assumptionButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata)) - method assumptionButton = assumptionButton - val autoButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata)) - method autoButton = autoButton - val toolbar7 = - new GButton.toolbar (GtkButton.Toolbar.cast - (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata)) - method toolbar7 = toolbar7 - val cutButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata)) - method cutButton = cutButton - val replaceButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata)) - method replaceButton = replaceButton - method reparent parent = - toolBarEventBox#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val confirmationDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) - method confirmationDialog = confirmationDialog - val dialog_vbox1 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata)) - method dialog_vbox1 = dialog_vbox1 - val dialog_action_area1 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area1 = dialog_action_area1 - val confirmationDialogCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata)) - method confirmationDialogCancelButton = confirmationDialogCancelButton - val confirmationDialogOkButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata)) - method confirmationDialogOkButton = confirmationDialogOkButton - val confirmationDialogLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata)) - method confirmationDialogLabel = confirmationDialogLabel - method reparent parent = - dialog_vbox1#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = let xmldata = Glade.create ~file ~root:"AboutWin" ?domain () in object (self) @@ -406,107 +33,203 @@ class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = toplevel#destroy () method check_widgets () = () end -class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in +class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"BrowserWin" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) method toplevel = toplevel - val uriChoiceDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) - method uriChoiceDialog = uriChoiceDialog - val dialog_vbox3 = + val browserWin = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) + method browserWin = browserWin + val browserWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata)) + method browserWinEventBox = browserWinEventBox + val browserVBox = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata)) - method dialog_vbox3 = dialog_vbox3 - val dialog_action_area3 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area3 = dialog_action_area3 - val uriChoiceAbortButton = + (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)) + method hbox7 = hbox7 + val browserNewButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata)) - method uriChoiceAbortButton = uriChoiceAbortButton - val uriChoiceSelectedButton = + (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata)) + method browserNewButton = browserNewButton + val image191 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata)) + method image191 = image191 + val browserBackButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata)) - method uriChoiceSelectedButton = uriChoiceSelectedButton - val alignment2 = + (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata)) + method browserBackButton = browserBackButton + val alignment3 = new GBin.alignment (GtkBin.Alignment.cast - (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata)) - method alignment2 = alignment2 - val hbox3 = + (Glade.get_widget_msg ~name:"alignment3" ~info:"GtkAlignment" xmldata)) + method alignment3 = alignment3 + val hbox6 = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata)) - method hbox3 = hbox3 - val image19 = + (Glade.get_widget_msg ~name:"hbox6" ~info:"GtkHBox" xmldata)) + method hbox6 = hbox6 + val image188 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata)) - method image19 = image19 - val label3 = + (Glade.get_widget_msg ~name:"image188" ~info:"GtkImage" xmldata)) + method image188 = image188 + val label10 = new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata)) - method label3 = label3 - val uriChoiceConstantsButton = + (Glade.get_widget_msg ~name:"label10" ~info:"GtkLabel" xmldata)) + method label10 = label10 + val browserForwardButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata)) - method uriChoiceConstantsButton = uriChoiceConstantsButton - val uriChoiceAutoButton = + (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata)) + method browserForwardButton = browserForwardButton + val image189 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata)) + method image189 = image189 + val browserRefreshButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata)) - method uriChoiceAutoButton = uriChoiceAutoButton - val alignment1 = - new GBin.alignment (GtkBin.Alignment.cast - (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata)) - method alignment1 = alignment1 - val hbox1 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata)) - method hbox1 = hbox1 - val image18 = + (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata)) + method browserRefreshButton = browserRefreshButton + val image229 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata)) - method image18 = image18 - val label1 = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata)) - method label1 = label1 - val vbox2 = + (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata)) + method image229 = image229 + val browserHomeButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata)) + method browserHomeButton = browserHomeButton + val image190 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata)) + method image190 = image190 + val image187 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata)) + method image187 = image187 + val browserUri = + new GEdit.entry (GtkEdit.Entry.cast + (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata)) + method browserUri = browserUri + val frame1 = + new GBin.frame (GtkBin.Frame.cast + (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata)) + method frame1 = frame1 + val scrolledBrowser = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata)) + method scrolledBrowser = scrolledBrowser + method reparent parent = + browserWinEventBox#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end +class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) + method toplevel = toplevel + val confirmationDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata)) + method confirmationDialog = confirmationDialog + val dialog_vbox1 = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata)) - method vbox2 = vbox2 - val uriChoiceLabel = + (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata)) + method dialog_vbox1 = dialog_vbox1 + val dialog_action_area1 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area1 = dialog_action_area1 + val confirmationDialogCancelButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata)) + method confirmationDialogCancelButton = confirmationDialogCancelButton + val confirmationDialogOkButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata)) + method confirmationDialogOkButton = confirmationDialogOkButton + val confirmationDialogLabel = new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata)) - method uriChoiceLabel = uriChoiceLabel - val scrolledwindow1 = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata)) - method scrolledwindow1 = scrolledwindow1 - val uriChoiceTreeView = - new GTree.view (GtkTree.TreeView.cast - (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata)) - method uriChoiceTreeView = uriChoiceTreeView - val hbox2 = + (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata)) + method confirmationDialogLabel = confirmationDialogLabel + method reparent parent = + dialog_vbox1#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end +class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"EmptyDialog" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) + method toplevel = toplevel + val emptyDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) + method emptyDialog = emptyDialog + val emptyDialogVBox = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata)) - method hbox2 = hbox2 - val label2 = + (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata)) + method emptyDialogVBox = emptyDialogVBox + val dialog_action_area5 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area5 = dialog_action_area5 + val emptyDialogCancelButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata)) + method emptyDialogCancelButton = emptyDialogCancelButton + val emptyDialogOkButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata)) + method emptyDialogOkButton = emptyDialogOkButton + val emptyDialogLabel = new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata)) - method label2 = label2 - val entry1 = - new GEdit.entry (GtkEdit.Entry.cast - (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata)) - method entry1 = entry1 + (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata)) + method emptyDialogLabel = emptyDialogLabel method reparent parent = - dialog_vbox3#misc#reparent parent; + emptyDialogVBox#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) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.file_selection (GtkWindow.FileSelection.cast + (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata)) + method toplevel = toplevel + val fileSelectionWin = + new GWindow.file_selection (GtkWindow.FileSelection.cast + (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata)) + method fileSelectionWin = fileSelectionWin + val fileSelCancelButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata)) + method fileSelCancelButton = fileSelCancelButton + val fileSelOkButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata)) + method fileSelOkButton = fileSelOkButton + method check_widgets () = () + end class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = let xmldata = Glade.create ~file ~root:"InterpChoiceDialog" ?domain () in object (self) @@ -541,59 +264,207 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () method interpChoiceOkButton = interpChoiceOkButton val vbox3 = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata)) - method vbox3 = vbox3 - val interpChoiceDialogLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata)) - method interpChoiceDialogLabel = interpChoiceDialogLabel - val scrolledwindow4 = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata)) - method scrolledwindow4 = scrolledwindow4 - val interpChoiceTreeView = - new GTree.view (GtkTree.TreeView.cast - (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata)) - method interpChoiceTreeView = interpChoiceTreeView - method reparent parent = - dialog_vbox4#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"EmptyDialog" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val emptyDialog = - new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) - method emptyDialog = emptyDialog - val emptyDialogVBox = + (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata)) + method vbox3 = vbox3 + val interpChoiceDialogLabel = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata)) + method interpChoiceDialogLabel = interpChoiceDialogLabel + val scrolledwindow4 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata)) + method scrolledwindow4 = scrolledwindow4 + val interpChoiceTreeView = + new GTree.view (GtkTree.TreeView.cast + (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata)) + method interpChoiceTreeView = interpChoiceTreeView + method reparent parent = + dialog_vbox4#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end +class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"MainWin" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata)) + method toplevel = toplevel + val mainWin = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata)) + method mainWin = mainWin + val mainWinEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata)) + method mainWinEventBox = mainWinEventBox + val mainWinShape = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata)) + method mainWinShape = mainWinShape + val mainMenuBar = + new GMenu.menu_shell (GtkMenu.MenuBar.cast + (Glade.get_widget_msg ~name:"MainMenuBar" ~info:"GtkMenuBar" xmldata)) + method mainMenuBar = mainMenuBar + val fileMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"FileMenu" ~info:"GtkMenuItem" xmldata)) + method fileMenu = fileMenu + val fileMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast + (Glade.get_widget_msg ~name:"FileMenu_menu" ~info:"GtkMenu" xmldata)) + method fileMenu_menu = fileMenu_menu + val newMenu = + new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast + (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata)) + method newMenu = newMenu + val image224 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata)) + method image224 = image224 + val newMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast + (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata)) + method newMenu_menu = newMenu_menu + val newProofMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata)) + method newProofMenuItem = newProofMenuItem + val newDefsMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata)) + method newDefsMenuItem = newDefsMenuItem + val openMenuItem = + new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast + (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata)) + method openMenuItem = openMenuItem + val image225 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata)) + method image225 = image225 + val saveMenuItem = + new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast + (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) + method saveMenuItem = saveMenuItem + val image226 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata)) + method image226 = image226 + val saveAsMenuItem = + new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast + (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) + method saveAsMenuItem = saveAsMenuItem + val image227 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata)) + method image227 = image227 + val separator1 = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata)) + method separator1 = separator1 + val quitMenuItem = + new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast + (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata)) + method quitMenuItem = quitMenuItem + val image228 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata)) + method image228 = image228 + val editMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) + method editMenu = editMenu + val viewMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"ViewMenu" ~info:"GtkMenuItem" xmldata)) + method viewMenu = viewMenu + val viewMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast + (Glade.get_widget_msg ~name:"ViewMenu_menu" ~info:"GtkMenu" xmldata)) + method viewMenu_menu = viewMenu_menu + val showToolBarMenuItem = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast + (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata)) + method showToolBarMenuItem = showToolBarMenuItem + val newCicBrowserMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata)) + method newCicBrowserMenuItem = newCicBrowserMenuItem + val showScriptMenuItem = + new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast + (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata)) + method showScriptMenuItem = showScriptMenuItem + val separator3 = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata)) + method separator3 = separator3 + val showConsoleMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata)) + method showConsoleMenuItem = showConsoleMenuItem + val debugMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata)) + method debugMenu = debugMenu + val debugMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast + (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata)) + method debugMenu_menu = debugMenu_menu + val separator2 = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata)) + method separator2 = separator2 + val helpMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata)) + method helpMenu = helpMenu + val helpMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast + (Glade.get_widget_msg ~name:"HelpMenu_menu" ~info:"GtkMenu" xmldata)) + method helpMenu_menu = helpMenu_menu + val aboutMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"AboutMenuItem" ~info:"GtkMenuItem" xmldata)) + method aboutMenuItem = aboutMenuItem + val mainVPanes = + new GPack.paned (GtkPack.Paned.cast + (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata)) + method mainVPanes = mainVPanes + val sequentsNotebook = + new GPack.notebook (GtkPack.Notebook.cast + (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata)) + method sequentsNotebook = sequentsNotebook + val consoleEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata)) + method consoleEventBox = consoleEventBox + val consoleHBox = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata)) + method consoleHBox = consoleHBox + val vbox6 = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata)) - method emptyDialogVBox = emptyDialogVBox - val dialog_action_area5 = - new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata)) - method dialog_action_area5 = dialog_action_area5 - val emptyDialogCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata)) - method emptyDialogCancelButton = emptyDialogCancelButton - val emptyDialogOkButton = + (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata)) + method vbox6 = vbox6 + val hideConsoleButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata)) - method emptyDialogOkButton = emptyDialogOkButton - val emptyDialogLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata)) - method emptyDialogLabel = emptyDialogLabel + (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata)) + method hideConsoleButton = hideConsoleButton + val image169 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata)) + method image169 = image169 + val scrolledConsole = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata)) + method scrolledConsole = scrolledConsole + val mainStatusBar = + new GMisc.statusbar (GtkMisc.Statusbar.cast + (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata)) + method mainStatusBar = mainStatusBar method reparent parent = - emptyDialogVBox#misc#reparent parent; + mainWinEventBox#misc#reparent parent; toplevel#destroy () method check_widgets () = () end @@ -637,10 +508,10 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata)) method scriptWinBackButton = scriptWinBackButton - val image133 = + val image237 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image133" ~info:"GtkImage" xmldata)) - method image133 = image133 + (Glade.get_widget_msg ~name:"image237" ~info:"GtkImage" xmldata)) + method image237 = image237 val scriptWinJumpButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"ScriptWinJumpButton" ~info:"GtkButton" xmldata)) @@ -653,18 +524,18 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"ScriptWinForwardButton" ~info:"GtkButton" xmldata)) method scriptWinForwardButton = scriptWinForwardButton - val image135 = + val image239 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata)) - method image135 = image135 + (Glade.get_widget_msg ~name:"image239" ~info:"GtkImage" xmldata)) + method image239 = image239 val scriptWinBottomButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"ScriptWinBottomButton" ~info:"GtkButton" xmldata)) method scriptWinBottomButton = scriptWinBottomButton - val image236 = + val image238 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image236" ~info:"GtkImage" xmldata)) - method image236 = image236 + (Glade.get_widget_msg ~name:"image238" ~info:"GtkImage" xmldata)) + method image238 = image238 val scriptNotebook = new GPack.notebook (GtkPack.Notebook.cast (Glade.get_widget_msg ~name:"ScriptNotebook" ~info:"GtkNotebook" xmldata)) @@ -685,200 +556,329 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (Glade.get_widget_msg ~name:"ScrolledOutline" ~info:"GtkScrolledWindow" xmldata)) method scrolledOutline = scrolledOutline - val treeview1 = + val outlineTreeView = new GTree.view (GtkTree.TreeView.cast - (Glade.get_widget_msg ~name:"treeview1" ~info:"GtkTreeView" xmldata)) - method treeview1 = treeview1 + (Glade.get_widget_msg ~name:"OutlineTreeView" ~info:"GtkTreeView" xmldata)) + method outlineTreeView = outlineTreeView val label8 = new GMisc.label (GtkMisc.Label.cast (Glade.get_widget_msg ~name:"label8" ~info:"GtkLabel" xmldata)) method label8 = label8 method reparent parent = - scriptWinEventBox#misc#reparent parent; + scriptWinEventBox#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end +class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"TextDialog" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) + method toplevel = toplevel + val textDialog = + new GWindow.dialog_any (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) + method textDialog = textDialog + val vbox5 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"vbox5" ~info:"GtkVBox" xmldata)) + method vbox5 = vbox5 + val hbuttonbox1 = + new GPack.button_box (GtkPack.BBox.cast + (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata)) + method hbuttonbox1 = hbuttonbox1 + val textDialogCancelButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata)) + method textDialogCancelButton = textDialogCancelButton + val textDialogOkButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata)) + method textDialogOkButton = textDialogOkButton + val textDialogLabel = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata)) + method textDialogLabel = textDialogLabel + val scrolledwindow2 = + new GBin.scrolled_window (GtkBin.ScrolledWindow.cast + (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata)) + method scrolledwindow2 = scrolledwindow2 + val textDialogTextView = + new GText.view (GtkText.View.cast + (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata)) + method textDialogTextView = textDialogTextView + method reparent parent = + vbox5#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end +class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"ToolBarWin" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata)) + method toplevel = toplevel + val toolBarWin = + new GWindow.window (GtkWindow.Window.cast + (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata)) + method toolBarWin = toolBarWin + val toolBarEventBox = + new GBin.event_box (GtkBin.EventBox.cast + (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata)) + method toolBarEventBox = toolBarEventBox + val toolBarVBox = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata)) + method toolBarVBox = toolBarVBox + val toolbar2 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata)) + method toolbar2 = toolbar2 + val introsButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata)) + method introsButton = introsButton + val applyButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata)) + method applyButton = applyButton + val exactButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata)) + method exactButton = exactButton + val toolbar3 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata)) + method toolbar3 = toolbar3 + val elimButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata)) + method elimButton = elimButton + val elimTypeButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata)) + method elimTypeButton = elimTypeButton + val toolbar4 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata)) + method toolbar4 = toolbar4 + val splitButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata)) + method splitButton = splitButton + val leftButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata)) + method leftButton = leftButton + val rightButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata)) + method rightButton = rightButton + val existsButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata)) + method existsButton = existsButton + val toolbar5 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata)) + method toolbar5 = toolbar5 + val reflexivityButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata)) + method reflexivityButton = reflexivityButton + val symmetryButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata)) + method symmetryButton = symmetryButton + val transitivityButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata)) + method transitivityButton = transitivityButton + val toolbar8 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata)) + method toolbar8 = toolbar8 + val simplifyButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata)) + method simplifyButton = simplifyButton + val reduceButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata)) + method reduceButton = reduceButton + val whdButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata)) + method whdButton = whdButton + val toolbar6 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata)) + method toolbar6 = toolbar6 + val assumptionButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata)) + method assumptionButton = assumptionButton + val autoButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata)) + method autoButton = autoButton + val toolbar7 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata)) + method toolbar7 = toolbar7 + val cutButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata)) + method cutButton = cutButton + val replaceButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata)) + method replaceButton = replaceButton + method reparent parent = + toolBarEventBox#misc#reparent parent; toplevel#destroy () method check_widgets () = () end -class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"TextDialog" ?domain () in +class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata val toplevel = new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) + (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val textDialog = + val uriChoiceDialog = new GWindow.dialog_any (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) - method textDialog = textDialog - val vbox5 = + (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata)) + method uriChoiceDialog = uriChoiceDialog + val dialog_vbox3 = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"vbox5" ~info:"GtkVBox" xmldata)) - method vbox5 = vbox5 - val hbuttonbox1 = + (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata)) + method dialog_vbox3 = dialog_vbox3 + val dialog_action_area3 = new GPack.button_box (GtkPack.BBox.cast - (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata)) - method hbuttonbox1 = hbuttonbox1 - val textDialogCancelButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata)) - method textDialogCancelButton = textDialogCancelButton - val textDialogOkButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata)) - method textDialogOkButton = textDialogOkButton - val textDialogLabel = - new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata)) - method textDialogLabel = textDialogLabel - val scrolledwindow2 = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata)) - method scrolledwindow2 = scrolledwindow2 - val textDialogTextView = - new GText.view (GtkText.View.cast - (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata)) - method textDialogTextView = textDialogTextView - method reparent parent = - vbox5#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end -class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"BrowserWin" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) - method toplevel = toplevel - val browserWin = - new GWindow.window (GtkWindow.Window.cast - (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata)) - method browserWin = browserWin - val browserWinEventBox = - new GBin.event_box (GtkBin.EventBox.cast - (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata)) - method browserWinEventBox = browserWinEventBox - val browserVBox = - 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)) - method hbox7 = hbox7 - val browserNewButton = + (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata)) + method dialog_action_area3 = dialog_action_area3 + val uriChoiceAbortButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata)) - method browserNewButton = browserNewButton - val image191 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata)) - method image191 = image191 - val browserBackButton = + (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata)) + method uriChoiceAbortButton = uriChoiceAbortButton + val uriChoiceSelectedButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata)) - method browserBackButton = browserBackButton - val alignment3 = + (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata)) + method uriChoiceSelectedButton = uriChoiceSelectedButton + val alignment2 = new GBin.alignment (GtkBin.Alignment.cast - (Glade.get_widget_msg ~name:"alignment3" ~info:"GtkAlignment" xmldata)) - method alignment3 = alignment3 - val hbox6 = + (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata)) + method alignment2 = alignment2 + val hbox3 = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox6" ~info:"GtkHBox" xmldata)) - method hbox6 = hbox6 - val image188 = + (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata)) + method hbox3 = hbox3 + val image19 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image188" ~info:"GtkImage" xmldata)) - method image188 = image188 - val label10 = + (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata)) + method image19 = image19 + val label3 = new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"label10" ~info:"GtkLabel" xmldata)) - method label10 = label10 - val browserForwardButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata)) - method browserForwardButton = browserForwardButton - val image189 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata)) - method image189 = image189 - val browserRefreshButton = + (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata)) + method label3 = label3 + val uriChoiceConstantsButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata)) - method browserRefreshButton = browserRefreshButton - val image229 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata)) - method image229 = image229 - val browserHomeButton = + (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata)) + method uriChoiceConstantsButton = uriChoiceConstantsButton + val uriChoiceAutoButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata)) - method browserHomeButton = browserHomeButton - val image190 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata)) - method image190 = image190 - val image187 = + (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata)) + method uriChoiceAutoButton = uriChoiceAutoButton + val alignment1 = + new GBin.alignment (GtkBin.Alignment.cast + (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata)) + method alignment1 = alignment1 + val hbox1 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata)) + method hbox1 = hbox1 + val image18 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata)) - method image187 = image187 - val browserUri = - new GEdit.entry (GtkEdit.Entry.cast - (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata)) - method browserUri = browserUri - val frame1 = - new GBin.frame (GtkBin.Frame.cast - (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata)) - method frame1 = frame1 - val scrolledBrowser = + (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata)) + method image18 = image18 + val label1 = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata)) + method label1 = label1 + val vbox2 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata)) + method vbox2 = vbox2 + val uriChoiceLabel = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata)) + method uriChoiceLabel = uriChoiceLabel + val scrolledwindow1 = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata)) - method scrolledBrowser = scrolledBrowser + (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata)) + method scrolledwindow1 = scrolledwindow1 + val uriChoiceTreeView = + new GTree.view (GtkTree.TreeView.cast + (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata)) + method uriChoiceTreeView = uriChoiceTreeView + val hbox2 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata)) + method hbox2 = hbox2 + val label2 = + new GMisc.label (GtkMisc.Label.cast + (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata)) + method label2 = label2 + val entry1 = + new GEdit.entry (GtkEdit.Entry.cast + (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata)) + method entry1 = entry1 method reparent parent = - browserWinEventBox#misc#reparent parent; + dialog_vbox3#misc#reparent parent; toplevel#destroy () method check_widgets () = () end let check_all ?(show=false) () = ignore (GMain.Main.init ()); - let browserWin = new browserWin () in - if show then browserWin#toplevel#show (); - browserWin#check_widgets (); + let uriChoiceDialog = new uriChoiceDialog () in + if show then uriChoiceDialog#toplevel#show (); + uriChoiceDialog#check_widgets (); + let toolBarWin = new toolBarWin () in + if show then toolBarWin#toplevel#show (); + toolBarWin#check_widgets (); let textDialog = new textDialog () in if show then textDialog#toplevel#show (); textDialog#check_widgets (); let scriptWin = new scriptWin () in if show then scriptWin#toplevel#show (); scriptWin#check_widgets (); - let emptyDialog = new emptyDialog () in - if show then emptyDialog#toplevel#show (); - emptyDialog#check_widgets (); + let mainWin = new mainWin () in + if show then mainWin#toplevel#show (); + mainWin#check_widgets (); let interpChoiceDialog = new interpChoiceDialog () in if show then interpChoiceDialog#toplevel#show (); interpChoiceDialog#check_widgets (); - let uriChoiceDialog = new uriChoiceDialog () in - if show then uriChoiceDialog#toplevel#show (); - uriChoiceDialog#check_widgets (); - let aboutWin = new aboutWin () in - if show then aboutWin#toplevel#show (); - aboutWin#check_widgets (); - let confirmationDialog = new confirmationDialog () in - if show then confirmationDialog#toplevel#show (); - confirmationDialog#check_widgets (); - let toolBarWin = new toolBarWin () in - if show then toolBarWin#toplevel#show (); - toolBarWin#check_widgets (); let fileSelectionWin = new fileSelectionWin () in if show then fileSelectionWin#toplevel#show (); fileSelectionWin#check_widgets (); - let mainWin = new mainWin () in - if show then mainWin#toplevel#show (); - mainWin#check_widgets (); + let emptyDialog = new emptyDialog () in + if show then emptyDialog#toplevel#show (); + emptyDialog#check_widgets (); + let confirmationDialog = new confirmationDialog () in + if show then confirmationDialog#toplevel#show (); + confirmationDialog#check_widgets (); + let browserWin = new browserWin () in + if show then browserWin#toplevel#show (); + browserWin#check_widgets (); + let aboutWin = new aboutWin () in + if show then aboutWin#toplevel#show (); + aboutWin#check_widgets (); if show then GMain.Main.main () ;; diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 8fb25564d..33b9a87f5 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -1,3 +1,190 @@ +class aboutWin : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val aboutDismissButton : GButton.button + val aboutLabel : GMisc.label + val aboutWin : GWindow.dialog_any + val dialog_action_area2 : GPack.button_box + val dialog_vbox2 : GPack.box + val toplevel : GWindow.dialog_any + val xml : Glade.glade_xml Gtk.obj + method aboutDismissButton : GButton.button + method aboutLabel : GMisc.label + method aboutWin : GWindow.dialog_any + method bind : name:string -> callback:(unit -> unit) -> unit + method check_widgets : unit -> unit + method dialog_action_area2 : GPack.button_box + method dialog_vbox2 : GPack.box + method reparent : GObj.widget -> unit + method toplevel : GWindow.dialog_any + method xml : Glade.glade_xml Gtk.obj + end +class browserWin : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val alignment3 : GBin.alignment + val browserBackButton : GButton.button + val browserForwardButton : GButton.button + val browserHomeButton : GButton.button + val browserNewButton : GButton.button + val browserRefreshButton : GButton.button + val browserUri : GEdit.entry + val browserVBox : GPack.box + 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 + val image188 : GMisc.image + val image189 : GMisc.image + val image190 : GMisc.image + val image191 : GMisc.image + val image229 : GMisc.image + val label10 : GMisc.label + val scrolledBrowser : GBin.scrolled_window + val toplevel : GWindow.window + val xml : Glade.glade_xml Gtk.obj + method alignment3 : GBin.alignment + method bind : name:string -> callback:(unit -> unit) -> unit + method browserBackButton : GButton.button + method browserForwardButton : GButton.button + method browserHomeButton : GButton.button + method browserNewButton : GButton.button + method browserRefreshButton : GButton.button + method browserUri : GEdit.entry + method browserVBox : GPack.box + method browserWin : GWindow.window + 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 + method image188 : GMisc.image + method image189 : GMisc.image + method image190 : GMisc.image + method image191 : GMisc.image + method image229 : GMisc.image + method label10 : GMisc.label + method reparent : GObj.widget -> unit + method scrolledBrowser : GBin.scrolled_window + method toplevel : GWindow.window + method xml : Glade.glade_xml Gtk.obj + end +class confirmationDialog : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val confirmationDialog : GWindow.dialog_any + val confirmationDialogCancelButton : GButton.button + val confirmationDialogLabel : GMisc.label + val confirmationDialogOkButton : GButton.button + val dialog_action_area1 : GPack.button_box + val dialog_vbox1 : GPack.box + val toplevel : GWindow.dialog_any + val xml : Glade.glade_xml Gtk.obj + method bind : name:string -> callback:(unit -> unit) -> unit + method check_widgets : unit -> unit + method confirmationDialog : GWindow.dialog_any + method confirmationDialogCancelButton : GButton.button + method confirmationDialogLabel : GMisc.label + method confirmationDialogOkButton : GButton.button + method dialog_action_area1 : GPack.button_box + method dialog_vbox1 : GPack.box + method reparent : GObj.widget -> unit + method toplevel : GWindow.dialog_any + method xml : Glade.glade_xml Gtk.obj + end +class emptyDialog : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val dialog_action_area5 : GPack.button_box + val emptyDialog : GWindow.dialog_any + val emptyDialogCancelButton : GButton.button + val emptyDialogLabel : GMisc.label + val emptyDialogOkButton : GButton.button + val emptyDialogVBox : GPack.box + val toplevel : GWindow.dialog_any + val xml : Glade.glade_xml Gtk.obj + method bind : name:string -> callback:(unit -> unit) -> unit + method check_widgets : unit -> unit + method dialog_action_area5 : GPack.button_box + method emptyDialog : GWindow.dialog_any + method emptyDialogCancelButton : GButton.button + method emptyDialogLabel : GMisc.label + method emptyDialogOkButton : GButton.button + method emptyDialogVBox : GPack.box + method reparent : GObj.widget -> unit + method toplevel : GWindow.dialog_any + method xml : Glade.glade_xml Gtk.obj + end +class fileSelectionWin : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val fileSelCancelButton : GButton.button + val fileSelOkButton : GButton.button + val fileSelectionWin : GWindow.file_selection + val toplevel : GWindow.file_selection + val xml : Glade.glade_xml Gtk.obj + method bind : name:string -> callback:(unit -> unit) -> unit + method check_widgets : unit -> unit + method fileSelCancelButton : GButton.button + method fileSelOkButton : GButton.button + method fileSelectionWin : GWindow.file_selection + method toplevel : GWindow.file_selection + method xml : Glade.glade_xml Gtk.obj + end +class interpChoiceDialog : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val dialog_action_area4 : GPack.button_box + val dialog_vbox4 : GPack.box + val interpChoiceCancelButton : GButton.button + val interpChoiceDialog : GWindow.dialog_any + val interpChoiceDialogLabel : GMisc.label + val interpChoiceHelpButton : GButton.button + val interpChoiceOkButton : GButton.button + val interpChoiceTreeView : GTree.view + val scrolledwindow4 : GBin.scrolled_window + val toplevel : GWindow.dialog_any + val vbox3 : GPack.box + val xml : Glade.glade_xml Gtk.obj + method bind : name:string -> callback:(unit -> unit) -> unit + method check_widgets : unit -> unit + method dialog_action_area4 : GPack.button_box + method dialog_vbox4 : GPack.box + method interpChoiceCancelButton : GButton.button + method interpChoiceDialog : GWindow.dialog_any + method interpChoiceDialogLabel : GMisc.label + method interpChoiceHelpButton : GButton.button + method interpChoiceOkButton : GButton.button + method interpChoiceTreeView : GTree.view + method reparent : GObj.widget -> unit + method scrolledwindow4 : GBin.scrolled_window + method toplevel : GWindow.dialog_any + method vbox3 : GPack.box + method xml : Glade.glade_xml Gtk.obj + end class mainWin : ?file:string -> ?domain:string -> @@ -98,23 +285,92 @@ class mainWin : method viewMenu_menu : GMenu.menu method xml : Glade.glade_xml Gtk.obj end -class fileSelectionWin : +class scriptWin : ?file:string -> ?domain:string -> ?autoconnect:bool -> unit -> object - val fileSelCancelButton : GButton.button - val fileSelOkButton : GButton.button - val fileSelectionWin : GWindow.file_selection - val toplevel : GWindow.file_selection + val handlebox2 : GBin.handle_box + val hbox8 : GPack.box + val image134 : GMisc.image + val image235 : GMisc.image + val image237 : GMisc.image + val image238 : GMisc.image + val image239 : GMisc.image + val label7 : GMisc.label + val label8 : GMisc.label + val outlineTreeView : GTree.view + 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 toplevel : GWindow.window + 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 fileSelCancelButton : GButton.button - method fileSelOkButton : GButton.button - method fileSelectionWin : GWindow.file_selection - method toplevel : GWindow.file_selection + method handlebox2 : GBin.handle_box + method hbox8 : GPack.box + method image134 : GMisc.image + method image235 : GMisc.image + method image237 : GMisc.image + method image238 : GMisc.image + method image239 : GMisc.image + method label7 : GMisc.label + method label8 : GMisc.label + method outlineTreeView : GTree.view + method reparent : GObj.widget -> unit + method scriptNotebook : GPack.notebook + 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 toplevel : GWindow.window + method vbox7 : GPack.box + method xml : Glade.glade_xml Gtk.obj + end +class textDialog : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val hbuttonbox1 : GPack.button_box + val scrolledwindow2 : GBin.scrolled_window + val textDialog : GWindow.dialog_any + val textDialogCancelButton : GButton.button + val textDialogLabel : GMisc.label + val textDialogOkButton : GButton.button + val textDialogTextView : GText.view + val toplevel : GWindow.dialog_any + val vbox5 : GPack.box + val xml : Glade.glade_xml Gtk.obj + method bind : name:string -> callback:(unit -> unit) -> unit + method check_widgets : unit -> unit + method hbuttonbox1 : GPack.button_box + method reparent : GObj.widget -> unit + method scrolledwindow2 : GBin.scrolled_window + method textDialog : GWindow.dialog_any + method textDialogCancelButton : GButton.button + method textDialogLabel : GMisc.label + method textDialogOkButton : GButton.button + method textDialogTextView : GText.view + method toplevel : GWindow.dialog_any + method vbox5 : GPack.box method xml : Glade.glade_xml Gtk.obj end class toolBarWin : @@ -189,56 +445,6 @@ class toolBarWin : method whdButton : GButton.button method xml : Glade.glade_xml Gtk.obj end -class confirmationDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val confirmationDialog : GWindow.dialog_any - val confirmationDialogCancelButton : GButton.button - val confirmationDialogLabel : GMisc.label - val confirmationDialogOkButton : GButton.button - val dialog_action_area1 : GPack.button_box - val dialog_vbox1 : GPack.box - val toplevel : GWindow.dialog_any - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method confirmationDialog : GWindow.dialog_any - method confirmationDialogCancelButton : GButton.button - method confirmationDialogLabel : GMisc.label - method confirmationDialogOkButton : GButton.button - method dialog_action_area1 : GPack.button_box - method dialog_vbox1 : GPack.box - method reparent : GObj.widget -> unit - method toplevel : GWindow.dialog_any - method xml : Glade.glade_xml Gtk.obj - end -class aboutWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val aboutDismissButton : GButton.button - val aboutLabel : GMisc.label - val aboutWin : GWindow.dialog_any - val dialog_action_area2 : GPack.button_box - val dialog_vbox2 : GPack.box - val toplevel : GWindow.dialog_any - val xml : Glade.glade_xml Gtk.obj - method aboutDismissButton : GButton.button - method aboutLabel : GMisc.label - method aboutWin : GWindow.dialog_any - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method dialog_action_area2 : GPack.button_box - method dialog_vbox2 : GPack.box - method reparent : GObj.widget -> unit - method toplevel : GWindow.dialog_any - method xml : Glade.glade_xml Gtk.obj - end class uriChoiceDialog : ?file:string -> ?domain:string -> @@ -297,210 +503,4 @@ class uriChoiceDialog : method vbox2 : GPack.box method xml : Glade.glade_xml Gtk.obj end -class interpChoiceDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val dialog_action_area4 : GPack.button_box - val dialog_vbox4 : GPack.box - val interpChoiceCancelButton : GButton.button - val interpChoiceDialog : GWindow.dialog_any - val interpChoiceDialogLabel : GMisc.label - val interpChoiceHelpButton : GButton.button - val interpChoiceOkButton : GButton.button - val interpChoiceTreeView : GTree.view - val scrolledwindow4 : GBin.scrolled_window - val toplevel : GWindow.dialog_any - val vbox3 : GPack.box - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method dialog_action_area4 : GPack.button_box - method dialog_vbox4 : GPack.box - method interpChoiceCancelButton : GButton.button - method interpChoiceDialog : GWindow.dialog_any - method interpChoiceDialogLabel : GMisc.label - method interpChoiceHelpButton : GButton.button - method interpChoiceOkButton : GButton.button - method interpChoiceTreeView : GTree.view - method reparent : GObj.widget -> unit - method scrolledwindow4 : GBin.scrolled_window - method toplevel : GWindow.dialog_any - method vbox3 : GPack.box - method xml : Glade.glade_xml Gtk.obj - end -class emptyDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val dialog_action_area5 : GPack.button_box - val emptyDialog : GWindow.dialog_any - val emptyDialogCancelButton : GButton.button - val emptyDialogLabel : GMisc.label - val emptyDialogOkButton : GButton.button - val emptyDialogVBox : GPack.box - val toplevel : GWindow.dialog_any - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method dialog_action_area5 : GPack.button_box - method emptyDialog : GWindow.dialog_any - method emptyDialogCancelButton : GButton.button - method emptyDialogLabel : GMisc.label - method emptyDialogOkButton : GButton.button - method emptyDialogVBox : GPack.box - method reparent : GObj.widget -> unit - method toplevel : GWindow.dialog_any - 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 toplevel : GWindow.window - val treeview1 : GTree.view - 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 - method scriptNotebook : GPack.notebook - 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 toplevel : GWindow.window - method treeview1 : GTree.view - method vbox7 : GPack.box - method xml : Glade.glade_xml Gtk.obj - end -class textDialog : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val hbuttonbox1 : GPack.button_box - val scrolledwindow2 : GBin.scrolled_window - val textDialog : GWindow.dialog_any - val textDialogCancelButton : GButton.button - val textDialogLabel : GMisc.label - val textDialogOkButton : GButton.button - val textDialogTextView : GText.view - val toplevel : GWindow.dialog_any - val vbox5 : GPack.box - val xml : Glade.glade_xml Gtk.obj - method bind : name:string -> callback:(unit -> unit) -> unit - method check_widgets : unit -> unit - method hbuttonbox1 : GPack.button_box - method reparent : GObj.widget -> unit - method scrolledwindow2 : GBin.scrolled_window - method textDialog : GWindow.dialog_any - method textDialogCancelButton : GButton.button - method textDialogLabel : GMisc.label - method textDialogOkButton : GButton.button - method textDialogTextView : GText.view - method toplevel : GWindow.dialog_any - method vbox5 : GPack.box - method xml : Glade.glade_xml Gtk.obj - end -class browserWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val alignment3 : GBin.alignment - val browserBackButton : GButton.button - val browserForwardButton : GButton.button - val browserHomeButton : GButton.button - val browserNewButton : GButton.button - val browserRefreshButton : GButton.button - val browserUri : GEdit.entry - val browserVBox : GPack.box - 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 - val image188 : GMisc.image - val image189 : GMisc.image - val image190 : GMisc.image - val image191 : GMisc.image - val image229 : GMisc.image - val label10 : GMisc.label - val scrolledBrowser : GBin.scrolled_window - val toplevel : GWindow.window - val xml : Glade.glade_xml Gtk.obj - method alignment3 : GBin.alignment - method bind : name:string -> callback:(unit -> unit) -> unit - method browserBackButton : GButton.button - method browserForwardButton : GButton.button - method browserHomeButton : GButton.button - method browserNewButton : GButton.button - method browserRefreshButton : GButton.button - method browserUri : GEdit.entry - method browserVBox : GPack.box - method browserWin : GWindow.window - 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 - method image188 : GMisc.image - method image189 : GMisc.image - method image190 : GMisc.image - method image191 : GMisc.image - method image229 : GMisc.image - method label10 : GMisc.label - method reparent : GObj.widget -> unit - method scrolledBrowser : GBin.scrolled_window - method toplevel : GWindow.window - method xml : Glade.glade_xml Gtk.obj - end val check_all : ?show:bool -> unit -> unit diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 04d52cd9e..c1bdfcc77 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -195,7 +195,6 @@ class gui file = end -let instance = - let gui = lazy (new gui (Helm_registry.get "matita.glade_file")) in - fun () -> Lazy.force gui +let gui () = new gui (Helm_registry.get "matita.glade_file") +let instance = singleton gui diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 88e44ea7a..922cc7b9a 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -47,7 +47,7 @@ let uri name = *) let baseuri = lazy (ref ("cic:/matita/" ^ Helm_registry.get "matita.owner")) -let basedir = ref ((Unix.getpwuid (Unix.getuid ())).Unix.pw_dir) ;; +let basedir = lazy (ref (Helm_registry.get "matita.basedir")) let qualify name = let baseuri = !(Lazy.force baseuri) in @@ -69,6 +69,7 @@ class virtual interpreterState = val dbd = MatitaMisc.dbd_instance () val currentProof = MatitaProof.instance () + val disambiguator = MatitaDisambiguator.instance () (** eval a toplevel phrase in the current state and return the new state *) @@ -105,7 +106,6 @@ class virtual interpreterState = (** Implements phrases that should be accepted in all states *) class sharedState - ~(disambiguator: MatitaTypes.disambiguator) ~(console: #MatitaTypes.console) ?(mathViewer: MatitaTypes.mathViewer option) () @@ -128,11 +128,12 @@ class sharedState !(Lazy.force baseuri)); Quiet | TacticAst.Command (TacticAst.Basedir (Some path)) -> - basedir := path; + Lazy.force basedir := path; console#echo_message (sprintf "base dir set to \"%s\"" path); Quiet | TacticAst.Command (TacticAst.Basedir None) -> - console#echo_message (sprintf "base dir is \"%s\"" !basedir); + console#echo_message (sprintf "base dir is \"%s\"" + !(Lazy.force basedir)); Quiet | TacticAst.Command (TacticAst.Check term) -> let (_, _, term,ugraph) = @@ -253,9 +254,7 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) = let cicIndTypes = List.rev cicIndTypes in (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) -let - save_object_to_disk uri obj -= +let save_object_to_disk uri obj = let ensure_path_exists path = let dir = Filename.dirname path in try @@ -275,7 +274,6 @@ let let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in - (* prepare XML *) let xml, bodyxml = Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false @@ -285,31 +283,28 @@ let Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false in - (* prepare URIs and paths *) let innertypesuri = UriManager.innertypesuri_of_uri uri in let bodyuri = UriManager.bodyuri_of_uri uri in let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri innertypesuri) ^ ".xml" in - let innertypespath = !basedir ^ "/" ^ innertypesfilename in - let xmlfilename = Str.replace_first (Str.regexp "^cic:") "" + let innertypespath = !(Lazy.force basedir) ^ "/" ^ innertypesfilename in + let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri uri) ^ ".xml" in - let xmlpath = !basedir ^ "/" ^ xmlfilename in - let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:") "" + let xmlpath = !(Lazy.force basedir) ^ "/" ^ xmlfilename in + let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri uri) ^ ".body.xml" in - let xmlbodypath = !basedir ^ "/" ^ xmlbodyfilename in - let path_scheme_of path = "file:/" ^ path in - + let xmlbodypath = !(Lazy.force basedir) ^ "/" ^ xmlbodyfilename in + let path_scheme_of path = "file://" ^ path in + MatitaMisc.mkdirs (List.map Filename.dirname [innertypespath; xmlpath]); (* now write to disk *) ensure_path_exists innertypespath; Xml.pp ~quiet:true xmlinnertypes (Some innertypespath) ; ensure_path_exists xmlpath; Xml.pp ~quiet:true xml (Some xmlpath) ; - (* now register to the getter *) Http_getter.register' innertypesuri (path_scheme_of innertypespath); Http_getter.register' uri (path_scheme_of xmlpath); - (* now the optional body, both write and register *) (match bodyxml,bodyuri with None,None -> () @@ -318,13 +313,8 @@ let Xml.pp ~quiet:true bodyxml (Some xmlbodypath) ; Http_getter.register' bodyuri (path_scheme_of xmlbodypath) | _-> assert false) -;; - - - (* TODO Zack a lot more to be done here: - * - save object to disk in xml format - * - register uri to the getter + (* TODO ZACK a lot more to be done here: * - save universe file *) let add_constant_to_world ~(console: #MatitaTypes.console) ~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph () @@ -337,8 +327,7 @@ let add_constant_to_world ~(console: #MatitaTypes.console) let obj = Cic.Constant (name, body, ty, params, attrs) in let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.add_type_checked_term uri (obj, ugraph); - MetadataDb.index_constant ~dbd - ~owner:(Helm_registry.get "matita.owner") ~uri ~body ~ty; + MetadataDb.index_constant ~dbd ~uri ~body ~ty; save_object_to_disk uri obj; console#echo_message (sprintf "%s constant defined" suri) end @@ -354,8 +343,7 @@ let add_inductive_def_to_world ~(console: #MatitaTypes.console) let obj = Cic.InductiveDefinition (indTypes, params, leftno, attrs) in let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in CicEnvironment.put_inductive_definition uri (obj, ugraph); - MetadataDb.index_inductive_def ~dbd - ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes; + MetadataDb.index_inductive_def ~dbd ~uri ~types:indTypes; save_object_to_disk uri obj; console#echo_message (sprintf "%s inductive type defined" suri); let elim sort = @@ -377,13 +365,8 @@ let add_inductive_def_to_world ~(console: #MatitaTypes.console) end (** Implements phrases that should be accepted only in Command state *) -class commandState - ~(disambiguator: MatitaTypes.disambiguator) - ~(console: #MatitaTypes.console) - ?mathViewer - () -= - let shared = new sharedState ~disambiguator ~console ?mathViewer () in +class commandState ~(console: #MatitaTypes.console) ?mathViewer () = + let shared = new sharedState ~console ?mathViewer () in object (self) inherit interpreterState ~console @@ -532,13 +515,8 @@ let namer_of names = (** Implements phrases that should be accepted only in Proof state, basically * tacticals *) -class proofState - ~(disambiguator: MatitaTypes.disambiguator) - ~(console: #MatitaTypes.console) - ?mathViewer - () -= - let shared = new sharedState ~disambiguator ~console ?mathViewer () in +class proofState ~(console: #MatitaTypes.console) ?mathViewer () = + let shared = new sharedState ~console ?mathViewer () in object (self) inherit interpreterState ~console @@ -634,14 +612,9 @@ class proofState | tactical -> shared#evalTactical tactical end -class interpreter - ~(disambiguator: MatitaTypes.disambiguator) - ~(console: #MatitaTypes.console) - ?mathViewer - () -= - let commandState = new commandState ~disambiguator ~console ?mathViewer () in - let proofState = new proofState ~disambiguator ~console ?mathViewer () in +class interpreter ~(console: #MatitaTypes.console) ?mathViewer () = + let commandState = new commandState ~console ?mathViewer () in + let proofState = new proofState ~console ?mathViewer () in object (self) val mutable state = commandState @@ -667,11 +640,6 @@ 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 () +let interpreter ~(console: #MatitaTypes.console) ?mathViewer () = + new interpreter ~console ?mathViewer () diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli index 2b0ad56da..a6da315ba 100644 --- a/helm/matita/matitaInterpreter.mli +++ b/helm/matita/matitaInterpreter.mli @@ -26,7 +26,6 @@ exception Command_error of string val interpreter: - disambiguator:MatitaTypes.disambiguator -> console:#MatitaTypes.console -> ?mathViewer:MatitaTypes.mathViewer -> unit -> diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 626e45634..e572f0982 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -265,11 +265,7 @@ exception Browser_failure of string let cicBrowsers = ref [] -class cicBrowser - ~(disambiguator:MatitaTypes.disambiguator) - ~(history:string MatitaMisc.history) - () -= +class cicBrowser ~(history:string MatitaMisc.history) () = let term_RE = Pcre.regexp "^term:(.*)" in let gui = MatitaGui.instance () in let win = gui#newBrowserWin () in @@ -310,6 +306,7 @@ class cicBrowser self#_loadUri ~add_to_history:false blank_uri; toplevel#show (); + val disambiguator = MatitaDisambiguator.instance () val currentProof = MatitaProof.instance () val mutable current_uri = "" @@ -426,10 +423,10 @@ let sequents_viewer ~(notebook:GPack.notebook) = new sequents_viewer ~notebook ~sequent_viewer ~set_goal () -let cicBrowser ~disambiguator () = +let cicBrowser () = let size = BuildTimeConf.browser_history_size in let rec aux history = - let browser = new cicBrowser ~disambiguator ~history () in + let browser = new cicBrowser ~history () in let win = browser#win in ignore (win#browserNewButton#connect#clicked (fun () -> let history = @@ -450,12 +447,12 @@ let cicBrowser ~disambiguator () = let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers -class mathViewer ~disambiguator = +class mathViewer = object method checkTerm (src:MatitaTypes.term_source) = - let browser = cicBrowser ~disambiguator () in - browser#loadTerm src + (cicBrowser ())#loadTerm src end -let mathViewer ~disambiguator () = new mathViewer ~disambiguator +let mathViewer () = new mathViewer +let instance = MatitaMisc.singleton mathViewer diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index cdc9a8d65..66508b631 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -83,15 +83,9 @@ val sequents_viewer: unit -> sequents_viewer -val cicBrowser: - disambiguator:MatitaTypes.disambiguator -> - unit -> - MatitaTypes.cicBrowser +val cicBrowser: unit -> MatitaTypes.cicBrowser val refresh_all_browsers: unit -> unit -val mathViewer: - disambiguator:MatitaTypes.disambiguator -> - unit -> - MatitaTypes.mathViewer +val mathViewer: unit -> MatitaTypes.mathViewer diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index dd84abcbd..0bb2ea7e0 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -140,3 +140,9 @@ let dbd_instance = in fun () -> Lazy.force dbd +let singleton f = + let instance = lazy (f ()) in + fun () -> Lazy.force instance + +let mkdirs = List.iter (fun d -> ignore (Unix.system ("mkdir -p " ^ d))) + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 36318dc1f..a0d19b8b2 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -66,6 +66,13 @@ 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 + (** create a singleton from a given function. Given function is invoked the + * first time it gets called. Next invocation will return first value *) +val singleton: (unit -> 'a) -> (unit -> 'a) + + (** create a list of directories, building also parents as needed *) +val mkdirs: string list -> unit + (** {2 db handling} *) val dbd_instance: unit -> Mysql.dbd diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index 9afb90a71..99214e724 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -151,7 +151,5 @@ 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 +let instance = MatitaMisc.singleton currentProof diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 5d6b8e99d..8f59d3fc9 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -77,14 +77,26 @@ class type console = method wrap_exn : 'a. (unit -> 'a) -> 'a option end +type choose_uris_callback = + selection_mode:[`MULTIPLE|`SINGLE] -> + ?title:string -> ?msg:string -> ?nonvars_button:bool -> + string list -> + string list +type choose_interp_callback = (string * string) list list -> int list + class type disambiguator = object - method parserr: parserr - method setParserr: parserr -> unit - method env: DisambiguateTypes.environment method setEnv: DisambiguateTypes.environment -> unit + method chooseUris: choose_uris_callback + method setChooseUris: choose_uris_callback -> unit + + method chooseInterp: choose_interp_callback + method setChooseInterp: choose_interp_callback -> unit + + method parserr: parserr + method disambiguateTerm: ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?env:DisambiguateTypes.environment -> @@ -165,13 +177,6 @@ type mml_of_cic_object = type namer = ProofEngineTypes.mk_fresh_name_type -type choose_uris_callback = - selection_mode:[`MULTIPLE|`SINGLE] -> - ?title:string -> ?msg:string -> ?nonvars_button:bool -> - string list -> - string list -type choose_interp_callback = (string * string) list list -> int list - let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ = raise (Failure "ambiguous input") let mono_interp_callback _ = raise (Failure "ambiguous input") diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index b165740aa..99e69f6e1 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -43,6 +43,22 @@ val explain: exn -> string val unopt_uri : 'a option -> 'a + (** {3 disambiguator callbacks} *) + +type choose_uris_callback = + selection_mode:[ `MULTIPLE | `SINGLE ] -> + ?title:string -> + ?msg:string -> ?nonvars_button:bool -> string list -> string list + +type choose_interp_callback = (string * string) list list -> int list + + (** @raise Failure if called, use if unambiguous input is required *) +val mono_uris_callback: choose_uris_callback + (** @raise Failure if called, use if unambiguous input is required *) +val mono_interp_callback: choose_interp_callback + +(** {2 major matita objects} *) + class type parserr = object method parseTactical : char Stream.t -> DisambiguateTypes.tactical @@ -60,12 +76,17 @@ class type console = class type disambiguator = object - method parserr : parserr - method setParserr : parserr -> unit - method env : DisambiguateTypes.environment method setEnv : DisambiguateTypes.environment -> unit + method chooseUris: choose_uris_callback + method setChooseUris: choose_uris_callback -> unit + + method chooseInterp: choose_interp_callback + method setChooseInterp: choose_interp_callback -> unit + + method parserr: parserr + (* TODO Zack: as long as matita doesn't support MDI inteface, * disambiguateTerm will return a single term *) (** @param env disambiguation environment. If this parameter is given the @@ -188,17 +209,3 @@ type mml_of_cic_object = type namer = ProofEngineTypes.mk_fresh_name_type - (** {3 disambiguator callbacks} *) - -type choose_uris_callback = - selection_mode:[ `MULTIPLE | `SINGLE ] -> - ?title:string -> - ?msg:string -> ?nonvars_button:bool -> string list -> string list - -type choose_interp_callback = (string * string) list list -> int list - - (** @raise Failure if called, use if unambiguous input is required *) -val mono_uris_callback: choose_uris_callback - (** @raise Failure if called, use if unambiguous input is required *) -val mono_interp_callback: choose_interp_callback - diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index c29b50779..2ae1c8d68 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -57,7 +57,12 @@ let usage = sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:" BuildTimeConf.version -let _ = Helm_registry.load_from "matita.conf.xml" +let _ = + Helm_registry.load_from "matita.conf.xml"; + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment () let scripts = let acc = ref [] in @@ -65,25 +70,8 @@ let scripts = Arg.parse arg_spec add_script usage; List.rev !acc -let parserr = new MatitaDisambiguator.parserr () -let dbd = - Mysql.quick_connect - ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") - ~database:(Helm_registry.get "db.database") - () - -let owner = (Helm_registry.get "matita.owner") ;; -let _ = MetadataTypes.ownerize_tables owner ;; -let _ = MatitaDb.clean_owner_environment dbd owner ;; -let _ = MatitaDb.create_owner_environment dbd owner ;; - -let disambiguator = - new MatitaDisambiguator.disambiguator ~parserr ~dbd - ~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback - () let console = new tty_console -let interpreter = MatitaInterpreter.interpreter ~disambiguator ~console () +let interpreter = MatitaInterpreter.interpreter ~console () let run_script fname = message (sprintf "execution of %s started:" fname);