From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sat, 13 Sep 2003 23:59:22 +0000 (+0000)
Subject: - added support for dumping environment to file on exit (disabled by default)
X-Git-Tag: V_0_4_3_4~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=05fb48fba4c9a1189bfba8eaa4fbb429f9e20b6c

- added support for dumping environment to file on exit (disabled by default)
- added environment restore on boot
---

diff --git a/helm/hbugs/tutors/hbugs_tutors_common.ml b/helm/hbugs/tutors/hbugs_tutors_common.ml
index ca3de9fed..8ffd4b704 100644
--- a/helm/hbugs/tutors/hbugs_tutors_common.ml
+++ b/helm/hbugs/tutors/hbugs_tutors_common.ml
@@ -30,6 +30,7 @@ open Hbugs_types;;
 open Printf;;
 
 let broker_url = "localhost:49081/act";;
+let dump_environment_on_exit = false;;
 
 let init_tutor = Hbugs_id_generator.new_tutor_id;;
 
@@ -138,6 +139,7 @@ module type HbugsTutorDescription =
     val hint: hint
     val hint_type: hint_type
     val description: string
+    val environment_file: string
   end
 
 module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
@@ -224,13 +226,34 @@ module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
             (Exception ("parse_error", reason)))
           outchan
 
+    let restore_environment () =
+      let ic = open_in Dsc.environment_file in
+      prerr_endline "Restoring environment ...";
+      CicEnvironment.restore_from_channel
+        ~callback:(fun uri -> prerr_endline uri) ic;
+      prerr_endline "... done!";
+      close_in ic
+
+    let dump_environment () =
+      let oc = open_out Dsc.environment_file in
+      prerr_endline "Dumping environment ...";
+      CicEnvironment.dump_to_channel
+        ~callback:(fun uri -> prerr_endline uri) oc;
+      prerr_endline "... done!";
+      close_out oc
+
     let main () =
       try
         Sys.catch_break true;
-        at_exit (fun () -> unregister_from_broker my_own_id);
+        at_exit (fun () ->
+          if dump_environment_on_exit then
+            dump_environment ();
+          unregister_from_broker my_own_id);
         broker_id :=
           Some (register_to_broker
             my_own_id my_own_url Dsc.hint_type Dsc.description);
+        if Sys.file_exists Dsc.environment_file then
+          restore_environment ();
         Http_daemon.start'
           ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
       with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
diff --git a/helm/hbugs/tutors/hbugs_tutors_common.mli b/helm/hbugs/tutors/hbugs_tutors_common.mli
index 927e31b4f..43cd99cce 100644
--- a/helm/hbugs/tutors/hbugs_tutors_common.mli
+++ b/helm/hbugs/tutors/hbugs_tutors_common.mli
@@ -53,6 +53,7 @@ module type HbugsTutorDescription =
     val hint: hint
     val hint_type: hint_type
     val description: string
+    val environment_file: string
   end
 
 module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor
diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
index 8ba1f8386..b410b6048 100644
--- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml
+++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
@@ -11,6 +11,8 @@ let broker_id = ref None
 let my_own_id = Hbugs_tutors_common.init_tutor ()
 let my_own_addr, my_own_port = "127.0.0.1", 50011
 let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
+let environment_file = "search_pattern_apply.environment"
+let dump_environment_on_exit = false
 
 let is_authenticated id =
   match !broker_id with
@@ -106,15 +108,36 @@ let callback mqi_handle (req: Http_types.request) outchan =
         (Exception ("parse_error", reason)))
       outchan
 
+let restore_environment () =
+  let ic = open_in environment_file in
+  prerr_endline "Restoring environment ...";
+  CicEnvironment.restore_from_channel
+    ~callback:(fun uri -> prerr_endline uri) ic;
+  prerr_endline "... done!";
+  close_in ic
+
+let dump_environment () =
+  let oc = open_out environment_file in
+  prerr_endline "Dumping environment ...";
+  CicEnvironment.dump_to_channel
+    ~callback:(fun uri -> prerr_endline uri) oc;
+  prerr_endline "... done!";
+  close_out oc
+
 let main () =
   let mqi_flags = [] in (* default MathQL interpreter options *)
   try
     Sys.catch_break true;
-    at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id);
+    at_exit (fun () ->
+      if dump_environment_on_exit then
+        dump_environment ();
+      Hbugs_tutors_common.unregister_from_broker my_own_id);
     broker_id :=
       Some (Hbugs_tutors_common.register_to_broker
         my_own_id my_own_url "FOO" "Search_pattern_apply tutor");
     let mqi_handle = MQIC.init mqi_flags prerr_string in 
+    if Sys.file_exists environment_file then
+      restore_environment ();
     Http_daemon.start'
       ~addr:my_own_addr ~port:my_own_port ~mode:`Thread (callback mqi_handle);
     MQIC.close mqi_handle