snapshot, notably:

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 5d6b8e99d1c83a7e2d8a2ec45448f82a1ef74af4..8f59d3fc95276e75ba617364fdd828fa770218f7 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -77,14 +77,26 @@ class type console =
     method wrap_exn       : 'a. (unit -> 'a) -> 'a option
   end
 
+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
+
 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
+
     method disambiguateTerm:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
@@ -165,13 +177,6 @@ type mml_of_cic_object =
 
 type namer = ProofEngineTypes.mk_fresh_name_type
 
-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
-
 let mono_uris_callback ~selection_mode ?title ?msg ?nonvars_button _ =
   raise (Failure "ambiguous input")
 let mono_interp_callback _ = raise (Failure "ambiguous input")