First steps towards a multi-document interface.

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

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index de95aac52ce9618500c05f5ed030aa5292a01843..02e06d2d14b2a129b57929daa4c7c81ec0a8155a 100644 (file)
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -59,7 +59,6 @@ object
   method loadFromFile : string -> unit
   method loadFromString : string -> unit
   method saveToFile : unit -> unit
-  method filename : string
 
   (** {2 Current proof} (if any) *)
 
@@ -74,6 +73,7 @@ object
 
   (** misc *)
   method clean_dirty_lock: unit
+  method set_star: bool -> unit
   
   (* debug *)
   method dump : unit -> unit
@@ -81,14 +81,11 @@ object
 
 end
 
-  (** @param set_star callback used to set the modified symbol (usually a star
-   * "*") on the side of a script name *)
 val script: 
   source_view:GSourceView2.source_view -> 
   urichooser: (NReference.reference list -> NReference.reference list) -> 
   ask_confirmation: 
     (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> 
-  set_star: (bool -> unit) ->
   unit -> 
     script