removed debug saving of "foo.conf.xml"

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 28bd1caaa7f35ae3244c3fc19ce93d120fddc656..7d2a47a943af0aeb8d5066c2c115e65171c52206 100644 (file)
--- 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,16 +272,16 @@ 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) =
       let xref_attr =
         node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
       in
-      xref_attr#to_string
+      List.hd (HExtlib.split ~sep:' ' xref_attr#to_string)
     in
     let id = get_id node in
     let script = MatitaScript.instance () in
@@ -591,7 +591,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     try
       f ()
     with exn ->
-      if Helm_registry.get_bool "matita.catch_top_level_exn" then
+      if not (Helm_registry.get_bool "matita.debug") then
         fail (MatitaExcPp.to_string exn)
       else raise exn
   in
@@ -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))