ported to Dbi-disambiguation

[helm.git] / helm / gTopLevel / texTermEditor.ml

diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml
index 1ea429926519bd688c3126e6374075efaf7c75ed..825b79e122671a3ed7fcbc1e224f0ff82f8e9ce6 100644 (file)
--- a/helm/gTopLevel/texTermEditor.ml
+++ b/helm/gTopLevel/texTermEditor.ml
@@ -59,7 +59,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
    module Disambiguate' = DisambiguatingParser.Make(C);;
 
    class term_editor_impl
-    mqi_handle
+    ~dbh
     ?packing ?width ?height
     ?isnotempty_callback ?share_environment_with () : term_editor
    =
@@ -219,7 +219,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
         debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
         let environment',metasenv,expr =
          match
-          Disambiguate'.disambiguate_term mqi_handle 
+          Disambiguate'.disambiguate_term ~dbh 
            context metasenv (Mathml_editor.get_tex tex_editor) !environment
          with
             [environment',metasenv,expr] -> environment',metasenv,expr