]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/texTermEditor.ml
Eureka!
[helm.git] / helm / gTopLevel / texTermEditor.ml
index c89fe04b2da80a94b53d0d38f4b425b1e040b354..b89974d7152ff94b2a8e7f8a0e4c32d43bfced7e 100644 (file)
@@ -46,21 +46,19 @@ class type term_editor =
    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
     ?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
@@ -131,10 +129,13 @@ module Make(C:Disambiguate.Callbacks) =
           mmlwidget#thaw ;
           adj#set_value adj#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
@@ -206,18 +207,14 @@ module Make(C:Disambiguate.Callbacks) =
          ) 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
+        let environment',metasenv,expr =
+         Disambiguate'.disambiguate_term mqi_handle 
+          context metasenv (Mathml_editor.get_tex tex_editor) !environment
+        in
+         environment := environment' ;
+         metasenv,expr
+
+      method environment = environment
    end
 
    let term_editor = new term_editor_impl