# HG changeset patch
# User wenzelm
# Date 1521734706 -3600
# Node ID 74dce5658d4c53a18a77b725de71a1cc6b37bbe8
# Parent  b2cdd24e83b608983937ad947d9926dc434c3280
provide tmp_dir for server session;

diff -r b2cdd24e83b6 -r 74dce5658d4c src/Doc/System/Server.thy
--- 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>
 
 
diff -r b2cdd24e83b6 -r 74dce5658d4c src/Pure/Thy/thy_resources.scala
--- 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,
diff -r b2cdd24e83b6 -r 74dce5658d4c src/Pure/Tools/server_commands.scala
--- 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)
     }
   }