X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.mli;h=be77c4435104b182f230a122ebcab5274a9d1d65;hb=e52175d0188a54fee13eca3ae0a8ee12d2270bd5;hp=662dad6ab6e9cbf092453a1c1206fbea432e5f75;hpb=cb408b9ea336cd8efb990f7a1c88b566ccf0bd2e;p=helm.git

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 662dad6ab..be77c4435 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -24,51 +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 status = {
-  aliases : DisambiguateTypes.environment;
-  moo_content_rev : string list;
-  proof_status : proof_status;
-  options : options;
-  objects : (UriManager.uri * string) list;
-}
-
-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 ]
 
@@ -80,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