removed no longer used METAs

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index c0946c89f8a0c8990d073ff489a3afa8b1be7c32..be77c4435104b182f230a122ebcab5274a9d1d65 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -24,59 +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 proof_status =
-    No_proof
-  | Incomplete_proof of ProofEngineTypes.status
-  | 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 ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
-
-type status = {
-  aliases: DisambiguateTypes.environment;   (** disambiguation aliases *)
-  moo_content_rev: ast_command list;
-  proof_status: proof_status;
-  options: options;
-  objects: (UriManager.uri * string) list;  (** in-scope objects, with paths *)
-  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: ast_command 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 ]
 
@@ -88,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