ported to Dbi-disambiguation

diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
index 3a74ef05111ce88f2948052896e5ce47a9fc598e..e7b50c2662efadad81dcfb91615bc6cb505d200b 100644 (file)
--- a/helm/gTopLevel/termEditor.ml
+++ b/helm/gTopLevel/termEditor.ml
@@ -56,7 +56,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
 
    module Disambiguate' = DisambiguatingParser.Make(C);;
 
-   class term_editor_impl mqi_handle ?packing ?width ?height
+   class term_editor_impl ~(dbh:Dbi.connection) ?packing ?width ?height
     ?isnotempty_callback ?share_environment_with () : term_editor
    =
     let environment =
@@ -100,7 +100,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
        in
         let environment',metasenv,expr =
          match
-          Disambiguate'.disambiguate_term mqi_handle context metasenv
+          Disambiguate'.disambiguate_term ~dbh context metasenv
            (input#buffer#get_text ()) !environment
          with
             [environment',metasenv,expr] -> environment',metasenv,expr

diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli
index b3fb949378f504bb9b060d1c88cf60d23bdfc812..ecb40decdb207d2bad00fbb155f8b3b03bca6dce 100644 (file)
--- a/helm/gTopLevel/termEditor.mli
+++ b/helm/gTopLevel/termEditor.mli
@@ -39,7 +39,7 @@ class type term_editor =
 module Make (C : DisambiguateTypes.Callbacks) :
    sig
     val term_editor :
-     MQIConn.handle ->
+     dbh:Dbi.connection ->
      ?packing:(GObj.widget -> unit) ->
      ?width:int ->
      ?height:int ->

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

diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli
index 8b040c9838a33a60c8fdb3d8fd1aae1a0cc0dafd..c7709b5326c3ff5714606ed465bcfe3f782f7ef6 100644 (file)
--- a/helm/gTopLevel/texTermEditor.mli
+++ b/helm/gTopLevel/texTermEditor.mli
@@ -40,7 +40,7 @@ class type term_editor =
 module Make (C : DisambiguateTypes.Callbacks) :
    sig
     val term_editor :
-     MQIConn.handle ->
+     dbh:Dbi.connection ->
      ?packing:(GObj.widget -> unit) ->
      ?width:int ->
      ?height:int ->