1. matitaEngine splitted into disambiguation (now in grafite_parser) and

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index ebf208b92954aa84a4243a61d32e3c785cfe2d79..be77c4435104b182f230a122ebcab5274a9d1d65 100644 (file)
--- 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 list;  (** in-scope objects *)
-  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 -> string -> option_value
-val get_string_option : status -> string -> string
-val set_option : status -> string -> 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
-