Commit 792ac412 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Can reload after parse error.

parent 56e63454
......@@ -334,37 +334,16 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
module C = Controller_itp.Make(S)
(* Manipulations of files that handle errors *)
let cont_from_session_dir cont f =
try cont_from_session_dir cont f; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s)); false
let cont_from_file cont f =
try cont_from_file cont f; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s)); false
let reload_files cont ~use_shapes =
try reload_files cont ~use_shapes; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s)); false
let add_file c ?format fname =
try add_file c ?format fname; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s)); false
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
type server_data =
{ config : Whyconf.config;
task_driver : Driver.driver;
sd_provers : Whyconf.config_prover Whyconf.Mprover.t;
(* true if the controller is in a correct state *)
mutable cont_status: bool;
(* Session file used in the first correct state of the controller *)
mutable init_file: string option;
cont : Controller_itp.controller;
}
......@@ -377,6 +356,78 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
exit 1
| Some x -> x
(*********************)
(* File input/output *)
(*********************)
let read_and_send f =
try
let d = get_server_data() in
let fn = Sysutil.absolutize_filename
(Session_itp.get_dir d.cont.controller_session) f in
let s = Sysutil.file_contents fn in
P.notify (File_contents (f, s))
with Invalid_argument s ->
P.notify (Message (Error s))
let save_file f file_content =
try
let d = get_server_data() in
let fn = Sysutil.absolutize_filename
(Session_itp.get_dir d.cont.controller_session) f in
Sysutil.write_file fn file_content;
P.notify (Message (File_Saved f))
with Invalid_argument s ->
P.notify (Message (Error s))
(* Send source file from the controller to the IDE even if the controller's
status is not correct *)
let load_files_session () =
let d = get_server_data () in
let s = d.cont.controller_session in
let files = Session_itp.get_files s in
Stdlib.Hstr.iter (fun _ f -> read_and_send f.file_name) files
(* Manipulations of files that handle errors and update the status of the
controller in server data. *)
let cont_from_session_dir cont f =
let d = get_server_data () in
try cont_from_session_dir cont f; d.cont_status <- true; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s));
d.cont_status <- false;
load_files_session ();
false
let cont_from_file cont f =
let d = get_server_data () in
(* Tries to reload even if controller is not correct to regenerate a
correct one. *)
try cont_from_file cont f; d.cont_status <- true; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s));
d.cont_status <- false;
false
(* Reload_files that is used even if the controller is not correct. It can
be incorrect and end up in a correct state. *)
let reload_files cont ~use_shapes =
let d = get_server_data () in
try reload_files cont ~use_shapes; d.cont_status <- true; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s));
d.cont_status <- false;
false
let add_file c ?format fname =
try add_file c ?format fname; true with
| e ->
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
P.notify (Message (Parse_Or_Type_Error s)); false
let task_driver config env =
try
let main = Whyconf.get_main config in
......@@ -412,32 +463,13 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
{ config = config;
task_driver = task_driver;
sd_provers = provers;
(* controller is not initialized with a session -> incorrect state *)
cont_status = false;
init_file = None;
cont = c }
(*********************)
(* File input/output *)
(*********************)
let read_and_send f =
try
let d = get_server_data() in
let fn = Sysutil.absolutize_filename
(Session_itp.get_dir d.cont.controller_session) f in
let s = Sysutil.file_contents fn in
P.notify (File_contents (f, s))
with Invalid_argument s ->
P.notify (Message (Error s))
let save_file f file_content =
try
let d = get_server_data() in
let fn = Sysutil.absolutize_filename
(Session_itp.get_dir d.cont.controller_session) f in
Sysutil.write_file fn file_content;
P.notify (Message (File_Saved f))
with Invalid_argument s ->
P.notify (Message (Error s))
......@@ -791,6 +823,29 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
P.notify (Dead (Pp.string_of Exn_printer.exn_printer e));
exit 1
(* Safe reload_files that do not make inconsistent server_data. If
reload_files fail, stable_cont is set to false and we know the
controller is in bad state *)
let reload_files cont ~use_shapes =
let d = get_server_data () in
(* First try to regenerate the controller with same arguments as its last
correct generation *)
if not d.cont_status then
begin
match d.init_file with
| None -> P.notify (Message (Error "You have to successfully open a \
session at least once before reloading")); false
| Some f ->
let b = init_cont f in
if b then
reload_files cont ~use_shapes
else
false (* Eventually print debug here *)
end
else
reload_files cont ~use_shapes
(* ----------------- Schedule proof attempt -------------------- *)
(* Callback of a proof_attempt *)
......@@ -902,9 +957,12 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let reload_session () : unit =
let d = get_server_data () in
clear_tables ();
(* Calling reload_files breaks the controller if it fails *)
let b = reload_files d.cont ~use_shapes:true in
if b then
init_and_send_the_tree ()
else
d.cont_status <- false
let replay_session () : unit =
let d = get_server_data () in
......@@ -935,7 +993,6 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* ----------------- treat_request -------------------- *)
let get_proof_node_id nid =
try
match any_from_node_ID nid with
......@@ -1012,14 +1069,13 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let f = Sysutil.relativize_filename
(Session_itp.get_dir d.cont.controller_session) f in
read_and_send f
| Open_session_req file_or_dir_name ->
begin
| Open_session_req file_or_dir_name ->
let b = init_cont file_or_dir_name in
d.init_file <- Some file_or_dir_name;
if b then
reload_session ()
else
() (* Eventually print debug here *)
end
| Set_max_tasks_req i -> C.set_max_tasks i
| Exit_req -> exit 0
)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment