helmns -> helm_ns

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e06c02297454c3e532fe877c083d9301cb6afccd..5eba45750b08a52d8119055c1650007fd411e4b8 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -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)