# HG changeset patch
# User wenzelm
# Date 1521841118 -3600
# Node ID da44f151f716cb7d3ba180a31fedc5b7b9039d7e
# Parent  91eb307511bb00e4750b12f9f77c019ddc0e9d17
clarified;

diff -r 91eb307511bb -r da44f151f716 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Fri Mar 23 22:31:50 2018 +0100
+++ b/src/Doc/System/Server.thy	Fri Mar 23 22:38:38 2018 +0100
@@ -929,9 +929,11 @@
   specifications may be given, which is occasionally useful for precise error
   locations.
 
-  \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
-  the imported theory. Normally this is determined implicitly from the parent
-  directory of the theory file.
+  \<^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 a
+  session-qualified theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute
+  path name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq"\<close>).
 
   \<^medskip>
   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The