eliminated default_qualifier: just a constant;
authorwenzelm
Fri Apr 21 14:09:03 2017 +0200 (2017-04-21)
changeset 65532febfd9f78bd4
parent 65531 24544e3f183d
child 65533 4a7e794944df
eliminated default_qualifier: just a constant;
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/update_imports.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/ML/ml_process.scala	Fri Apr 21 13:51:43 2017 +0200
     1.2 +++ b/src/Pure/ML/ml_process.scala	Fri Apr 21 14:09:03 2017 +0200
     1.3 @@ -99,8 +99,8 @@
     1.4              ML_Syntax.print_list(
     1.5                ML_Syntax.print_pair(
     1.6                  ML_Syntax.print_string, ML_Syntax.print_string))(table)
     1.7 -          List("Resources.init_session_base {default_qualifier = \"\"" +
     1.8 -            ", global_theories = " + print_table(base.global_theories.toList) +
     1.9 +          List("Resources.init_session_base" +
    1.10 +            " {global_theories = " + print_table(base.global_theories.toList) +
    1.11              ", loaded_theories = " + print_table(base.loaded_theories.toList) +
    1.12              ", known_theories = " + print_table(base.dest_known_theories) + "}")
    1.13        }
     2.1 --- a/src/Pure/PIDE/protocol.ML	Fri Apr 21 13:51:43 2017 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Apr 21 14:09:03 2017 +0200
     2.3 @@ -19,13 +19,12 @@
     2.4  
     2.5  val _ =
     2.6    Isabelle_Process.protocol_command "Prover.session_base"
     2.7 -    (fn [default_qualifier, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
     2.8 +    (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
     2.9        let
    2.10          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
    2.11        in
    2.12          Resources.init_session_base
    2.13 -          {default_qualifier = default_qualifier,
    2.14 -           global_theories = decode_table global_theories_yxml,
    2.15 +          {global_theories = decode_table global_theories_yxml,
    2.16             loaded_theories = decode_table loaded_theories_yxml,
    2.17             known_theories = decode_table known_theories_yxml}
    2.18        end);
     3.1 --- a/src/Pure/PIDE/protocol.scala	Fri Apr 21 13:51:43 2017 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Apr 21 14:09:03 2017 +0200
     3.3 @@ -312,7 +312,6 @@
     3.4  
     3.5    def session_base(resources: Resources): Unit =
     3.6      protocol_command("Prover.session_base",
     3.7 -      Symbol.encode(resources.default_qualifier),
     3.8        encode_table(resources.session_base.global_theories.toList),
     3.9        encode_table(resources.session_base.loaded_theories.toList),
    3.10        encode_table(resources.session_base.dest_known_theories))
     4.1 --- a/src/Pure/PIDE/resources.ML	Fri Apr 21 13:51:43 2017 +0200
     4.2 +++ b/src/Pure/PIDE/resources.ML	Fri Apr 21 14:09:03 2017 +0200
     4.3 @@ -6,13 +6,12 @@
     4.4  
     4.5  signature RESOURCES =
     4.6  sig
     4.7 +  val default_qualifier: string
     4.8    val init_session_base:
     4.9 -    {default_qualifier: string,
    4.10 -     global_theories: (string * string) list,
    4.11 +    {global_theories: (string * string) list,
    4.12       loaded_theories: (string * string) list,
    4.13       known_theories: (string * string) list} -> unit
    4.14    val finish_session_base: unit -> unit
    4.15 -  val default_qualifier: unit -> string
    4.16    val global_theory: string -> string option
    4.17    val loaded_theory: string -> string option
    4.18    val known_theory: string -> Path.T option
    4.19 @@ -37,36 +36,32 @@
    4.20  
    4.21  (* session base *)
    4.22  
    4.23 +val default_qualifier = "Draft";
    4.24 +
    4.25  val empty_session_base =
    4.26 -  {default_qualifier = "Draft",
    4.27 -   global_theories = Symtab.empty: string Symtab.table,
    4.28 +  {global_theories = Symtab.empty: string Symtab.table,
    4.29     loaded_theories = Symtab.empty: string Symtab.table,
    4.30     known_theories = Symtab.empty: Path.T Symtab.table};
    4.31  
    4.32  val global_session_base =
    4.33    Synchronized.var "Sessions.base" empty_session_base;
    4.34  
    4.35 -fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
    4.36 +fun init_session_base {global_theories, loaded_theories, known_theories} =
    4.37    Synchronized.change global_session_base
    4.38      (fn _ =>
    4.39 -      {default_qualifier =
    4.40 -        if default_qualifier <> "" then default_qualifier
    4.41 -        else #default_qualifier empty_session_base,
    4.42 -       global_theories = Symtab.make global_theories,
    4.43 +      {global_theories = Symtab.make global_theories,
    4.44         loaded_theories = Symtab.make loaded_theories,
    4.45         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    4.46  
    4.47  fun finish_session_base () =
    4.48    Synchronized.change global_session_base
    4.49      (fn {global_theories, loaded_theories, ...} =>
    4.50 -      {default_qualifier = #default_qualifier empty_session_base,
    4.51 -       global_theories = global_theories,
    4.52 +      {global_theories = global_theories,
    4.53         loaded_theories = loaded_theories,
    4.54         known_theories = #known_theories empty_session_base});
    4.55  
    4.56  fun get_session_base f = f (Synchronized.value global_session_base);
    4.57  
    4.58 -fun default_qualifier () = get_session_base #default_qualifier;
    4.59  fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
    4.60  fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    4.61  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
     5.1 --- a/src/Pure/PIDE/resources.scala	Fri Apr 21 13:51:43 2017 +0200
     5.2 +++ b/src/Pure/PIDE/resources.scala	Fri Apr 21 14:09:03 2017 +0200
     5.3 @@ -15,7 +15,6 @@
     5.4  
     5.5  class Resources(
     5.6    val session_base: Sessions.Base,
     5.7 -  val default_qualifier: String = Sessions.DRAFT,
     5.8    val log: Logger = No_Logger)
     5.9  {
    5.10    val thy_info = new Thy_Info(this)
     6.1 --- a/src/Pure/Thy/sessions.scala	Fri Apr 21 13:51:43 2017 +0200
     6.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 21 14:09:03 2017 +0200
     6.3 @@ -150,7 +150,7 @@
     6.4                parent_base.copy(known =
     6.5                  Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
     6.6  
     6.7 -            val resources = new Resources(imports_base, default_qualifier = info.theory_qualifier)
     6.8 +            val resources = new Resources(imports_base)
     6.9  
    6.10              if (verbose || list_files) {
    6.11                val groups =
     7.1 --- a/src/Pure/Thy/thy_info.ML	Fri Apr 21 13:51:43 2017 +0200
     7.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Apr 21 14:09:03 2017 +0200
     7.3 @@ -408,7 +408,7 @@
     7.4  fun use_thy name =
     7.5    use_theories
     7.6      {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
     7.7 -     qualifier = Resources.default_qualifier (), master_dir = Path.current}
     7.8 +     qualifier = Resources.default_qualifier, master_dir = Path.current}
     7.9      [(name, Position.none)];
    7.10  
    7.11  
     8.1 --- a/src/Pure/Tools/build.ML	Fri Apr 21 13:51:43 2017 +0200
     8.2 +++ b/src/Pure/Tools/build.ML	Fri Apr 21 14:09:03 2017 +0200
     8.3 @@ -182,8 +182,7 @@
     8.4  
     8.5      val _ =
     8.6        Resources.init_session_base
     8.7 -        {default_qualifier = name,
     8.8 -         global_theories = global_theories,
     8.9 +        {global_theories = global_theories,
    8.10           loaded_theories = loaded_theories,
    8.11           known_theories = known_theories};
    8.12  
     9.1 --- a/src/Pure/Tools/build.scala	Fri Apr 21 13:51:43 2017 +0200
     9.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 21 14:09:03 2017 +0200
     9.3 @@ -223,7 +223,7 @@
     9.4              ML_Syntax.print_string0(File.platform_path(output))
     9.5  
     9.6          if (pide && !Sessions.is_pure(name)) {
     9.7 -          val resources = new Resources(deps(parent), default_qualifier = info.theory_qualifier)
     9.8 +          val resources = new Resources(deps(parent))
     9.9            val session = new Session(options, resources)
    9.10            val handler = new Handler(progress, session, name)
    9.11            session.init_protocol_handler(handler)
    10.1 --- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 13:51:43 2017 +0200
    10.2 +++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 14:09:03 2017 +0200
    10.3 @@ -68,7 +68,7 @@
    10.4      {
    10.5        val info = full_sessions(session_name)
    10.6        val session_base = deps(session_name)
    10.7 -      val resources = new Resources(session_base, default_qualifier = info.theory_qualifier)
    10.8 +      val resources = new Resources(session_base)
    10.9        val local_theories = session_base.known.theories_local.iterator.map(_._2).toSet
   10.10  
   10.11        def standard_import(qualifier: String, s: String): String =
    11.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Apr 21 13:51:43 2017 +0200
    11.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Apr 21 14:09:03 2017 +0200
    11.3 @@ -63,7 +63,7 @@
    11.4    def node_name(file: JFile): Document.Node.Name =
    11.5      session_base.known.get_file(file) getOrElse {
    11.6        val node = file.getPath
    11.7 -      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    11.8 +      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
    11.9          case (true, theory) => Document.Node.Name.loaded_theory(theory)
   11.10          case (false, theory) =>
   11.11            val master_dir = if (theory == "") "" else file.getParent
    12.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Apr 21 13:51:43 2017 +0200
    12.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Apr 21 14:09:03 2017 +0200
    12.3 @@ -32,7 +32,7 @@
    12.4      known_file(path) getOrElse {
    12.5        val vfs = VFSManager.getVFSForPath(path)
    12.6        val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    12.7 -      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    12.8 +      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
    12.9          case (true, theory) => Document.Node.Name.loaded_theory(theory)
   12.10          case (false, theory) =>
   12.11            val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)