When switching to a new script, the other parts of the interface are

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

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index 5e8658d3fc184493f99af6cfc7b28942e00ffc9a..28f415ab2aa947fdc92008e013e916a3623e9cda 100644 (file)
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -50,6 +50,7 @@ object
 
   (** {2 History} *)
 
+  method activate : unit
   method advance : ?statement:string -> unit -> unit
   method retract : unit -> unit
   method goto: [`Top | `Bottom | `Cursor] -> unit -> unit
@@ -117,4 +118,5 @@ val script:
     script
 
 val current: unit -> script
+val at_page: int -> script
 val iter_scripts: (script -> unit) -> unit