X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=f9c617385a945e8a4facc9ee39517f6816729fc6;hb=f7d04edd37b51a7daa4e372be9439163f92648b6;hp=1ad4b2cd10a79dd14348b67d157d4b4b7552beab;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 1ad4b2cd1..f9c617385 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -62,9 +62,27 @@ let near (x1, y1) (x2, y2) =
   let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
   (distance < 4.)
 
+let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
+let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
 let href_ds = Gdome.domString "href"
 let xref_ds = Gdome.domString "xref"
 
+let domImpl = Gdome.domImplementation ()
+
+  (** Gdome.element of a MathML document whose rendering should be blank. Used
+  * by cicBrowser to render "about:blank" document *)
+let empty_mathml = lazy (
+  domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
+    ~qualifiedName:(Gdome.domString "math") ~doctype:None)
+
+let empty_boxml = lazy (
+  domImpl#createDocument ~namespaceURI:(Some DomMisc.boxml_ns) 
+    ~qualifiedName:(Gdome.domString "box") ~doctype:None)
+
+  (** shown for goals closed by side effects *)
+let closed_goal_mathml = lazy (
+  domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
+
 (* ids_to_terms should not be passed here, is just for debugging *)
 let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
   let find_parent id ids =
@@ -190,11 +208,11 @@ object (self)
           (match self#get_element_at x y with
           | None -> ()
           | Some elt ->
-              let namespaceURI = DomMisc.xlink_ns in
               let localName = href_ds in
-              if elt#hasAttributeNS ~namespaceURI ~localName then
+              if elt#hasAttributeNS ~namespaceURI:xlink_ns ~localName then
                 self#invoke_href_callback
-                  (elt#getAttributeNS ~namespaceURI ~localName)#to_string
+                  (elt#getAttributeNS ~namespaceURI:xlink_ns
+                    ~localName)#to_string
                   gdk_button
               else
                 ignore (self#action_toggle elt));
@@ -231,7 +249,7 @@ object (self)
       ignore (self#coerce#misc#grab_selection Gdk.Atom.primary)
     in
     let rec aux elt =
-      if (elt#getAttributeNS ~namespaceURI:DomMisc.helm_ns
+      if (elt#getAttributeNS ~namespaceURI:helm_ns
             ~localName:xref_ds)#to_string <> ""
       then
         set_selection elt
@@ -243,7 +261,7 @@ object (self)
         with GdomeInit.DOMCastException _ -> ()
     in
     (match gdome_elt with
-    | Some elt when (elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns
+    | Some elt when (elt#getAttributeNS ~namespaceURI:xlink_ns
         ~localName:href_ds)#to_string <> "" ->
           set_selection elt
     | Some elt -> aux elt
@@ -274,14 +292,14 @@ object (self)
          (try Hashtbl.find ids_to_terms id with Not_found -> assert false)
 
   method private string_of_node node =
-    if node#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
+    if node#hasAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
     then self#string_of_id_node node
     else string_of_dom_node node
 
   method private string_of_id_node node =
     let get_id (node: Gdome.element) =
       let xref_attr =
-        node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
+        node#getAttributeNS ~namespaceURI:helm_ns ~localName:xref_ds
       in
       List.hd (HExtlib.split ~sep:' ' xref_attr#to_string)
     in
@@ -369,7 +387,7 @@ object (self)
         Hashtbl.create 1, None));
     let name = "sequent_viewer.xml" in
     MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
-    ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
+    ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
     self#load_root ~root:mathml#get_documentElement
 
   method load_object obj =
@@ -389,7 +407,7 @@ object (self)
     |  _ ->
         let name = "cic_browser.xml" in
         MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
-        ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ());
+        ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
         self#load_root ~root:mathml#get_documentElement;
         current_mathml <- Some mathml);
 end
@@ -519,7 +537,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           let markup =
             match depth, pos with
             | 0, _ -> `Current (render_switch sw)
-            | 1, pos when Stack.head_tag stack = Stack.BranchTag ->
+            | 1, pos when Stack.head_tag stack = `BranchTag ->
                 `Shift (pos, render_switch sw)
             | _ -> render_switch sw
           in
@@ -538,7 +556,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       (match goal_switch with
       | Stack.Open goal -> cicMathView#load_sequent _metasenv goal
       | Stack.Closed goal ->
-          let doc = Lazy.force MatitaMisc.closed_goal_mathml in
+          let doc = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root:doc#get_documentElement);
       (try
         cicMathView#set_selection None;
@@ -775,8 +793,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private blank () =
       self#_showMath;
-      mathView#load_root
-        (Lazy.force MatitaMisc.empty_mathml)#get_documentElement
+      mathView#load_root (Lazy.force empty_mathml)#get_documentElement
 
     method private _loadCheck term =
       failwith "not implemented _loadCheck";