]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.mli
added support for coercions
[helm.git] / helm / matita / matitaGui.mli
index aabcba1e8805441cd1c6cdd5bd1327e9ae91a4d9..f517bbb9cb3c59415cc6e87933e353af687e3ec5 100644 (file)
@@ -69,6 +69,8 @@ object
     (** prompt the user for a (multiline) text entry *)
   method askText: ?title:string -> ?msg:string -> unit -> string option
 
+  method loadScript: string -> unit
+                                                            
 end
 
   (** singleton instance of the gui *)
@@ -84,7 +86,10 @@ val instance: unit -> gui
     * @raise MatitaTypes.Cancel *)
 val interactive_uri_choice:
   ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string ->
-  ?msg:string -> ?nonvars_button:bool -> unit ->
+  ?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 *)