Added comments/cleaning and get_file to get session files from name.

src/session/controller_itp.ml

@@ -459,7 +459,6 @@ let set_max_tasks n =
   max_number_of_running_provers := n;
   Prove_client.set_max_running_provers n
 
-
 let number_of_running_provers = ref 0
 
 let observer = ref (fun _ _ _ -> ())

src/session/itp_server.ml

@@ -857,20 +857,23 @@ end
      path from the session directory to the file. *)
   let add_file_to_session cont f =
     let fn = Sysutil.relativize_filename
-      (Session_itp.get_dir cont.controller_session) f in
-    let files = get_files cont.controller_session in
-    if (not (Stdlib.Hstr.mem files fn)) then
-      if (Sys.file_exists f) then
-      begin
-        let b = add_file cont f in
-        if b then
-          let file = Stdlib.Hstr.find files fn in
-          init_and_send_file file
-      end
-      else
-        P.notify (Message (Open_File_Error ("File not found: " ^ f)))
-    else
-      P.notify (Message (Open_File_Error ("File already in session: " ^ fn)))
+      (get_dir cont.controller_session) f in
+    let fn_exists =
+      try Some (get_file cont.controller_session fn)
+      with | Not_found -> None
+    in
+    match fn_exists with
+    | None ->
+        if (Sys.file_exists f) then
+          begin
+            let b = add_file cont f in
+            if b then
+              let file = get_file cont.controller_session fn in
+              init_and_send_file file
+          end
+        else
+          P.notify (Message (Open_File_Error ("File not found: " ^ f)))
+    | Some _ -> P.notify (Message (Open_File_Error ("File already in session: " ^ fn)))
 
 
   (* ------------ init server ------------ *)

src/session/session_itp.ml

@@ -154,6 +154,7 @@ let get_theories s =
  *)
 
 let get_files s = s.session_files
+let get_file s name = Hstr.find s.session_files name
 let get_dir s = s.session_dir
 
 let get_shape_version s = s.session_shape_version

src/session/session_itp.mli

@@ -37,6 +37,7 @@ type file = private {
   file_detached_theories : theory list;
 }
 
+(* Any proof node of the tree *)
 type any =
   | AFile of file
   | ATh of theory
@@ -44,15 +45,22 @@ type any =
   | APn of proofNodeID
   | APa of proofAttemptID
 
-val theory_name : theory -> Ident.ident
-val theory_goals : theory -> proofNodeID list
-val theory_detached_goals : theory -> proofNodeID list
-val theory_parent : session -> theory -> file
+(** Session / File *)
 
+(* Get all the files in the session *)
 val get_files : session -> file Stdlib.Hstr.t
+(* Get a single file in the session using its name *)
+val get_file: session -> string -> file
+(* Get directory containing the session *)
 val get_dir : session -> string
 val get_shape_version : session -> int
 
+(** Theory *)
+val theory_name : theory -> Ident.ident
+val theory_goals : theory -> proofNodeID list
+val theory_detached_goals : theory -> proofNodeID list
+val theory_parent : session -> theory -> file
+
 type proof_attempt_node = private {
   parent              : proofNodeID;
   prover              : Whyconf.prover;