debian version 0.0.5-6

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index cc91486d672650793d0eae22e20be2b7e4fb5994..26299967224cb6b4f850da5a53935360691296e9 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -43,6 +43,22 @@ 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
@@ -56,16 +72,23 @@ class type console =
     method echo_error : string -> unit
     method echo_message : string -> unit
     method wrap_exn : 'a. (unit -> 'a) -> 'a option
+    method choose_uri : string list -> string
+    method show : ?msg:string -> unit -> unit
   end
 
 class type disambiguator =
   object
-    method parserr : parserr
-    method setParserr : parserr -> unit
-
     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
@@ -125,11 +148,18 @@ class type currentProof =
   * second component represents console action: true = hide, false = keep *)
 type command_outcome = bool * bool
 
+  (** schematic representation of items scripts are made of *)
+type script_item =
+  [ `Tactic                       (** action on proof status *)
+  | `Theorem                      (** start of proof, to be proved *)
+  | `Qed of UriManager.uri        (** end of proof, successfull *)
+  | `Def of UriManager.uri        (** constant with body *)
+  | `Inductive of UriManager.uri  (** inductive definition *)
+  ]
+
   (** 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
@@ -144,19 +174,43 @@ class type interpreter =
       (** as above, evaluating a command/tactics AST *)
     method evalAst: DisambiguateTypes.tactical -> command_outcome
 
+    (** {3 callbacks} *)
+
+    method setEvalAstCallback: (DisambiguateTypes.tactical -> unit) -> unit
+
+    (** {3 stateful methods}
+     * bookkeeping of last interpreted phrase *)
+
       (** 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
 
+      (** last item parsed *)
+    method lastItem: script_item option
+
+      (** change internal interpreter state *)
+    method setState: [`Proof | `Command] -> unit
+
   end
 
 (** {2 MathML widgets} *)
 
+type term_source =
+  [ `Ast of DisambiguateTypes.term
+  | `Cic of Cic.term * Cic.metasenv
+  | `String of string
+  ]
+
 class type mathViewer =
   object
-    method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
-    method unload: unit -> unit
+    method checkTerm: term_source -> unit
+  end
+
+class type cicBrowser =
+  object
+    method loadUri: string -> unit
+    method loadTerm: term_source -> unit
   end
 
 type mml_of_cic_sequent =
@@ -177,17 +231,3 @@ type mml_of_cic_object =
 
 type namer = ProofEngineTypes.mk_fresh_name_type
 
-  (** {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
-