Class mathViewer got rid of. The circular dependency between

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

diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli
index e1369617dc91823f70f4646d9856c11335917ce2..de95aac52ce9618500c05f5ed030aa5292a01843 100644 (file)
--- a/matita/matita/matitaScript.mli
+++ b/matita/matita/matitaScript.mli
@@ -63,12 +63,6 @@ object
 
   (** {2 Current proof} (if any) *)
 
-  (** @return true if there is an ongoing proof, false otherise *)
-  method onGoingProof: unit -> bool
-
-  method proofMetasenv: Cic.metasenv          (** @raise Statement_error *)
-  method proofContext: Cic.context            (** @raise Statement_error *)
-  method proofConclusion: Cic.term            (** @raise Statement_error *)
   method stack: Continuationals.Stack.t       (** @raise Statement_error *)
 
   method setGoal: int option -> unit
@@ -91,8 +85,7 @@ end
    * "*") on the side of a script name *)
 val script: 
   source_view:GSourceView2.source_view -> 
-  mathviewer: MatitaTypes.mathViewer-> 
-  urichooser: (UriManager.uri list -> UriManager.uri list) -> 
+  urichooser: (NReference.reference list -> NReference.reference list) -> 
   ask_confirmation: 
     (title:string -> message:string -> [`YES | `NO | `CANCEL]) -> 
   set_star: (bool -> unit) ->