X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.mli;h=6f9601f710475b740fa1529dd9549850ee5f5bfd;hb=57b43a967eaf3b0747350cd775d4301a53af2820;hp=dfb93cd1880248fd8df732a2a395edc950b8055e;hpb=142d3076f2a4dc17d9045c2bba4d4b01eddfd008;p=helm.git

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index dfb93cd18..6f9601f71 100644
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -23,59 +23,91 @@
  * http://helm.cs.unibo.it/
  *)
 
-(*
-class type stringListModel =
-  object
-    method clear: unit -> unit
-    method append: string -> unit
-  end
-*)
+class type console =
+object
+  method message: string -> unit
+  method error: string -> unit
+  method warning: string -> unit
+  method debug: string -> unit
+  method clear: unit -> unit
 
-  (** @param fname name of the Glade file describing the GUI *)
-class gui :
-  string ->
-  object
+  method log_callback: MatitaLog.log_callback
+end
+
+class type browserWin =
+object
+  inherit MatitaGeneratedGui.browserWin
+  method browserUri: GEdit.combo_box_entry
+end
 
-    method setQuitCallback    : (unit -> unit) -> unit
-    method setPhraseCallback  : (string -> bool) -> unit
+  (** @param fname name of the Glade file describing the GUI *)
+class type gui =
+object
 
-      (** {2 Access to lower-level GTK widgets} *)
+  method setQuitCallback    : (unit -> unit) -> unit
 
-    method about :        MatitaGeneratedGui.aboutWin
-    method check :        MatitaGeneratedGui.checkWin
-    method fileSel :      MatitaGeneratedGui.fileSelectionWin
-    method main :         MatitaGeneratedGui.mainWin
-    method proof :        MatitaGeneratedGui.proofWin
-    method script:        MatitaGeneratedGui.scriptWin
-    method toolbar :      MatitaGeneratedGui.toolBarWin
+    (** {2 Access to singleton instances of lower-level GTK widgets} *)
 
-      (** {2 Access to GUI useful components} *)
+  method about :        MatitaGeneratedGui.aboutWin
+  method fileSel :      MatitaGeneratedGui.fileSelectionWin
+  method main :         MatitaGeneratedGui.mainWin
+  method findRepl :     MatitaGeneratedGui.findReplWin
+(*   method toolbar :      MatitaGeneratedGui.toolBarWin *)
 
-    method console:       MatitaConsole.console
+  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 *)
+    (** {2 Dialogs instantiation}
+     * methods below create a new window on each invocation. You should
+     * remember to destroy windows after use *)
 
-    method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
-    method newInterpDialog:       unit -> MatitaGeneratedGui.interpChoiceDialog
-    method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
-    method newEmptyDialog:        unit -> MatitaGeneratedGui.emptyDialog
+  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} *)
+    (** {2 Utility methods} *)
 
-      (** ask the used to choose a file with the file chooser *)
-    method chooseFile: unit -> string option
+    (** 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
 
-      (** prompt the user for a (multiline) text entry *)
-    method askText: ?title:string -> ?msg:string -> unit -> string option
+    (** prompt the user for a (multiline) text entry *)
+  method askText: ?title:string -> ?msg:string -> unit -> string option
 
-      (** lock script text view from the beginning to the given offset (in UTF-8
-      * characters) *)
-    method lockScript: int -> unit
+  method loadScript: string -> unit
+  method setStar: string -> bool -> unit
 
-  end
+    (** {3 Fonts} *)
+  method increaseFontSize: unit -> unit
+  method decreaseFontSize: unit -> unit
+  method resetFontSize: unit -> unit
+                                                            
+end
 
   (** singleton instance of the gui *)
 val instance: unit -> gui
 
+  (** {2 Disambiguation callbacks}
+  * Use singleton gui instance. *)
+
+  (** @param selection_mode selection mode in uri list, default to `MULTIPLE
+    * @param title window title, defaults to ""
+    * @param msg message for the user, defaults to ""
+    * @param nonvars_button enable button to exclude vars?, defaults to false
+    * @raise MatitaTypes.Cancel *)
+val interactive_uri_choice:
+  ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string ->
+  ?msg:string -> ?nonvars_button:bool -> 
+  ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string ->
+  ?ok_action:[`AUTO|`SELECT] ->
+  ?copy_cb:(string -> unit) -> unit ->
+    MatitaDisambiguator.choose_uris_callback
+
+  (** @raise MatitaTypes.Cancel *)
+val interactive_interp_choice:
+  unit ->
+    MatitaDisambiguator.choose_interp_callback
+