X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.mli;h=be77c4435104b182f230a122ebcab5274a9d1d65;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=321e26b99e9efcfdecae62346feb7fd3b3b1ad05;hpb=0ac236dda6f80f6dc86a7f12d8c88b25e64e3251;p=helm.git

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 321e26b99..be77c4435 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -24,65 +24,6 @@
  *)
 
 exception Cancel
-exception Statement_error of string
-val statement_error : string -> 'a
-
-exception Command_error of string
-val command_error : string -> 'a
-
-exception Option_error of string * string
-exception Unbound_identifier of string
-
-type incomplete_proof = {
-  proof: ProofEngineTypes.proof;
-  stack: Continuationals.Stack.t;
-}
-
-type proof_status =
-    No_proof
-  | Incomplete_proof of incomplete_proof
-  | Proof of ProofEngineTypes.proof
-  | Intermediate of Cic.metasenv
-
-module StringMap : Map.S with type key = String.t
-
-type option_value =
-  | String of string
-  | Int of int
-type options = option_value StringMap.t
-val no_options : 'a StringMap.t
-
-type status = {
-  aliases: DisambiguateTypes.environment;         (** disambiguation aliases *)
-  multi_aliases: DisambiguateTypes.multiple_environment;
-  moo_content_rev: GrafiteMarshal.moo;
-  proof_status: proof_status;                             (** logical status *)
-  options: options;
-  objects: (UriManager.uri * string) list;  (** in-scope objects, with paths *)
-  coercions: UriManager.uri list;                      (** defined coercions *)
-  notation_ids: CicNotation.notation_id list;      (** in-scope notation ids *)
-}
-
-val set_metasenv: Cic.metasenv -> status -> status
-
-  (** list is not reversed, head command will be the first emitted *)
-val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
-val add_moo_metadata: GrafiteAst.metadata list -> status -> status
-
-val dump_status : status -> unit
-val get_option : status -> StringMap.key -> option_value
-val get_string_option : status -> StringMap.key -> string
-val set_option : status -> StringMap.key -> string -> status
-
-class type console =
-  object
-    method choose_uri : string list -> string
-    method clear : unit -> unit
-    method echo_error : string -> unit
-    method echo_message : string -> unit
-    method show : ?msg:string -> unit -> unit
-    method wrap_exn : (unit -> 'a) -> 'a option
-  end
 
 type abouts = [ `Blank | `Current_proof | `Us ]
 
@@ -94,17 +35,8 @@ type mathViewer_entry =
   | `Uri of UriManager.uri
   | `Whelp of string * UriManager.uri list ]
 
-val string_of_entry :
-  [< `About of [< `Blank | `Current_proof | `Us ]
-   | `Check of 'a
-   | `Cic of 'b * 'c
-   | `Dir of string
-   | `Uri of UriManager.uri
-   | `Whelp of string * 'd ] ->
-  string
-
-val entry_of_string :
-  string -> [> `About of [> `Blank | `Current_proof | `Us ] ]
+val string_of_entry : mathViewer_entry -> string
+val entry_of_string : string -> mathViewer_entry
 
 class type mathViewer =
   object
@@ -112,14 +44,3 @@ class type mathViewer =
     method show_uri_list :
       ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
   end
-
-val qualify: status -> string -> string
-
-val get_current_proof: status -> ProofEngineTypes.proof
-val get_proof_metasenv: status ->  Cic.metasenv
-val get_proof_context: status -> ProofEngineTypes.goal -> Cic.context 
-val get_proof_conclusion: status -> ProofEngineTypes.goal -> Cic.term
-val get_stack: status -> Continuationals.Stack.t
-
-val set_stack: Continuationals.Stack.t -> status -> status
-