# HG changeset patch
# User wenzelm
# Date 1521922489 -3600
# Node ID e1e57c288e45cdfff068001ca517e51dd2389c50
# Parent  984c3dc46cc0991caee8b4baf5d0704a6b67a24e
session tmp_dir is default master_dir;

diff -r 984c3dc46cc0 -r e1e57c288e45 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Mar 24 20:51:42 2018 +0100
+++ b/src/Doc/System/Server.thy	Sat Mar 24 21:14:49 2018 +0100
@@ -814,11 +814,15 @@
   running, independently of the current client connection.
 
   \<^medskip>
-  The \<open>tmp_dir\<close> fields reveals a temporary directory that is specifically
+  The \<open>tmp_dir\<close> field refers to 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.
+
+  As \<open>tmp_dir\<close> is the default \<open>master_dir\<close> for commands \<^verbatim>\<open>use_theories\<close> and
+  \<^verbatim>\<open>purge_theories\<close>, theory files copied there may be used without further
+  path specification.
 \<close>
 
 
@@ -887,10 +891,12 @@
   \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   \quad\<open>{session_id: uuid,\<close> \\
   \quad~~\<open>theories: [string],\<close> \\
-  \quad~~\<open>master_dir?: string,\<close> \\
+  \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
   \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
+  \end{tabular}
 
+  \begin{tabular}{ll}
   \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
   \quad\<open>{ok: bool,\<close> \\
   \quad~~\<open>errors: [message],\<close> \\
@@ -926,8 +932,8 @@
   \<^medskip>
   The \<open>master_dir\<close> field specifies the master directory of imported theories:
   it acts like the ``current working directory'' for locating theory files.
-  This may be omitted if all entries of \<open>theories\<close> use an absolute path name
-  (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
+  This is irrelevant for \<open>theories\<close> with an absolute path name (e.g.\
+  \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
   \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
 
   \<^medskip>
@@ -1006,11 +1012,11 @@
   regular result: & \<^verbatim>\<open>OK\<close> \<open>purge_theories_result\<close> \\
   \end{tabular}
 
-  \begin{tabular}{ll}
+  \begin{tabular}{lll}
   \<^bold>\<open>type\<close> \<open>purge_theories_arguments =\<close> \\
   \quad\<open>{session_id: uuid,\<close> \\
   \quad~~\<open>theories: [string],\<close> \\
-  \quad~~\<open>master_dir?: string,\<close> \\
+  \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
   \quad~~\<open>all?: bool}\<close> \\[2ex]
   \end{tabular}
 
@@ -1039,7 +1045,7 @@
 
   \<^medskip>
   The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>.
-  It is redundant, when passing fully-qualified theory node names (e.g.\
+  This is irrelevant, when passing fully-qualified theory node names (e.g.\
   \<open>node_name\<close> from \<open>nodes\<close> in \<open>use_theories_results\<close>).
 
   \<^medskip>
diff -r 984c3dc46cc0 -r e1e57c288e45 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Mar 24 20:51:42 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 24 21:14:49 2018 +0100
@@ -80,6 +80,7 @@
     session =>
 
     val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
+    val tmp_dir_name: String = File.path(tmp_dir).implode
 
     override def toString: String = session_name
 
@@ -101,7 +102,7 @@
     {
       val dep_theories =
         resources.load_theories(session, id, theories, qualifier = qualifier,
-          master_dir = master_dir, progress = progress)
+          master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
 
       val result = Future.promise[Theories_Result]
 
@@ -147,7 +148,7 @@
         master_dir: String = "",
         all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
       resources.purge_theories(session, theories = theories, qualifier = qualifier,
-        master_dir = master_dir, all = all)
+        master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
   }
 
 
@@ -235,9 +236,9 @@
     session: Session,
     id: UUID,
     theories: List[String],
-    qualifier: String = Sessions.DRAFT,
-    master_dir: String = "",
-    progress: Progress = No_Progress): List[Document.Node.Name] =
+    qualifier: String,
+    master_dir: String,
+    progress: Progress): List[Document.Node.Name] =
   {
     val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
     val dependencies = resources.dependencies(import_names, progress = progress).check_errors
@@ -295,9 +296,9 @@
 
   def purge_theories(session: Session,
     theories: List[String],
-    qualifier: String = Sessions.DRAFT,
-    master_dir: String = "",
-    all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
+    qualifier: String,
+    master_dir: String,
+    all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
   {
     val nodes = theories.map(import_name(qualifier, master_dir, _))