Release 0.5.9.

[helm.git] / helm / software / matita / matitaInit.ml

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 70125f54c222bb5dc3c3d146a8a7cc8aecfee294..2f9ba6a47ed92237d5d13f222b86652e915f9f6d 100644 (file)
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -98,7 +98,18 @@ let initialize_db init_status =
   if not (already_configured [ Db ] init_status) then
     begin
       if not (Helm_registry.get_bool "matita.system") then
-        MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+       ((* SQL does not allow dots in table names. Let's replace them
+           with underscore and let's quote underscores by doubling them *)
+        let owner = Helm_registry.get "matita.owner" in
+        let owner = Str.global_replace (Str.regexp "_") "__" owner in
+        let owner = Str.global_replace (Str.regexp "\\.") "_" owner in
+        if Str.string_match (Str.regexp "^[a-zA-Z][a-zA-Z0-9_]*$") owner 0 then
+         MetadataTypes.ownerize_tables owner
+        else (
+         prerr_endline ("Error: the matita.owner configuration variable must contain only latin characters, digits and underscores. If the default configuration is used, the variable is set to the USER environment variable and can be changed prepending the USER=any_valid_name to the matita command.");
+         exit (-1)
+        )
+       );
       LibraryDb.create_owner_environment ();
       Db::init_status
     end