First committed version that (may) use the MathML editor to enter formulas.

[helm.git] / helm / gTopLevel / disambiguate.mli

diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli
index 2a03f58d997d22812192ce44ba30059a460295a0..40ad3ec2e97a02d184230568d7fcaa14d4778d3f 100644 (file)
--- a/helm/gTopLevel/disambiguate.mli
+++ b/helm/gTopLevel/disambiguate.mli
@@ -38,6 +38,12 @@
 
 module type Callbacks =
   sig
+    (* The following two functions are used to save/restore the metasenv *)
+    (* before/after the parsing.                                         *)
+    (*CSC: This should be made functional sooner or later! *)
+    val get_metasenv : unit -> Cic.metasenv
+    val set_metasenv : Cic.metasenv -> unit
+
     val output_html : string -> unit
     val interactive_user_uri_choice :
       selection_mode:[`SINGLE | `EXTENDED] ->
@@ -50,7 +56,8 @@ module type Callbacks =
   end
 
 type domain_and_interpretation =
- string list * (string -> CicTextualParser0.uri option)
+ CicTextualParser0.interpretation_domain_item list *
+  CicTextualParser0.interpretation
 
 module Make (C : Callbacks) :
     sig
@@ -58,9 +65,8 @@ module Make (C : Callbacks) :
       val disambiguate_input :
         Cic.context ->
         Cic.metasenv ->
-        string list ->
-        ((string -> CicTextualParser0.interp_codomain option) ->
-         Cic.metasenv * Cic.term) ->
+        CicTextualParser0.interpretation_domain_item list ->
+        (CicTextualParser0.interpretation -> Cic.metasenv * Cic.term) ->
         id_to_uris:domain_and_interpretation ->
         domain_and_interpretation * Cic.metasenv * Cic.term
     end