X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2Fsearch_pattern_apply_tutor.ml;h=b410b604827b2d4c3e003dc5ce1ecc496385955d;hb=05fb48fba4c9a1189bfba8eaa4fbb429f9e20b6c;hp=8ba1f8386b7c4846b2b8b4fbb07c2135fab54e2a;hpb=5a8190d19187ebd7876524173fa236e9975ff87f;p=helm.git

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