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
| hd::tl -> hd
in
let uris =
- TacticChaser.searchPattern mqi_handle
+ TacticChaser.matchConclusion mqi_handle
~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
in
if uris = [] then
(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