src/Doc/System/Server.thy
changeset 67937 91eb307511bb
parent 67931 f7917c15b566
child 67938 da44f151f716
--- 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>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
   \quad\<open>{session_id: uuid,\<close> \\
   \quad~~\<open>theories: [theory_name],\<close> \\
-  \quad~~\<open>qualifier?: string,\<close> \\
   \quad~~\<open>master_dir?: string,\<close> \\
   \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
   \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
@@ -930,15 +929,6 @@
   specifications may be given, which is occasionally useful for precise error
   locations.
 
-  \<^medskip>
-  The \<open>qualifier\<close> field provides an alternative session qualifier for theories
-  that are not formally recognized as a member of a particular session. The
-  default is \<^verbatim>\<open>Draft\<close> 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>\<open>imports\<close>).
-
   \<^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.