]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/termEditor.ml
ported to Dbi-disambiguation
[helm.git] / helm / gTopLevel / termEditor.ml
index 3a74ef05111ce88f2948052896e5ce47a9fc598e..e7b50c2662efadad81dcfb91615bc6cb505d200b 100644 (file)
@@ -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