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

diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml
index 047938828..5ea965f2f 100644
--- a/helm/gTopLevel/texTermEditor.ml
+++ b/helm/gTopLevel/texTermEditor.ml
@@ -23,6 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let debug = true
+let debug_print s = if debug then prerr_endline s
+
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
@@ -42,32 +45,33 @@ 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
-   method id_to_uris : Disambiguate.domain_and_interpretation ref
+   method environment : DisambiguatingParser.EnvironmentP3.t ref
  end
 ;;
 
-let empty_id_to_uris = ([],function _ -> None);;
-
-module Make(C:Disambiguate.Callbacks) =
+module Make(C:DisambiguateTypes.Callbacks) =
   struct
 
-   module Disambiguate' = Disambiguate.Make(C);;
+   module Disambiguate' = DisambiguatingParser.Make(C);;
 
    class term_editor_impl
-    mqi_handle
+    ~dbd
     ?packing ?width ?height
-    ?isnotempty_callback ?share_id_to_uris_with () : term_editor
+    ?isnotempty_callback ?share_environment_with () : term_editor
    =
     let mmlwidget =
      GMathViewAux.single_selection_math_view
       ?packing ?width ?height () in
+(*
     let drawing_area = mmlwidget#get_drawing_area in
     let _ = drawing_area#misc#set_can_focus true in
     let _ = drawing_area#misc#grab_focus () in
+*)
     let logger =
      fun l s -> prerr_endline ("TERM_EDITOR (" ^ string_of_int l ^ "): " ^ s) in
     let tex_editor =
@@ -81,11 +85,14 @@ module Make(C:Disambiguate.Callbacks) =
       ~tml_uri:"/usr/share/editex/tml-litex.xsl"
       ~log:logger
     in
+(*
     let _ =
      (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#button_press
       ~callback:(fun _ -> drawing_area#misc#grab_focus () ; true) in
+*)
     let _ =
-     (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in
+(*      (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in *)
+     (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_in
        ~callback:
          (fun _ ->
            mmlwidget#freeze ;
@@ -93,7 +100,8 @@ module Make(C:Disambiguate.Callbacks) =
            mmlwidget#thaw ;
            true) in
     let _ =
-     (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out
+(*      (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out *)
+     (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_out
        ~callback:
          (fun _ ->
            mmlwidget#freeze ;
@@ -102,9 +110,10 @@ module Make(C:Disambiguate.Callbacks) =
            true) in
     let _ = Mathml_editor.push tex_editor '$' in
     let dom_tree = Mathml_editor.get_mml tex_editor in
-    let _ = mmlwidget#load_doc dom_tree in
+    let _ = mmlwidget#load_root dom_tree#get_documentElement in
     let _ = 
-     drawing_area#event#connect#key_press
+(*      drawing_area#event#connect#key_press *)
+     (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#key_press
       (function e ->
         let key = GdkEvent.Key.keyval e in
          mmlwidget#freeze ;
@@ -126,15 +135,18 @@ module Make(C:Disambiguate.Callbacks) =
           Mathml_editor.drop tex_editor
            (List.mem `CONTROL (GdkEvent.Key.state e))
          else if key = GdkKeysyms._v then
-           ignore (mmlwidget#misc#convert_selection "STRING" `PRIMARY);
-         let adj = mmlwidget#get_hadjustment in
+           ignore (mmlwidget#misc#convert_selection "STRING" Gdk.Atom.primary);
+         let hadj, _ = mmlwidget#get_adjustments in
           mmlwidget#thaw ;
-          adj#set_value adj#upper ;
+          hadj#set_value hadj#upper ;
           false) in
-    let id_to_uris =
-     match share_id_to_uris_with with
-        None -> ref empty_id_to_uris
-      | Some obj -> obj#id_to_uris
+    let environment =
+     match share_environment_with with
+        None ->
+         ref
+          (DisambiguatingParser.EnvironmentP3.of_string
+            DisambiguatingParser.EnvironmentP3.empty)
+      | Some obj -> obj#environment
     in
     let _ =
      match isnotempty_callback with
@@ -205,19 +217,20 @@ module Make(C:Disambiguate.Callbacks) =
            | None -> None
          ) context
        in
-prerr_endline ("###CSC: " ^ (Mathml_editor.get_tex tex_editor)) ;
-        let lexbuf = Lexing.from_string (Mathml_editor.get_tex tex_editor) in
-         let dom,mk_metasenv_and_expr =
-          TexCicTextualParserContext.main
-           ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf
-         in
-          let id_to_uris',metasenv,expr =
-           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' ;
-           metasenv,expr
-      method id_to_uris = id_to_uris
+        debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
+        let environment',metasenv,expr,ugraph =
+         match
+          Disambiguate'.disambiguate_term ~dbd
+           ~context ~metasenv (Mathml_editor.get_tex tex_editor) 
+	    ~initial_ugraph:CicUniv.empty_ugraph ~aliases:!environment
+         with
+            [environment',metasenv,expr,u] -> environment',metasenv,expr,u
+          | _ -> assert false
+        in
+         environment := environment' ;
+         metasenv,expr,ugraph
+
+      method environment = environment
    end
 
    let term_editor = new term_editor_impl