snapshot, notably:

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index b165740aade4081290fd3851568998eee98dd49b..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
@@ -188,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
-