X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;h=5ea965f2fd76c01ffd0c3e23f3210afe8aa38acb;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1ea429926519bd688c3126e6374075efaf7c75ed;hpb=f36273550bc0538ea194cf0dee32ec608a6790f7;p=helm.git

diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml
index 1ea429926..5ea965f2f 100644
--- a/helm/gTopLevel/texTermEditor.ml
+++ b/helm/gTopLevel/texTermEditor.ml
@@ -45,7 +45,8 @@ class type term_editor =
    method get_as_string : string
    method get_metasenv_and_term :
      context:Cic.context ->
-     metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+     metasenv:Cic.metasenv -> 
+     Cic.metasenv * Cic.term * CicUniv.universe_graph
    method reset : unit
    (* The input of set_term is unquoted *)
    method set_term : string -> unit
@@ -59,7 +60,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
    module Disambiguate' = DisambiguatingParser.Make(C);;
 
    class term_editor_impl
-    mqi_handle
+    ~dbd
     ?packing ?width ?height
     ?isnotempty_callback ?share_environment_with () : term_editor
    =
@@ -217,16 +218,17 @@ module Make(C:DisambiguateTypes.Callbacks) =
          ) context
        in
         debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
-        let environment',metasenv,expr =
+        let environment',metasenv,expr,ugraph =
          match
-          Disambiguate'.disambiguate_term mqi_handle 
-           context metasenv (Mathml_editor.get_tex tex_editor) !environment
+          Disambiguate'.disambiguate_term ~dbd
+           ~context ~metasenv (Mathml_editor.get_tex tex_editor) 
+	    ~initial_ugraph:CicUniv.empty_ugraph ~aliases:!environment
          with
-            [environment',metasenv,expr] -> environment',metasenv,expr
+            [environment',metasenv,expr,u] -> environment',metasenv,expr,u
           | _ -> assert false
         in
          environment := environment' ;
-         metasenv,expr
+         metasenv,expr,ugraph
 
       method environment = environment
    end