From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 17 Feb 2004 17:20:57 +0000 (+0000)
Subject: mathql_db_map.txt is now retrieved by Helm_registry.
X-Git-Tag: v0_0_4~171
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d9b746b8c3a6f62d874329c425ea444969af5576;p=helm.git

mathql_db_map.txt is now retrieved by Helm_registry.
---

diff --git a/helm/gTopLevel/gTopLevel.conf.xml.sample b/helm/gTopLevel/gTopLevel.conf.xml.sample
index 9bc696dc5..b3bebb774 100644
--- a/helm/gTopLevel/gTopLevel.conf.xml.sample
+++ b/helm/gTopLevel/gTopLevel.conf.xml.sample
@@ -11,6 +11,9 @@
   </section>
 
   <!-- From now on it is unlikely that something needs to be changed -->
+  <section name="mathql_interpreter">
+   <key name="db_map">mathql_db_map.txt</key>
+  </section>
   <section name="local_library">
     <key name="dir">file://$(users_settings.per_user_work_directory)/objects</key>
     <key name="url">$(local_library.dir)</key>
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e14c9955b..8643ec313 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -48,9 +48,18 @@ module MQGT = MQGTypes
 module MQGU = MQGUtil
 module MQG  = MQueryGenerator
 
-(* GLOBAL CONSTANTS *)
 
-let configuration_file = "gTopLevel.conf.xml"
+(* first of all let's initialize the Helm_registry *)
+let _ =
+ let configuration_file = "gTopLevel.conf.xml" in
+  if not (Sys.file_exists configuration_file) then begin
+    eprintf "E: Can't find configuration file '%s'\n" configuration_file;
+    exit 2
+  end;
+ Helm_registry.load_from configuration_file
+;;
+
+(* GLOBAL CONSTANTS *)
 
 let mqi_debug_fun s = debug_print ~level:2 s
 let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
@@ -2835,11 +2844,6 @@ end
 (* MAIN *)
 
 let initialize_everything () =
-  if not (Sys.file_exists configuration_file) then begin
-    eprintf "E: Can't find configuration file '%s'\n" configuration_file;
-    exit 2
-  end;
-  Helm_registry.load_from configuration_file;
   let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
   let notebook = new notebook in
   let rendering_window' = new rendering_window output notebook in
diff --git a/helm/ocaml/mathql_interpreter/mQIMap.ml b/helm/ocaml/mathql_interpreter/mQIMap.ml
index 341ebd310..ed02524cc 100644
--- a/helm/ocaml/mathql_interpreter/mQIMap.ml
+++ b/helm/ocaml/mathql_interpreter/mQIMap.ml
@@ -37,11 +37,7 @@ type pg_alias = (string * string) list
 let empty_map () = "", [], []
 
 let read_map () =
-   let default_map = "mathql_db_map.txt" in
-   let map = 
-      try Sys.getenv "MATHQL_DB_MAP"
-      with Not_found -> default_map 
-   in
+   let map = Helm_registry.get "mathql_interpreter.db_map" in
    let ich = open_in map in 
    let pgs = input_line ich in
    let rec aux r s =