X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibraryDb.ml;h=e6af1eb814bf198e3f3d714eca0556450fbfdc63;hb=82d0bc4291648c88e9f248fc5a67518e938eacdf;hp=78cff79482d2f261c5c46c461d65f2a0152f0a69;hpb=ac741958783108ff31552e533c853e85c2ebb1c5;p=helm.git

diff --git a/helm/software/components/library/libraryDb.ml b/helm/software/components/library/libraryDb.ml
index 78cff7948..e6af1eb81 100644
--- a/helm/software/components/library/libraryDb.ml
+++ b/helm/software/components/library/libraryDb.ml
@@ -58,7 +58,7 @@ let clean_owner_environment () =
   let owned_uris =
     try
       MetadataDb.clean ~dbd
-    with HSql.Error as exn ->
+    with (HSql.Error _) as exn ->
       match HSql.errno dbd with 
       | HSql.No_such_table -> []
       | _ -> raise exn
@@ -77,7 +77,7 @@ let clean_owner_environment () =
   List.iter (fun statement -> 
     try
       ignore (HSql.exec dbd statement)
-    with HSql.Error as exn ->
+    with (HSql.Error _) as exn ->
       match HSql.errno dbd with 
       | HSql.No_such_table
       | HSql.Bad_table_error
@@ -116,14 +116,14 @@ let create_owner_environment () =
     try
       ignore (HSql.exec dbd statement)
     with
-      HSql.Error -> 
+      (HSql.Error _) as exc -> 
       let status = HSql.errno dbd in 
       match status with 
       | HSql.Table_exists_error -> ()
       | HSql.Dup_keyname -> ()
       | HSql.GENERIC_ERROR _ -> 
           prerr_endline statement;
-          raise HSql.Error
+          raise exc
       | _ -> ()
 
 
@@ -164,9 +164,13 @@ let remove_uri uri =
 let xpointers_of_ind uri =
   let dbd = instance () in
   let name_tbl =  MetadataTypes.name_tbl () in
+  let escape s =
+    Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+  in
   let query = sprintf 
-    "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl 
-      (HSql.escape (UriManager.string_of_uri uri))
+    ("SELECT source FROM %s WHERE source LIKE '%s#xpointer%%' "
+     ^^ HSql.escape_string_for_like)
+    name_tbl (escape (UriManager.string_of_uri uri))
   in
   let rc = HSql.exec dbd query in
   let l = ref [] in