session tmp_dir is default master_dir;
authorwenzelm
Sat Mar 24 21:14:49 2018 +0100 (14 months ago)
changeset 67946e1e57c288e45
parent 67945 984c3dc46cc0
child 67947 ad735a551a11
session tmp_dir is default master_dir;
src/Doc/System/Server.thy
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Doc/System/Server.thy	Sat Mar 24 20:51:42 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Sat Mar 24 21:14:49 2018 +0100
     1.3 @@ -814,11 +814,15 @@
     1.4    running, independently of the current client connection.
     1.5  
     1.6    \<^medskip>
     1.7 -  The \<open>tmp_dir\<close> fields reveals a temporary directory that is specifically
     1.8 +  The \<open>tmp_dir\<close> field refers to a temporary directory that is specifically
     1.9    created for this session and deleted after it has been stopped. This may
    1.10    serve as auxiliary file-space for the \<^verbatim>\<open>use_theories\<close> command, but
    1.11    concurrent use requires some care in naming temporary files, e.g.\ by
    1.12    using sub-directories with globally unique names.
    1.13 +
    1.14 +  As \<open>tmp_dir\<close> is the default \<open>master_dir\<close> for commands \<^verbatim>\<open>use_theories\<close> and
    1.15 +  \<^verbatim>\<open>purge_theories\<close>, theory files copied there may be used without further
    1.16 +  path specification.
    1.17  \<close>
    1.18  
    1.19  
    1.20 @@ -887,10 +891,12 @@
    1.21    \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
    1.22    \quad\<open>{session_id: uuid,\<close> \\
    1.23    \quad~~\<open>theories: [string],\<close> \\
    1.24 -  \quad~~\<open>master_dir?: string,\<close> \\
    1.25 +  \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
    1.26    \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
    1.27    \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
    1.28 +  \end{tabular}
    1.29  
    1.30 +  \begin{tabular}{ll}
    1.31    \<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
    1.32    \quad\<open>{ok: bool,\<close> \\
    1.33    \quad~~\<open>errors: [message],\<close> \\
    1.34 @@ -926,8 +932,8 @@
    1.35    \<^medskip>
    1.36    The \<open>master_dir\<close> field specifies the master directory of imported theories:
    1.37    it acts like the ``current working directory'' for locating theory files.
    1.38 -  This may be omitted if all entries of \<open>theories\<close> use an absolute path name
    1.39 -  (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
    1.40 +  This is irrelevant for \<open>theories\<close> with an absolute path name (e.g.\
    1.41 +  \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
    1.42    \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
    1.43  
    1.44    \<^medskip>
    1.45 @@ -1006,11 +1012,11 @@
    1.46    regular result: & \<^verbatim>\<open>OK\<close> \<open>purge_theories_result\<close> \\
    1.47    \end{tabular}
    1.48  
    1.49 -  \begin{tabular}{ll}
    1.50 +  \begin{tabular}{lll}
    1.51    \<^bold>\<open>type\<close> \<open>purge_theories_arguments =\<close> \\
    1.52    \quad\<open>{session_id: uuid,\<close> \\
    1.53    \quad~~\<open>theories: [string],\<close> \\
    1.54 -  \quad~~\<open>master_dir?: string,\<close> \\
    1.55 +  \quad~~\<open>master_dir?: string,\<close> & \<^bold>\<open>default:\<close> session \<open>tmp_dir\<close> \\
    1.56    \quad~~\<open>all?: bool}\<close> \\[2ex]
    1.57    \end{tabular}
    1.58  
    1.59 @@ -1039,7 +1045,7 @@
    1.60  
    1.61    \<^medskip>
    1.62    The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>.
    1.63 -  It is redundant, when passing fully-qualified theory node names (e.g.\
    1.64 +  This is irrelevant, when passing fully-qualified theory node names (e.g.\
    1.65    \<open>node_name\<close> from \<open>nodes\<close> in \<open>use_theories_results\<close>).
    1.66  
    1.67    \<^medskip>
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 24 20:51:42 2018 +0100
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 24 21:14:49 2018 +0100
     2.3 @@ -80,6 +80,7 @@
     2.4      session =>
     2.5  
     2.6      val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
     2.7 +    val tmp_dir_name: String = File.path(tmp_dir).implode
     2.8  
     2.9      override def toString: String = session_name
    2.10  
    2.11 @@ -101,7 +102,7 @@
    2.12      {
    2.13        val dep_theories =
    2.14          resources.load_theories(session, id, theories, qualifier = qualifier,
    2.15 -          master_dir = master_dir, progress = progress)
    2.16 +          master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress)
    2.17  
    2.18        val result = Future.promise[Theories_Result]
    2.19  
    2.20 @@ -147,7 +148,7 @@
    2.21          master_dir: String = "",
    2.22          all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
    2.23        resources.purge_theories(session, theories = theories, qualifier = qualifier,
    2.24 -        master_dir = master_dir, all = all)
    2.25 +        master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
    2.26    }
    2.27  
    2.28  
    2.29 @@ -235,9 +236,9 @@
    2.30      session: Session,
    2.31      id: UUID,
    2.32      theories: List[String],
    2.33 -    qualifier: String = Sessions.DRAFT,
    2.34 -    master_dir: String = "",
    2.35 -    progress: Progress = No_Progress): List[Document.Node.Name] =
    2.36 +    qualifier: String,
    2.37 +    master_dir: String,
    2.38 +    progress: Progress): List[Document.Node.Name] =
    2.39    {
    2.40      val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
    2.41      val dependencies = resources.dependencies(import_names, progress = progress).check_errors
    2.42 @@ -295,9 +296,9 @@
    2.43  
    2.44    def purge_theories(session: Session,
    2.45      theories: List[String],
    2.46 -    qualifier: String = Sessions.DRAFT,
    2.47 -    master_dir: String = "",
    2.48 -    all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
    2.49 +    qualifier: String,
    2.50 +    master_dir: String,
    2.51 +    all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
    2.52    {
    2.53      val nodes = theories.map(import_name(qualifier, master_dir, _))
    2.54