let username = Helm_registry.get "user.name" in
let tmp_db_name =
if HExtlib.is_dir "/dev/shm/" && HExtlib.writable_dir "/dev/shm/" then
- (HLog.debug "using /dev/shm to store the working copy of the db";
+ ((*HLog.debug "using /dev/shm to store the working copy of the db";*)
"/dev/shm/matita.db." ^ username ^ "." ^ string_of_int (Unix.getpid ()))
else
- (HLog.debug "/dev/shm not available";
+ ((*HLog.debug "/dev/shm not available";*)
Helm_registry.get "matita.basedir" ^ "/matita.db." ^ username ^ "." ^
string_of_int (Unix.getpid ()))
in
let db_name = Helm_registry.get "matita.basedir" ^ "/" ^ database ^ ".db" in
- (* XXX big hack XXX *)
- let standard_db_name = "/usr/share/matita/metadata.db" in
+ let standard_db_name =
+ Helm_registry.get "matita.rt_base_dir" ^ "/metadata.db"
+ in
let cp_to_ram_cmd =
if HExtlib.is_regular db_name then
"cp " ^ db_name ^ " " ^ tmp_db_name
ignore (Sys.command ("mv " ^ tmp_db_name ^ " " ^ db_name))
in
at_exit mv_to_disk_cmd;
- Some (Sqlite3.db_open tmp_db_name)
+ let db = Sqlite3.db_open tmp_db_name in
+ (* attach the REGEX function *)
+ Sqlite3.create_fun_2 db "REGEXP"
+ (fun s rex ->
+ match rex, s with
+ | Sqlite3.Data.TEXT rex, Sqlite3.Data.BLOB s
+ | Sqlite3.Data.TEXT rex, Sqlite3.Data.TEXT s ->
+ let r = Str.regexp rex in
+ if Str.string_match r s 0 then
+ Sqlite3.Data.INT 1L
+ else
+ Sqlite3.Data.INT 0L
+ | _ -> raise (Error "wrong types to 'REGEXP'"));
+ Some db
;;
let disconnect db =