]> matita.cs.unibo.it Git - helm.git/commitdiff
helmns -> helm_ns
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 20 Jan 2005 10:32:38 +0000 (10:32 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 20 Jan 2005 10:32:38 +0000 (10:32 +0000)
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/termViewer.ml

index e06c02297454c3e532fe877c083d9301cb6afccd..5eba45750b08a52d8119055c1650007fd411e4b8 100644 (file)
@@ -67,8 +67,6 @@ let dbd =
     ~database:(Helm_registry.get "db.database")
     ()
 
-let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
-
 let restore_environment_on_boot = true ;;
 let notify_hbugs_on_goal_change = false ;;
 
@@ -887,9 +885,9 @@ let
     match n with
        None -> ()
      | Some n' ->
-        if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
+        if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then
          let uri =
-          (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
+          (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href)#to_string
          in 
           show_in_show_window_uri (UriManager.uri_of_string uri)
         else
@@ -2091,7 +2089,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
  let module G = Gdome in
   let rec aux element =
    if element#hasAttributeNS
-       ~namespaceURI:Misc.helmns
+       ~namespaceURI:Misc.helm_ns
        ~localName:(G.domString "xref")
    then
      mmlwidget#set_selection (Some element)
index 8a7bb0901d09c511edf17b34430bb3a87bab404c..97fa7536a43fb29fb0a76e9ecd93021d45d55b21 100644 (file)
@@ -86,7 +86,7 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
      (function node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
@@ -108,7 +108,7 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
      (function node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
@@ -188,7 +188,7 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
       Some node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
@@ -207,7 +207,7 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
       Some node ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
-          ~namespaceURI:Misc.helmns
+          ~namespaceURI:Misc.helm_ns
           ~localName:(Gdome.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)