VERY EXPERIMENTAL:

[helm.git] / matita / matita / matitaGuiTypes.mli

diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli
index 8e3932b04a1882dad615859a769bf52a4ce47f18..fa62970cef6c0835a74561ff0fcf23e59d02955e 100644 (file)
--- a/matita/matita/matitaGuiTypes.mli
+++ b/matita/matita/matitaGuiTypes.mli
@@ -71,6 +71,7 @@ object
     (** prompt the user for a (multiline) text entry *)
   method askText: ?title:string -> ?msg:string -> unit -> string option
 
+  method newScript: unit -> unit
   method loadScript: string -> unit
 end