src/Doc/System/Server.thy
changeset 67946 e1e57c288e45
parent 67944 cb2b1a75ff59
child 68106 a514e29db980
     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>