Commit a4d4e60a authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Removed cont_from_file. Only cont_from_session is needed.

Removed unnecessary duplications of cont_from*
parent c0a9864b
......@@ -1300,7 +1300,8 @@ let treat_notification n =
| Not_found -> create_source_view file_name content
end
| Dead _ ->
print_message "Serveur sent an unexpected notification '%a'. Please report." print_notify n
print_message "Serveur sent an unexpected notification '%a'. Please report."
print_notify n
end;
(* temporary: this should be better executed each time
one clicks on the tree view *)
......
......@@ -398,24 +398,6 @@ let () =
Format.eprintf "File : %s@." f.file_name;
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 =
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));
load_files_session ();
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));
load_files_session ();
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 =
......@@ -468,11 +450,6 @@ let () =
sd_provers = provers;
cont = c }
(* ----------------------------------- ------------------------------------- *)
let get_node_type (node: any) =
......@@ -810,42 +787,20 @@ let () =
List.map (fun (c,_,_) -> c) commands
}
in
try (
if Sys.file_exists f then
begin
if Sys.is_directory f then
begin
let b = cont_from_session_dir d.cont f in
if b then
P.notify (Initialized infos);
b
end
else
begin
let b = cont_from_file d.cont f in
if b then
begin
add_file_to_session d.cont f;
P.notify (Initialized infos);
end;
b
end
end
else
begin
P.notify (Message (Open_File_Error ("File not found: " ^ f)));
false
end)
with
| NotADirectory f ->
P.notify (Message (Open_File_Error ("Not a directory: " ^ f))); false
| BadFileName f ->
P.notify (Message (Open_File_Error ("Bad file name: " ^ f))); false
| e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
P.notify (Dead (Pp.string_of Exn_printer.exn_printer e));
exit 1
match cont_from_session ~notify:P.notify d.cont f with
| Some false ->
begin
add_file_to_session d.cont f;
P.notify (Initialized infos);
true
end
| Some true ->
P.notify (Initialized infos);
true
| None ->
(* Even if it fails we want to load source files *)
load_files_session ();
false
(* ----------------- Schedule proof attempt -------------------- *)
......
......@@ -5,6 +5,7 @@
replaced by proper server notifications *)
open Session_itp
open Itp_communication
exception NotADirectory of string
exception BadFileName of string
......@@ -13,11 +14,23 @@ exception BadFileName of string
(* Creation of the controller *)
(******************************)
let cont_from_session_dir cont dir =
(* [cont_from_session]: returns an option to a boolean which returns None in
case of failure, true if nothing is left to do and false if sessions was
loaded but [f] should still be added to the session as a file. *)
let cont_from_session ~notify cont f : bool option =
(* If a file is given, find the corresponding directory *)
let dir = try (Filename.chop_extension f) with
| Invalid_argument _ -> f in
(* create project directory if needed *)
if Sys.file_exists dir then
begin
if not (Sys.is_directory dir) then raise (NotADirectory dir)
(* Case of user giving a file that gets chopped to an other file *)
if not (Sys.is_directory dir) then
begin
let s = "Not a directory: " ^ dir in
Format.eprintf "%s@." s;
exit 1
end
end
else
begin
......@@ -31,13 +44,21 @@ let cont_from_session_dir cont dir =
(* create the controller *)
Controller_itp.init_controller ses cont;
(* update the session *)
Controller_itp.reload_files cont ~use_shapes
try (Controller_itp.reload_files cont ~use_shapes;
(* Check if the initial file given was a file or not. If it was, we return
that it should be added to the session. *)
if Sys.file_exists f && not (Sys.is_directory f) then
Some false
else
Some true) with
| e ->
begin
let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
notify (Message (Parse_Or_Type_Error s));
None
end
(* If we have a file we chop it and return new session based on the directory *)
let cont_from_file cont f =
let dir = try (Filename.chop_extension f) with
| Invalid_argument _ -> raise (BadFileName f) in
cont_from_session_dir cont dir
(******************)
......
......@@ -3,14 +3,10 @@ exception BadFileName of string
(** Controller initialization *)
(* Init the given controller with the session in directory given *)
val cont_from_session_dir: Controller_itp.controller -> string -> unit
(* Init the controller with the session located in a directory with the name of
the file without extension *)
val cont_from_file: Controller_itp.controller -> string -> unit
(* Init the given controller with the session in file/directory given *)
val cont_from_session:
notify:(Itp_communication.notification -> unit) ->
Controller_itp.controller -> string -> bool option
(** Simple queries *)
......
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