]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.mli
- handles about:* uris in cicBrowser
[helm.git] / helm / matita / matitaGui.mli
index cb2cbeb0c00ef46775cb549b4d54b8d62d7d538c..674f3702cec56241bfd6d10af607e2f0ef394dc6 100644 (file)
@@ -34,6 +34,12 @@ object
   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
@@ -53,7 +59,7 @@ object
      * methods below create a new window on each invocation. You should
      * remember to destroy windows after use *)
 
-  method newBrowserWin:         unit -> MatitaGeneratedGui.browserWin
+  method newBrowserWin:         unit -> browserWin
   method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
   method newInterpDialog:       unit -> MatitaGeneratedGui.interpChoiceDialog
   method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
@@ -88,6 +94,7 @@ 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