X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.mli;h=be77c4435104b182f230a122ebcab5274a9d1d65;hb=41be5e85a1103a5b14495bb487995a6a88e79c48;hp=99e69f6e1cb5e7a0de251fdb419ca5c105be9a23;hpb=6187b40af194fb960d91653682a0eb2096f20f3b;p=helm.git

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 99e69f6e1..be77c4435 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -23,189 +23,24 @@
  * http://helm.cs.unibo.it/
  *)
 
-  (** exceptions whose content should be presented to the user *)
-exception Not_implemented of string
-exception Failure of string
-
-val not_implemented : string -> 'a
-val error : string -> 'a
-val warning : string -> unit
-val debug_print : string -> unit
-
-exception No_proof  (** no current proof is available *)
 exception Cancel
-exception Unbound_identifier of string
-
-  (** @param exn an exception
-  * @return a string which is meant to be a textual explaination of the
-   exception understandable by a user *)
-val explain: exn -> string
-
-val unopt_uri : 'a option -> 'a
-
-  (** {3 disambiguator callbacks} *)
-
-type choose_uris_callback =
-  selection_mode:[ `MULTIPLE | `SINGLE ] ->
-  ?title:string ->
-  ?msg:string -> ?nonvars_button:bool -> string list -> string list
-
-type choose_interp_callback = (string * string) list list -> int list
-
-  (** @raise Failure if called, use if unambiguous input is required *)
-val mono_uris_callback: choose_uris_callback
-  (** @raise Failure if called, use if unambiguous input is required *)
-val mono_interp_callback: choose_interp_callback
-
-(** {2 major matita objects} *)
-
-class type parserr =
-  object
-    method parseTactical : char Stream.t -> DisambiguateTypes.tactical
-    method parseTerm : char Stream.t -> DisambiguateTypes.term
-  end
-
-  (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
-class type console =
-  object
-    method clear : unit -> unit
-    method echo_error : string -> unit
-    method echo_message : string -> unit
-    method wrap_exn : 'a. (unit -> 'a) -> 'a option
-  end
-
-class type disambiguator =
-  object
-    method env : DisambiguateTypes.environment
-    method setEnv : DisambiguateTypes.environment -> unit
-
-    method chooseUris: choose_uris_callback
-    method setChooseUris: choose_uris_callback -> unit
-
-    method chooseInterp: choose_interp_callback
-    method setChooseInterp: choose_interp_callback -> unit
-
-    method parserr: parserr
-
-      (* TODO Zack: as long as matita doesn't support MDI inteface,
-      * disambiguateTerm will return a single term *)
-      (** @param env disambiguation environment. If this parameter is given the
-      * disambiguator act statelessly, that is internal disambiguation status
-      * want be changed but only returned. If this parameter is not given the
-      * internal one will be used and updated with the disambiguation status
-      * resulting from the disambiguation *)
-    method disambiguateTerm :
-      ?context:Cic.context ->
-      ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-      char Stream.t ->
-      DisambiguateTypes.environment * Cic.metasenv * Cic.term *
-      CicUniv.universe_graph
-
-      (** @param env @see disambiguateTerm above *)
-    method disambiguateTermAst :
-      ?context:Cic.context ->
-      ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-      DisambiguateTypes.term ->
-      DisambiguateTypes.environment * Cic.metasenv * Cic.term *
-      CicUniv.universe_graph
-
-      (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All
-      * AST should be closed hence no context param is permitted on this method
-      *)
-    method disambiguateTermAsts :
-      ?metasenv:Cic.metasenv ->
-      ?env:DisambiguateTypes.environment ->
-      DisambiguateTypes.term list ->
-      DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
-      CicUniv.universe_graph
-  end
 
-class type proof =
-  object
-    inherit [unit] StatefulProofEngine.status
-
-    (** return a pair of "xml" (as defined in Xml module) representing the *
-     * current proof type and body, respectively *)
-    method toXml : Xml.token Stream.t * Xml.token Stream.t
-
-    method toString : string
-  end
-
-class type currentProof =
-  object
-    method onGoing: unit -> bool  (** true if a proof is on going *)
-    method proof: proof           (** @raise Failure "No current proof" *)
-    method start: proof -> unit   (** starts a new proof *)
-    method abort: unit -> unit    (** abort the on going proof *)
-    method quit: unit -> unit     (** quit matita *)
-  end
-
-  (** first component represents success: true = success, false = failure
-  * second component represents console action: true = hide, false = keep *)
-type command_outcome = bool * bool
-
-  (** interpreter for toplevel phrases given via console *)
-class type interpreter =
-  object
-    method reset: unit  (** return the interpreter to the initial state *)
-
-      (** parse a single phrase contained in the input string. Additional
-      * garbage at the end of the phrase is ignored
-      * @return true if no exception has been raised by the evaluation, false
-      * otherwise
-      *)
-    method evalPhrase: string -> command_outcome
-
-      (** as evalPhrase above, but parses a character stream. Only characters
-      * composing next phrases are consumed *)
-(*     method evalStream: char Stream.t -> command_outcome *)
+type abouts = [ `Blank | `Current_proof | `Us ]
 
-      (** as above, evaluating a command/tactics AST *)
-    method evalAst: DisambiguateTypes.tactical -> command_outcome
+type mathViewer_entry =
+  [ `About of abouts
+  | `Check of string
+  | `Cic of Cic.term * Cic.metasenv
+  | `Dir of string
+  | `Uri of UriManager.uri
+  | `Whelp of string * UriManager.uri list ]
 
-      (** offset from the starting of the last string parser by evalPhrase where
-      * parsing stop.
-      * @raise Failure when no offset has been recorded *)
-    method endOffset: int
-
-  end
-
-(** {2 MathML widgets} *)
-
-type term_source =
-  [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
-  | `String of string
-  ]
+val string_of_entry : mathViewer_entry -> string
+val entry_of_string : string -> mathViewer_entry
 
 class type mathViewer =
   object
-    method checkTerm: term_source -> unit
-  end
-
-class type cicBrowser =
-  object
-    method loadUri: string -> unit
-    method loadTerm: term_source -> unit
+    method show_entry : ?reuse:bool -> mathViewer_entry -> unit
+    method show_uri_list :
+      ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
   end
-
-type mml_of_cic_sequent =
-  Cic.metasenv ->
-  Cic.conjecture ->
-  Gdome.document *
-  ((Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.id option) Hashtbl.t *
-   (string, Cic.hypothesis) Hashtbl.t)
-
-type mml_of_cic_object =
-  explode_all:bool ->
-  UriManager.uri ->
-  Cic.annobj ->
-  (string, string) Hashtbl.t ->
-  (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
-
-(** {2 shorthands} *)
-
-type namer = ProofEngineTypes.mk_fresh_name_type
-