diff -r 141a93b93aa6 -r 91eb307511bb src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Fri Mar 23 22:26:50 2018 +0100 +++ b/src/Doc/System/Server.thy Fri Mar 23 22:31:50 2018 +0100 @@ -884,7 +884,6 @@ \<^bold>\type\ \use_theories_arguments =\ \\ \quad\{session_id: uuid,\ \\ \quad~~\theories: [theory_name],\ \\ - \quad~~\qualifier?: string,\ \\ \quad~~\master_dir?: string,\ \\ \quad~~\pretty_margin?: double\ & \<^bold>\default:\ \<^verbatim>\76\ \\ \quad~~\unicode_symbols?: bool}\ \\[2ex] @@ -930,15 +929,6 @@ specifications may be given, which is occasionally useful for precise error locations. - \<^medskip> - The \qualifier\ field provides an alternative session qualifier for theories - that are not formally recognized as a member of a particular session. The - default is \<^verbatim>\Draft\ as in Isabelle/jEdit. There is rarely a need to change - that, as theory nodes are already uniquely identified by their physical - file-system location. This already allows reuse of theory base names with - the same session qualifier --- as long as these theories are not used - together (e.g.\ in \<^theory_text>\imports\). - \<^medskip> The \master_dir\ field explicit specifies the formal master directory of the imported theory. Normally this is determined implicitly from the parent directory of the theory file.