]> matita.cs.unibo.it Git - helm.git/commitdiff
mathql_db_map.txt is now retrieved by Helm_registry.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 17 Feb 2004 17:20:57 +0000 (17:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 17 Feb 2004 17:20:57 +0000 (17:20 +0000)
helm/gTopLevel/gTopLevel.conf.xml.sample
helm/gTopLevel/gTopLevel.ml
helm/ocaml/mathql_interpreter/mQIMap.ml

index 9bc696dc56471d9e354952dea27f36008314f0c5..b3bebb774a233cf19fe5985e518d7a4ef6f485ed 100644 (file)
@@ -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>
index e14c9955bcef09b4b4ad6076f322714374347d19..8643ec313ed053896d57eebe739c09836f29731f 100644 (file)
@@ -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
index 341ebd310490802e786991c7082d2d1b48207aca..ed02524cce9ee56994d7351ddc3f389e01343dc7 100644 (file)
@@ -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 =