removed somewhat pointless argument;
authorwenzelm
Fri Mar 23 22:31:50 2018 +0100 (14 months ago)
changeset 6793791eb307511bb
parent 67936 141a93b93aa6
child 67938 da44f151f716
removed somewhat pointless argument;
src/Doc/System/Server.thy
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Fri Mar 23 22:26:50 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Fri Mar 23 22:31:50 2018 +0100
     1.3 @@ -884,7 +884,6 @@
     1.4    \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
     1.5    \quad\<open>{session_id: uuid,\<close> \\
     1.6    \quad~~\<open>theories: [theory_name],\<close> \\
     1.7 -  \quad~~\<open>qualifier?: string,\<close> \\
     1.8    \quad~~\<open>master_dir?: string,\<close> \\
     1.9    \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
    1.10    \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
    1.11 @@ -930,15 +929,6 @@
    1.12    specifications may be given, which is occasionally useful for precise error
    1.13    locations.
    1.14  
    1.15 -  \<^medskip>
    1.16 -  The \<open>qualifier\<close> field provides an alternative session qualifier for theories
    1.17 -  that are not formally recognized as a member of a particular session. The
    1.18 -  default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
    1.19 -  that, as theory nodes are already uniquely identified by their physical
    1.20 -  file-system location. This already allows reuse of theory base names with
    1.21 -  the same session qualifier --- as long as these theories are not used
    1.22 -  together (e.g.\ in \<^theory_text>\<open>imports\<close>).
    1.23 -
    1.24    \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
    1.25    the imported theory. Normally this is determined implicitly from the parent
    1.26    directory of the theory file.
     2.1 --- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:26:50 2018 +0100
     2.2 +++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:31:50 2018 +0100
     2.3 @@ -10,7 +10,6 @@
     2.4  object Server_Commands
     2.5  {
     2.6    def default_preferences: String = Options.read_prefs()
     2.7 -  def default_qualifier: String = Sessions.DRAFT
     2.8  
     2.9    def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] =
    2.10      json match {
    2.11 @@ -166,7 +165,6 @@
    2.12      sealed case class Args(
    2.13        session_id: UUID,
    2.14        theories: List[(String, Position.T)],
    2.15 -      qualifier: String = default_qualifier,
    2.16        master_dir: String = "",
    2.17        pretty_margin: Double = Pretty.default_margin,
    2.18        unicode_symbols: Boolean = false)
    2.19 @@ -175,13 +173,12 @@
    2.20        for {
    2.21          session_id <- JSON.uuid(json, "session_id")
    2.22          theories <- JSON.list(json, "theories", unapply_name_pos _)
    2.23 -        qualifier <- JSON.string_default(json, "qualifier", default_qualifier)
    2.24          master_dir <- JSON.string_default(json, "master_dir")
    2.25          pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin)
    2.26          unicode_symbols <- JSON.bool_default(json, "unicode_symbols")
    2.27        }
    2.28        yield {
    2.29 -        Args(session_id, theories, qualifier = qualifier, master_dir = master_dir,
    2.30 +        Args(session_id, theories, master_dir = master_dir,
    2.31            pretty_margin = pretty_margin, unicode_symbols)
    2.32        }
    2.33  
    2.34 @@ -191,8 +188,8 @@
    2.35        progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
    2.36      {
    2.37        val result =
    2.38 -        session.use_theories(args.theories, qualifier = args.qualifier,
    2.39 -          master_dir = args.master_dir, id = id, progress = progress)
    2.40 +        session.use_theories(args.theories, master_dir = args.master_dir,
    2.41 +          id = id, progress = progress)
    2.42  
    2.43        def output_text(s: String): String =
    2.44          if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s)