From 9f62475df3ed7aa7545321d53843cf80281645d7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Jan 2005 10:32:38 +0000 Subject: [PATCH] helmns -> helm_ns --- helm/gTopLevel/gTopLevel.ml | 8 +++----- helm/gTopLevel/termViewer.ml | 8 ++++---- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index e06c02297..5eba45750 100644 --- 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) diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index 8a7bb0901..97fa7536a 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -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!!!" *) -- 2.39.2