triciclo.conf.xml ==> gTopLevel.conf.xml

diff --git a/helm/gTopLevel/gTopLevel.conf.xml.sample b/helm/gTopLevel/gTopLevel.conf.xml.sample
new file mode 100644 (file)
index 0000000..e8f1a5c
--- /dev/null
+++ b/helm/gTopLevel/gTopLevel.conf.xml.sample
@@ -0,0 +1,32 @@
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+  <!-- These are the only settings that are likely to be changed by the user -->
+  <section name="users_settings">
+   <!-- The directory where the current proof and environment are stored -->
+   <key name="per_user_work_directory">/home/sacerdot/helm/local_stuff</key>
+
+   <!-- The URL of the host of the Getter and UWOBO -->
+   <!-- <key name="daemons_host">http://mowgli.cs.unibo.it</key> -->
+   <key name="daemons_host">http://localhost</key>
+  </section>
+
+  <!-- From now on it is unlikely that something needs to be changed -->
+  <section name="local_library">
+    <key name="dir">file://$(users_settings_per_user_work_directory)/objects</key>
+    <key name="url">$(local_library.dir)</key>
+  </section>
+  <section name="getter">
+    <key name="mode">remote</key>
+    <key name="url">$(users_settings.daemons_host):58081/</key>
+  </section>
+  <section name="gtoplevel">
+    <key name="constant_type_file">$(users_settings.per_user_work_directory)/constanttype</key>
+    <key name="environment_file">$(users_settings.per_user_work_directory)/environment</key>
+    <key name="inner_types_file">$(users_settings.per_user_work_directory)/innertypes</key>
+    <key name="proof_file">$(users_settings.per_user_work_directory)/currentproof</key>
+    <key name="proof_file_type">$(users_settings.per_user_work_directory)/currentprooftype</key>
+  </section>
+  <section name="uwobo">
+    <key name="url">$(users_settings.daemons_host):58080/</key>
+  </section>
+</helm_registry>

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index ba334ac036908b166c779037acbda0be2bb443b5..e14c9955bcef09b4b4ad6076f322714374347d19 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -50,7 +50,7 @@ module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
-let configuration_file = "triciclo.conf.xml"
+let configuration_file = "gTopLevel.conf.xml"
 
 let mqi_debug_fun s = debug_print ~level:2 s
 let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
@@ -484,8 +484,8 @@ let qed () =
   (** save an unfinished proof on the filesystem *)
 let save_unfinished_proof () =
  let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
- let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
- let proof_file = Helm_registry.get "triciclo.proof_file" in
+ let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+ let proof_file = Helm_registry.get "gtoplevel.proof_file" in
  Xml.pp ~quiet:true xml (Some proof_file_type) ;
  HelmLogger.log
   (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ;
@@ -676,8 +676,8 @@ let load_unfinished_proof () =
       None -> raise NoChoice
     | Some uri0 ->
        let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
-       let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
-       let proof_file = Helm_registry.get "triciclo.proof_file" in
+       let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+       let proof_file = Helm_registry.get "gtoplevel.proof_file" in
         match CicParser.obj_of_xml proof_file_type (Some proof_file) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
@@ -2585,7 +2585,7 @@ end
 
 let dump_environment () =
   try
-    let oc = open_out (Helm_registry.get "triciclo.environment_file") in
+    let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in
     HelmLogger.log (`Msg (`T "Dumping environment ..."));
     CicEnvironment.dump_to_channel oc;
     HelmLogger.log (`Msg (`T "... done!")) ;
@@ -2597,7 +2597,7 @@ let dump_environment () =
 ;;
 let restore_environment () =
   try
-    let ic = open_in (Helm_registry.get "triciclo.environment_file") in
+    let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in
     HelmLogger.log (`Msg (`T "Restoring environment ... "));
     CicEnvironment.restore_from_channel ic;
     HelmLogger.log (`Msg (`T "... done!"));
@@ -2853,7 +2853,7 @@ let initialize_everything () =
     (Some (print_error_as_html "XSLT Debug Message: "));
   rendering_window'#show () ;
   if restore_environment_on_boot &&
-    Sys.file_exists (Helm_registry.get "triciclo.environment_file")
+    Sys.file_exists (Helm_registry.get "gtoplevel.environment_file")
   then
     restore_environment ();
   GtkThread.main ()

diff --git a/helm/gTopLevel/triciclo.conf.xml.sample b/helm/gTopLevel/triciclo.conf.xml.sample
deleted file mode 100644 (file)
index 7a2a3e3..0000000
--- a/helm/gTopLevel/triciclo.conf.xml.sample
+++ /dev/null
@@ -1,32 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>
-<helm_registry>
-  <!-- These are the only settings that are likely to be changed by the user -->
-  <section name="users_settings">
-   <!-- The directory where the current proof and environment are stored -->
-   <key name="per_user_work_directory">/home/sacerdot/helm/local_stuff</key>
-
-   <!-- The URL of the host of the Getter and UWOBO -->
-   <!-- <key name="daemons_host">http://mowgli.cs.unibo.it</key> -->
-   <key name="daemons_host">http://localhost</key>
-  </section>
-
-  <!-- From now on it is unlikely that something needs to be changed -->
-  <section name="local_library">
-    <key name="dir">file://$(users_settings_per_user_work_directory)/objects</key>
-    <key name="url">$(local_library.dir)</key>
-  </section>
-  <section name="getter">
-    <key name="mode">remote</key>
-    <key name="url">$(users_settings.daemons_host):58081</key>
-  </section>
-  <section name="triciclo">
-    <key name="constant_type_file">$(users_settings.per_user_work_directory)/constanttype</key>
-    <key name="environment_file">$(users_settings.per_user_work_directory)/environment</key>
-    <key name="inner_types_file">$(users_settings.per_user_work_directory)/innertypes</key>
-    <key name="proof_file">$(users_settings.per_user_work_directory)/currentproof</key>
-    <key name="proof_file_type">$(users_settings.per_user_work_directory)/currentprooftype</key>
-  </section>
-  <section name="uwobo">
-    <key name="url">$(users_settings.daemons_host):58080/</key>
-  </section>
-</helm_registry>