-matita.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \
- matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo
-matita.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \
- matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx
+matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
+ matitacleanLib.cmi
+matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
+ matitacleanLib.cmi
+matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
+ buildTimeConf.cmo
+matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
+ buildTimeConf.cmx
+matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \
+ matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi matitaDb.cmi \
+ buildTimeConf.cmo matitacLib.cmi
+matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \
+ matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \
+ buildTimeConf.cmx matitacLib.cmi
+matitac.cmo: matitacLib.cmi
+matitac.cmx: matitacLib.cmx
matitaDb.cmo: matitaMisc.cmi matitaDb.cmi
matitaDb.cmx: matitaMisc.cmx matitaDb.cmi
+matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo
+matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx
matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \
buildTimeConf.cmx matitaGui.cmi
matitaLog.cmo: matitaLog.cmi
matitaLog.cmx: matitaLog.cmi
+matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \
+ matitamakeLib.cmi
+matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \
+ matitamakeLib.cmi
+matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo
+matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx
matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
matitaGui.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \
matitaMathView.cmi
buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \
buildTimeConf.cmx matitaMisc.cmi
+matita.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
+ matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \
+ matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo
+matita.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
+ matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \
+ matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx
matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \
matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo matitaScript.cmi
matitaSync.cmi
matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi
matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi
-matitac.cmo: matitacLib.cmi
-matitac.cmx: matitacLib.cmx
-matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaLog.cmi matitaExcPp.cmi matitaEngine.cmi matitaDb.cmi \
- buildTimeConf.cmo matitacLib.cmi
-matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \
- matitaLog.cmx matitaExcPp.cmx matitaEngine.cmx matitaDb.cmx \
- buildTimeConf.cmx matitacLib.cmi
-matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
- buildTimeConf.cmo
-matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
- buildTimeConf.cmx
-matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
- matitacleanLib.cmi
-matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
- matitacleanLib.cmi
-matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi buildTimeConf.cmo
-matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx
-matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo
-matitamake.cmx: matitamakeLib.cmx buildTimeConf.cmx
-matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \
- matitamakeLib.cmi
-matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \
- matitamakeLib.cmi
matitaDisambiguator.cmi: matitaTypes.cmi
matitaEngine.cmi: matitaTypes.cmi
matitaGtkMisc.cmi: matitaGeneratedGui.cmi
-matitaGui.cmi: matitaLog.cmi matitaGeneratedGui.cmi matitaDisambiguator.cmi
+matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi
+matitaGuiTypes.cmi: matitaLog.cmi matitaGeneratedGui.cmi
matitaMathView.cmi: matitaTypes.cmi
matitaMisc.cmi: matitaTypes.cmi
matitaScript.cmi: matitaTypes.cmi
matitaScript.cmo \
matitaGeneratedGui.cmo \
matitaGtkMisc.cmo \
- matitaGui.cmo \
matitaMathView.cmo \
+ matitaGui.cmo \
$(NULL)
# objects for matitac (batch compiler)
CCMOS = \
open MatitaTypes
open MatitaMisc
-
(* ALB to link paramodulation... *)
let _ = Paramodulation.Saturation.init ()
-
(** {2 Initialization} *)
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
MatitaDb.create_owner_environment ();
MatitamakeLib.initialize ();
- GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
- GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
- ignore (GMain.Main.init ());
CicEnvironment.set_trust (* environment trust *)
(let trust = Helm_registry.get_bool "matita.environment_trust" in
fun _ -> trust)
let gui = MatitaGui.instance ()
-let _ =
- ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
- ignore (MatitaMathView.cicBrowser ())));
- (* font sizes *)
- ignore (gui#main#increaseFontSizeMenuItem#connect#activate (fun _ ->
- gui#increaseFontSize ();
- MatitaMathView.increase_font_size ();
- MatitaMathView.update_font_sizes ()));
- ignore (gui#main#decreaseFontSizeMenuItem#connect#activate (fun _ ->
- gui#decreaseFontSize ();
- MatitaMathView.decrease_font_size ();
- MatitaMathView.update_font_sizes ()));
- ignore (gui#main#normalFontSizeMenuItem#connect#activate (fun _ ->
- gui#resetFontSize ();
- MatitaMathView.reset_font_size ();
- MatitaMathView.update_font_sizes ()));
- MatitaMathView.reset_font_size ();
- (* disambiguator callback *)
- MatitaDisambiguator.set_choose_uris_callback
- (MatitaGui.interactive_uri_choice ());
- MatitaDisambiguator.set_choose_interp_callback
- (MatitaGui.interactive_interp_choice ())
-
let script =
let s =
MatitaScript.script
gui#sourceView#source_buffer#end_not_undoable_action ();
s
-
(* math viewers *)
let _ =
let sequent_viewer = MatitaMathView.sequentViewer_instance () in
let clipboard =
let atom = Gdk.Atom.clipboard in
GData.clipboard atom in
- ignore(self#main#editMenu#connect#activate
+ ignore (self#main#editMenu#connect#activate
~callback:
(fun () ->
let something_selected =
clean_locked := false;
(MatitaScript.instance ())#clean_dirty_lock;
clean_locked := true
- end))
+ end));
+ (* math view handling *)
+ connect_menu_item main#newCicBrowserMenuItem (fun () ->
+ ignore (MatitaMathView.cicBrowser ()));
+ connect_menu_item main#increaseFontSizeMenuItem (fun () ->
+ self#increaseFontSize ();
+ MatitaMathView.increase_font_size ();
+ MatitaMathView.update_font_sizes ());
+ connect_menu_item main#decreaseFontSizeMenuItem (fun () ->
+ self#decreaseFontSize ();
+ MatitaMathView.decrease_font_size ();
+ MatitaMathView.update_font_sizes ());
+ connect_menu_item main#normalFontSizeMenuItem (fun () ->
+ self#resetFontSize ();
+ MatitaMathView.reset_font_size ();
+ MatitaMathView.update_font_sizes ());
+ MatitaMathView.reset_font_size ();
method loadScript file =
let script = MatitaScript.instance () in
let gui () =
let g = new gui () in
gui_instance := Some g;
+ MatitaMathView.set_gui g;
g
let instance = singleton gui
GtkThread.main ();
(match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
+let _ =
+ (* disambiguator callbacks *)
+ MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
+ MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+ (* gtk initialization *)
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
+ GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
+ ignore (GMain.Main.init ())
+
* http://helm.cs.unibo.it/
*)
-class type console =
-object
- method message: string -> unit
- method error: string -> unit
- method warning: string -> unit
- method debug: string -> unit
- method clear: unit -> unit
-
- method log_callback: MatitaLog.log_callback
-end
-
-class type browserWin =
-object
- inherit MatitaGeneratedGui.browserWin
- method browserUri: GEdit.combo_box_entry
-end
-
- (** @param fname name of the Glade file describing the GUI *)
-class type gui =
-object
-
- method setQuitCallback : (unit -> unit) -> unit
-
- (** {2 Access to singleton instances of lower-level GTK widgets} *)
-
- method fileSel : MatitaGeneratedGui.fileSelectionWin
- method main : MatitaGeneratedGui.mainWin
- method findRepl : MatitaGeneratedGui.findReplWin
- method develList: MatitaGeneratedGui.develListWin
- method newDevel: MatitaGeneratedGui.newDevelWin
-(* method toolbar : MatitaGeneratedGui.toolBarWin *)
-
- method console: console
- method sourceView: GSourceView.source_view
-
- (** {2 Dialogs instantiation}
- * methods below create a new window on each invocation. You should
- * remember to destroy windows after use *)
-
- method newBrowserWin: unit -> browserWin
- method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
- method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
- method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
- method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
-
- (** {2 Utility methods} *)
-
- (** ask the used to choose a file with the file chooser
- * @param ok_not_exists if set to true returns also non existent files
- * (useful for save). Defaults to false *)
- method chooseFile: ?ok_not_exists:bool -> unit -> string option
- method createDevelopment: containing:string option -> unit
-
- (** prompt the user for a (multiline) text entry *)
- method askText: ?title:string -> ?msg:string -> unit -> string option
-
- method loadScript: string -> unit
- method setStar: string -> bool -> unit
-
- (** {3 Fonts} *)
- method increaseFontSize: unit -> unit
- method decreaseFontSize: unit -> unit
- method resetFontSize: unit -> unit
-
-end
-
(** singleton instance of the gui *)
-val instance: unit -> gui
+val instance: unit -> MatitaGuiTypes.gui
(** {2 Disambiguation callbacks}
* Use singleton gui instance. *)
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+class type console =
+object
+ method message: string -> unit
+ method error: string -> unit
+ method warning: string -> unit
+ method debug: string -> unit
+ method clear: unit -> unit
+
+ method log_callback: MatitaLog.log_callback
+end
+
+class type browserWin =
+object
+ inherit MatitaGeneratedGui.browserWin
+ method browserUri: GEdit.combo_box_entry
+end
+
+class type gui =
+object
+ method setQuitCallback : (unit -> unit) -> unit
+
+ (** {2 Access to singleton instances of lower-level GTK widgets} *)
+
+ method fileSel : MatitaGeneratedGui.fileSelectionWin
+ method main : MatitaGeneratedGui.mainWin
+ method findRepl : MatitaGeneratedGui.findReplWin
+ method develList: MatitaGeneratedGui.develListWin
+ method newDevel: MatitaGeneratedGui.newDevelWin
+(* method toolbar : MatitaGeneratedGui.toolBarWin *)
+
+ method console: console
+ method sourceView: GSourceView.source_view
+
+ (** {2 Dialogs instantiation}
+ * methods below create a new window on each invocation. You should
+ * remember to destroy windows after use *)
+
+ method newBrowserWin: unit -> browserWin
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
+ method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
+
+ (** {2 Utility methods} *)
+
+ (** ask the used to choose a file with the file chooser
+ * @param ok_not_exists if set to true returns also non existent files
+ * (useful for save). Defaults to false *)
+ method chooseFile: ?ok_not_exists:bool -> unit -> string option
+ method createDevelopment: containing:string option -> unit
+
+ (** prompt the user for a (multiline) text entry *)
+ method askText: ?title:string -> ?msg:string -> unit -> string option
+
+ method loadScript: string -> unit
+ method setStar: string -> bool -> unit
+
+ (** {3 Fonts} *)
+ method increaseFontSize: unit -> unit
+ method decreaseFontSize: unit -> unit
+ method resetFontSize: unit -> unit
+end
+
+ (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions
+ * are handled internally. Hyperlinks are handled by calling an user provided
+ * callback *)
+class type clickableMathView =
+object
+ inherit GMathViewAux.multi_selection_math_view
+
+ (** set hyperlink callback. None disable hyperlink handling *)
+ method set_href_callback: (string -> unit) option -> unit
+
+ method string_of_selected_terms: string
+
+ method update_font_size: unit
+end
+
+class type sequentViewer =
+object
+ inherit clickableMathView
+
+ (** load a sequent and render it into parent widget *)
+ method load_sequent: Cic.metasenv -> int -> unit
+end
+
+class type sequentsViewer =
+object
+ method reset: unit
+ method load_sequents: ProofEngineTypes.status -> unit
+ method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
+end
+
+class type cicBrowser =
+object
+ method load: MatitaTypes.mathViewer_entry -> unit
+ (* method loadList: string list -> MatitaTypes.mathViewer_entry -> unit *)
+ method loadInput: string -> unit
+end
+
end
let cicBrowsers = ref []
+let gui_instance = ref None
+let set_gui gui = gui_instance := Some gui
+let get_gui () =
+ match !gui_instance with
+ | None -> assert false
+ | Some gui -> gui
let default_font_size () =
Helm_registry.get_opt_default Helm_registry.int
let href_ds = Gdome.domString "href"
let xref_ds = Gdome.domString "xref"
-
class clickableMathView obj =
let text_width = 80 in
object (self)
let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in
let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
- let gui = MatitaGui.instance () in
- let win = gui#newBrowserWin () in
+ let gui = get_gui () in
+ let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
let combo,_ = GEdit.combo_box_text ~strings:queries () in
let activate_combo_query input q =
let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer
let default_sequentsViewer () =
- let gui = MatitaGui.instance () in
+ let gui = get_gui () in
let sequentViewer = sequentViewer_instance () in
sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer ()
let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
* http://helm.cs.unibo.it/
*)
- (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions
- * are handled internally. Hyperlinks are handled by calling an user provided
- * callback *)
-class type clickableMathView =
- object
- inherit GMathViewAux.multi_selection_math_view
-
- (** set hyperlink callback. None disable hyperlink handling *)
- method set_href_callback: (string -> unit) option -> unit
-
- method string_of_selected_terms: string
-
- method update_font_size: unit
- end
-
-class type sequentViewer =
- object
- inherit clickableMathView
-
-(* |+* @return the list of selected terms. Selections which are not terms are
- * ignored +|
- method get_selected_terms: Cic.term list
-
- |+* @return the list of selected hypothese. Selections which are not
- * hypotheses are ignored +|
- method get_selected_hypotheses: Cic.hypothesis list *)
-
- (** load a sequent and render it into parent widget *)
- method load_sequent: Cic.metasenv -> int -> unit
- end
-
-class type sequentsViewer =
- object
- method reset: unit
- method load_sequents: ProofEngineTypes.status -> unit
- method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
- end
-
-class type cicBrowser =
-object
- method load: MatitaTypes.mathViewer_entry -> unit
- (* method loadList: string list -> MatitaTypes.mathViewer_entry -> unit *)
- method loadInput: string -> unit
-end
-
(** {2 Constructors} *)
(** meta constructor *)
unit ->
'widget
-val clickableMathView: clickableMathView constructor
+val clickableMathView: MatitaGuiTypes.clickableMathView constructor
-val sequentViewer: sequentViewer constructor
+val sequentViewer: MatitaGuiTypes.sequentViewer constructor
val sequentsViewer:
notebook:GPack.notebook ->
- sequentViewer:sequentViewer ->
+ sequentViewer:MatitaGuiTypes.sequentViewer ->
unit ->
- sequentsViewer
+ MatitaGuiTypes.sequentsViewer
-val cicBrowser: unit -> cicBrowser
+val cicBrowser: unit -> MatitaGuiTypes.cicBrowser
-(** mathview wide functions *)
+(** {2 Mathview wide functions} *)
-val increase_font_size: unit -> unit
-val decrease_font_size: unit -> unit
-val reset_font_size: unit -> unit
+val increase_font_size: unit -> unit
+val decrease_font_size: unit -> unit
+val reset_font_size: unit -> unit
val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *)
-val update_font_sizes: unit -> unit
+val update_font_sizes: unit -> unit
+
+(** {2 Singleton instances} *)
+
+val sequentViewer_instance: unit -> MatitaGuiTypes.sequentViewer
+val sequentsViewer_instance: unit -> MatitaGuiTypes.sequentsViewer
-(** {2 singleton instances} *)
+val mathViewer: unit -> MatitaTypes.mathViewer
-val sequentViewer_instance: unit -> sequentViewer
-val sequentsViewer_instance: unit -> sequentsViewer
+(** {2 Initialization} *)
-val mathViewer: unit -> MatitaTypes.mathViewer
+val set_gui: MatitaGuiTypes.gui -> unit
projects / helm.git / commitdiff