clarified;
authorwenzelm
Fri Mar 23 22:38:38 2018 +0100 (14 months ago)
changeset 67938da44f151f716
parent 67937 91eb307511bb
child 67939 544a7a21298e
clarified;
src/Doc/System/Server.thy
     1.1 --- a/src/Doc/System/Server.thy	Fri Mar 23 22:31:50 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Fri Mar 23 22:38:38 2018 +0100
     1.3 @@ -929,9 +929,11 @@
     1.4    specifications may be given, which is occasionally useful for precise error
     1.5    locations.
     1.6  
     1.7 -  \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
     1.8 -  the imported theory. Normally this is determined implicitly from the parent
     1.9 -  directory of the theory file.
    1.10 +  \<^medskip> The \<open>master_dir\<close> field specifies the master directory of imported
    1.11 +  theories: it acts like the ``current working directory'' for locating theory
    1.12 +  files. This may be omitted if all entries of \<open>theories\<close> use a
    1.13 +  session-qualified theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute
    1.14 +  path name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq"\<close>).
    1.15  
    1.16    \<^medskip>
    1.17    The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The