- Added DisambiguatingParser (that abstracts both the parser and the

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

diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli
new file mode 100644 (file)
index 0000000..962aa05
--- /dev/null
+++ b/helm/gTopLevel/chosenTermEditor.mli
@@ -0,0 +1,23 @@
+class type term_editor =
+  object
+    method coerce : GObj.widget
+    method get_as_string : string
+    method get_metasenv_and_term :
+      context:Cic.context ->
+      metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+    method environment : DisambiguatingParser.Environment.t ref
+    method reset : unit
+    method set_term : string -> unit
+  end
+
+module Make :
+  functor (C : Disambiguate_types.Callbacks) ->
+    sig
+      val term_editor :
+        MQIConn.handle ->
+        ?packing:(GObj.widget -> unit) ->
+        ?width:int ->
+        ?height:int ->
+        ?isnotempty_callback:(bool -> unit) ->
+        ?share_environment_with:term_editor -> unit -> term_editor
+    end