provide tmp_dir for server session;
authorwenzelm
Thu Mar 22 17:05:06 2018 +0100 (14 months ago)
changeset 6792574dce5658d4c
parent 67924 b2cdd24e83b6
child 67926 e6b9703b9656
provide tmp_dir for server session;
src/Doc/System/Server.thy
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Thu Mar 22 17:00:48 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Thu Mar 22 17:05:06 2018 +0100
     1.3 @@ -764,7 +764,7 @@
     1.4    argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
     1.5    immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
     1.6    notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
     1.7 -  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id\<close> \\
     1.8 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id \<oplus> {tmp_dir: string}\<close> \\
     1.9    error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
    1.10    \end{tabular}
    1.11  
    1.12 @@ -806,6 +806,13 @@
    1.13    The \<open>session_id\<close> provides the internal identification of the session object
    1.14    within the sever process. It can remain active as long as the server is
    1.15    running, independently of the current client connection.
    1.16 +
    1.17 +  \<^medskip>
    1.18 +  The \<open>tmp_dir\<close> fields reveals a temporary directory that is specifically
    1.19 +  created for this session and deleted after it has been stopped. This may
    1.20 +  serve as auxiliary file-space for the \<^verbatim>\<open>use_theories\<close> command, but
    1.21 +  concurrent use requires some care in naming temporary files, e.g.\ by
    1.22 +  using sub-directories with globally unique names.
    1.23  \<close>
    1.24  
    1.25  
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Thu Mar 22 17:00:48 2018 +0100
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Thu Mar 22 17:05:06 2018 +0100
     2.3 @@ -7,6 +7,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8 +
     2.9 +
    2.10  object Thy_Resources
    2.11  {
    2.12    /* PIDE session */
    2.13 @@ -75,6 +78,14 @@
    2.14    {
    2.15      session =>
    2.16  
    2.17 +    val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
    2.18 +
    2.19 +    override def stop(): Process_Result =
    2.20 +    {
    2.21 +      try { super.stop() }
    2.22 +      finally { Isabelle_System.rm_tree(tmp_dir) }
    2.23 +    }
    2.24 +
    2.25      def use_theories(
    2.26        theories: List[(String, Position.T)],
    2.27        qualifier: String = Sessions.DRAFT,
     3.1 --- a/src/Pure/Tools/server_commands.scala	Thu Mar 22 17:00:48 2018 +0100
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Thu Mar 22 17:05:06 2018 +0100
     3.3 @@ -137,7 +137,12 @@
     3.4  
     3.5        val id = UUID()
     3.6  
     3.7 -      (JSON.Object("session_id" -> id.toString), id -> session)
     3.8 +      val res =
     3.9 +        JSON.Object(
    3.10 +          "session_id" -> id.toString,
    3.11 +          "tmp_dir" -> File.path(session.tmp_dir).implode)
    3.12 +
    3.13 +      (res, id -> session)
    3.14      }
    3.15    }
    3.16