changeset 67938 da44f151f716
parent 67937 91eb307511bb
child 67940 b4e80f062fbf
--- 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
-  \<^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>).
   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The