X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermEditor.ml;h=1b9986caa294184335c6bb697be47b35a6e0a26a;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=db637554f249e8d4fe9bfee54ccdb516ac4b81ca;hpb=8004125685a99b6c0f2f95fd7f3fa09a4f5c9094;p=helm.git

diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
index db637554f..1b9986caa 100644
--- a/helm/gTopLevel/termEditor.ml
+++ b/helm/gTopLevel/termEditor.ml
@@ -23,15 +23,15 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 06/01/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                              PROJECT HELM                                 *)
+(*                                                                           *)
+(*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                06/01/2002                                 *)
+(*                                                                           *)
+(*                                                                           *)
+(*****************************************************************************)
 
 open Printf
 
@@ -44,7 +44,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
@@ -56,12 +57,12 @@ module Make(C:DisambiguateTypes.Callbacks) =
 
    module Disambiguate' = DisambiguatingParser.Make(C);;
 
-   class term_editor_impl mqi_handle ?packing ?width ?height
+   class term_editor_impl ~(dbd:Mysql.dbd) ?packing ?width ?height
     ?isnotempty_callback ?share_environment_with () : term_editor
    =
     let environment =
      match share_environment_with with
-        None -> ref
+        None -> ref (*DisambiguateTypes.empty_environment*)
           (DisambiguatingParser.EnvironmentP3.of_string
             DisambiguatingParser.EnvironmentP3.empty)
       | Some obj -> obj#environment
@@ -98,12 +99,18 @@ module Make(C:DisambiguateTypes.Callbacks) =
            | None -> None
          ) context
        in
-        let environment',metasenv,expr =
-          Disambiguate'.disambiguate_term mqi_handle context metasenv
-           (input#buffer#get_text ()) !environment
+        let environment',metasenv,expr,ugraph =
+         match
+          Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
+           (input#buffer#get_text ()) ~initial_ugraph:CicUniv.empty_ugraph
+	    ~aliases:!environment
+         with
+            [environment',metasenv,expr,u] -> environment',metasenv,expr,u
+          | _ -> assert false
         in
         environment := environment';
-        (metasenv, expr)
+        (metasenv, expr,ugraph) 
+	  (* TASSI: FIXME ?are we sure we have to keep this?  *)
 
       method environment = environment
    end