X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=4297634c809e423c8856efb4c24d7ff7384973ad;hb=3147daf418c31528a67462c77b4cb3fd6431289c;hp=28bd1caaa7f35ae3244c3fc19ce93d120fddc656;hpb=29a5b18f3da1a3ed648f23709384b7789cb099bf;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 28bd1caaa..4297634c8 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -206,7 +206,7 @@ object (self) match href_callback with | None -> () | Some f -> - (match MatitaMisc.split href_value with + (match HExtlib.split href_value with | [ uri ] -> f uri | uris -> let menu = GMenu.menu () in @@ -272,9 +272,9 @@ 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.xlink_ns ~localName:href_ds - then string_of_dom_node node - else self#string_of_id_node node + if node#hasAttributeNS ~namespaceURI:DomMisc.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) = @@ -738,11 +738,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; match self#script#status.proof_status with | Proof (uri, metasenv, bo, ty) -> - let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj | Incomplete_proof ((uri, metasenv, bo, ty), _) -> - let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj | _ -> self#blank () @@ -798,7 +798,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** this is what the browser does when you enter a string an hit enter *) method loadInput txt = - let txt = MatitaMisc.trim_blanks txt in + let txt = HExtlib.trim_blanks txt in let fix_uri txt = UriManager.string_of_uri (UriManager.strip_xpointer (UriManager.uri_of_string txt))