]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/termEditor.ml
MQueryInterpreter: interface updated
[helm.git] / helm / gTopLevel / termEditor.ml
index 90ce49ae4489ca892f835ee9b123a2c243666065..48f5adb63648b2ff04e92ddfee490fe45bb75f06 100644 (file)
@@ -55,7 +55,7 @@ module Make(C:Disambiguate.Callbacks) =
 
    module Disambiguate' = Disambiguate.Make(C);;
 
-   class term_editor_impl ?packing ?width ?height ?isnotempty_callback
+   class term_editor_impl mqi_handle ?packing ?width ?height ?isnotempty_callback
     ?share_id_to_uris_with () : term_editor
    =
     let id_to_uris =
@@ -96,7 +96,7 @@ module Make(C:Disambiguate.Callbacks) =
            ~context:name_context ~metasenv CicTextualLexer.token lexbuf
          in
           let id_to_uris',metasenv,expr =
-           Disambiguate'.disambiguate_input
+           Disambiguate'.disambiguate_input mqi_handle
             context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris
           in
            id_to_uris := id_to_uris' ;