--- a/src/Doc/System/Server.thy Thu Mar 22 17:00:48 2018 +0100
+++ b/src/Doc/System/Server.thy Thu Mar 22 17:05:06 2018 +0100
@@ -764,7 +764,7 @@
argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
- regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id\<close> \\
+ regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id \<oplus> {tmp_dir: string}\<close> \\
error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
\end{tabular}
@@ -806,6 +806,13 @@
The \<open>session_id\<close> provides the internal identification of the session object
within the sever process. It can remain active as long as the server is
running, independently of the current client connection.
+
+ \<^medskip>
+ The \<open>tmp_dir\<close> fields reveals a temporary directory that is specifically
+ created for this session and deleted after it has been stopped. This may
+ serve as auxiliary file-space for the \<^verbatim>\<open>use_theories\<close> command, but
+ concurrent use requires some care in naming temporary files, e.g.\ by
+ using sub-directories with globally unique names.
\<close>
--- a/src/Pure/Thy/thy_resources.scala Thu Mar 22 17:00:48 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala Thu Mar 22 17:05:06 2018 +0100
@@ -7,6 +7,9 @@
package isabelle
+import java.io.{File => JFile}
+
+
object Thy_Resources
{
/* PIDE session */
@@ -75,6 +78,14 @@
{
session =>
+ val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
+
+ override def stop(): Process_Result =
+ {
+ try { super.stop() }
+ finally { Isabelle_System.rm_tree(tmp_dir) }
+ }
+
def use_theories(
theories: List[(String, Position.T)],
qualifier: String = Sessions.DRAFT,
--- a/src/Pure/Tools/server_commands.scala Thu Mar 22 17:00:48 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Thu Mar 22 17:05:06 2018 +0100
@@ -137,7 +137,12 @@
val id = UUID()
- (JSON.Object("session_id" -> id.toString), id -> session)
+ val res =
+ JSON.Object(
+ "session_id" -> id.toString,
+ "tmp_dir" -> File.path(session.tmp_dir).implode)
+
+ (res, id -> session)
}
}