]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/texTermEditor.ml
MQueryInterpreter: interface updated
[helm.git] / helm / gTopLevel / texTermEditor.ml
index 789b77d81b604f3d4639f44f5095e0562a9b231b..b8375b3eab0a9a861d8841c35a8cef17f4c714ed 100644 (file)
@@ -56,6 +56,7 @@ module Make(C:Disambiguate.Callbacks) =
    module Disambiguate' = Disambiguate.Make(C);;
 
    class term_editor_impl
+    mqi_handle
     ?packing ?width ?height
     ?isnotempty_callback ?share_id_to_uris_with () : term_editor
    =
@@ -191,7 +192,7 @@ module Make(C:Disambiguate.Callbacks) =
            ~context:name_context ~metasenv TexCicTextualLexer.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' ;