# HG changeset patch
# User wenzelm
# Date 1521840710 -3600
# Node ID 91eb307511bb00e4750b12f9f77c019ddc0e9d17
# Parent  141a93b93aa6992e8d7714519d7433864eaafcf4
removed somewhat pointless argument;

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>\<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.
diff -r 141a93b93aa6 -r 91eb307511bb src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:26:50 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:31:50 2018 +0100
@@ -10,7 +10,6 @@
 object Server_Commands
 {
   def default_preferences: String = Options.read_prefs()
-  def default_qualifier: String = Sessions.DRAFT
 
   def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] =
     json match {
@@ -166,7 +165,6 @@
     sealed case class Args(
       session_id: UUID,
       theories: List[(String, Position.T)],
-      qualifier: String = default_qualifier,
       master_dir: String = "",
       pretty_margin: Double = Pretty.default_margin,
       unicode_symbols: Boolean = false)
@@ -175,13 +173,12 @@
       for {
         session_id <- JSON.uuid(json, "session_id")
         theories <- JSON.list(json, "theories", unapply_name_pos _)
-        qualifier <- JSON.string_default(json, "qualifier", default_qualifier)
         master_dir <- JSON.string_default(json, "master_dir")
         pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
         unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
       }
       yield {
-        Args(session_id, theories, qualifier = qualifier, master_dir = master_dir,
+        Args(session_id, theories, master_dir = master_dir,
           pretty_margin = pretty_margin, unicode_symbols)
       }
 
@@ -191,8 +188,8 @@
       progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
     {
       val result =
-        session.use_theories(args.theories, qualifier = args.qualifier,
-          master_dir = args.master_dir, id = id, progress = progress)
+        session.use_theories(args.theories, master_dir = args.master_dir,
+          id = id, progress = progress)
 
       def output_text(s: String): String =
         if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)