snapshot, notably:

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index b0830c70928b09f4b1beea6b28d6287ea3bb8b3d..99e69f6e1cb5e7a0de251fdb419ca5c105be9a23 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
@@ -60,12 +76,17 @@ class type console =
 
 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
@@ -153,11 +174,21 @@ class type interpreter =
 
 (** {2 MathML widgets} *)
 
+type term_source =
+  [ `Ast of DisambiguateTypes.term
+  | `Cic of Cic.term
+  | `String of string
+  ]
+
 class type mathViewer =
   object
-    method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
-    method unload: unit -> unit
-    method set_href_callback: (UriManager.uri -> unit) option -> 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 =
@@ -178,17 +209,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
-