--- a/NEWS Thu Sep 28 11:53:55 2017 +0200
+++ b/NEWS Thu Sep 28 15:11:32 2017 +0200
@@ -7,6 +7,14 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Session-qualified theory names are mandatory: it is no longer possible
+to refer to unqualified theories from the parent session.
+INCOMPATIBILITY for old developments that have not been updated to
+Isabelle2017 yet (using the "isabelle imports" tool).
+
+
*** HOL ***
* SMT module:
--- a/src/Pure/ML/ml_process.scala Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/ML/ml_process.scala Thu Sep 28 15:11:32 2017 +0200
@@ -99,9 +99,11 @@
ML_Syntax.print_list(
ML_Syntax.print_pair(
ML_Syntax.print_string, ML_Syntax.print_string))(table)
+ def print_list(list: List[String]): String =
+ ML_Syntax.print_list(ML_Syntax.print_string)(list)
List("Resources.init_session_base" +
" {global_theories = " + print_table(base.global_theories.toList) +
- ", loaded_theories = " + print_table(base.loaded_theories.toList) +
+ ", loaded_theories = " + print_list(base.loaded_theories.toList) +
", known_theories = " + print_table(base.dest_known_theories) + "}")
}
--- a/src/Pure/PIDE/protocol.ML Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML Thu Sep 28 15:11:32 2017 +0200
@@ -22,10 +22,11 @@
(fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
let
val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
+ val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
in
Resources.init_session_base
{global_theories = decode_table global_theories_yxml,
- loaded_theories = decode_table loaded_theories_yxml,
+ loaded_theories = decode_list loaded_theories_yxml,
known_theories = decode_table known_theories_yxml}
end);
--- a/src/Pure/PIDE/protocol.scala Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Sep 28 15:11:32 2017 +0200
@@ -316,12 +316,18 @@
Symbol.encode_yxml(list(pair(string, string))(table))
}
+ private def encode_list(lst: List[String]): String =
+ {
+ import XML.Encode._
+ Symbol.encode_yxml(list(string)(lst))
+ }
+
def session_base(resources: Resources)
{
val base = resources.session_base.standard_path
protocol_command("Prover.session_base",
encode_table(base.global_theories.toList),
- encode_table(base.loaded_theories.toList),
+ encode_list(base.loaded_theories.toList),
encode_table(base.dest_known_theories))
}
--- a/src/Pure/PIDE/resources.ML Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/resources.ML Thu Sep 28 15:11:32 2017 +0200
@@ -9,11 +9,11 @@
val default_qualifier: string
val init_session_base:
{global_theories: (string * string) list,
- loaded_theories: (string * string) list,
+ loaded_theories: string list,
known_theories: (string * string) list} -> unit
val finish_session_base: unit -> unit
val global_theory: string -> string option
- val loaded_theory: string -> string option
+ val loaded_theory: string -> bool
val known_theory: string -> Path.T option
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
@@ -39,7 +39,7 @@
val empty_session_base =
{global_theories = Symtab.empty: string Symtab.table,
- loaded_theories = Symtab.empty: string Symtab.table,
+ loaded_theories = Symtab.empty: unit Symtab.table,
known_theories = Symtab.empty: Path.T Symtab.table};
val global_session_base =
@@ -49,7 +49,7 @@
Synchronized.change global_session_base
(fn _ =>
{global_theories = Symtab.make global_theories,
- loaded_theories = Symtab.make loaded_theories,
+ loaded_theories = Symtab.make_set loaded_theories,
known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
fun finish_session_base () =
@@ -62,7 +62,7 @@
fun get_session_base f = f (Synchronized.value global_session_base);
fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
-fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
+fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
@@ -107,15 +107,14 @@
SOME qualifier => qualifier
| NONE => Long_Name.qualifier theory);
-fun theory_name qualifier theory0 =
- (case loaded_theory theory0 of
- SOME theory => (true, theory)
- | NONE =>
- let val theory =
- if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
- then theory0
- else Long_Name.qualify qualifier theory0
- in (false, theory) end);
+fun theory_name qualifier theory =
+ if loaded_theory theory then (true, theory)
+ else
+ let val theory' =
+ if Long_Name.is_qualified theory orelse is_some (global_theory theory)
+ then theory
+ else Long_Name.qualify qualifier theory
+ in (false, theory') end;
fun import_name qualifier dir s =
(case theory_name qualifier (Thy_Header.import_name s) of
--- a/src/Pure/PIDE/resources.scala Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Thu Sep 28 15:11:32 2017 +0200
@@ -88,15 +88,14 @@
def theory_qualifier(name: Document.Node.Name): String =
session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
- def theory_name(qualifier: String, theory0: String): (Boolean, String) =
- session_base.loaded_theories.get(theory0) match {
- case Some(theory) => (true, theory)
- case None =>
- val theory =
- if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0))
- theory0
- else Long_Name.qualify(qualifier, theory0)
- (false, theory)
+ def theory_name(qualifier: String, theory: String): (Boolean, String) =
+ if (session_base.loaded_theory(theory)) (true, theory)
+ else {
+ val theory1 =
+ if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
+ theory
+ else Long_Name.qualify(qualifier, theory)
+ (false, theory1)
}
def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
--- a/src/Pure/Thy/sessions.scala Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Sep 28 15:11:32 2017 +0200
@@ -115,7 +115,7 @@
sealed case class Base(
pos: Position.T = Position.none,
global_theories: Map[String, String] = Map.empty,
- loaded_theories: Map[String, String] = Map.empty,
+ loaded_theories: Set[String] = Set.empty,
known: Known = Known.empty,
keywords: Thy_Header.Keywords = Nil,
syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -127,8 +127,8 @@
def platform_path: Base = copy(known = known.platform_path)
def standard_path: Base = copy(known = known.standard_path)
- def loaded_theory(name: Document.Node.Name): Boolean =
- loaded_theories.isDefinedAt(name.theory)
+ def loaded_theory(name: String): Boolean = loaded_theories.contains(name)
+ def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
def known_theory(name: String): Option[Document.Node.Name] =
known.theories.get(name)
--- a/src/Pure/Thy/thy_info.scala Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala Thu Sep 28 15:11:32 2017 +0200
@@ -61,13 +61,8 @@
lazy val syntax: Outer_Syntax =
resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
- def loaded_theories: Map[String, String] =
- (resources.session_base.loaded_theories /: rev_deps) {
- case (loaded, dep) =>
- val name = dep.name
- loaded + (name.theory -> name.theory) +
- (name.theory_base_name -> name.theory) // legacy
- }
+ def loaded_theories: Set[String] =
+ resources.session_base.loaded_theories ++ rev_deps.map(dep => dep.name.theory)
def loaded_files: List[(String, List[Path])] =
{
--- a/src/Pure/Tools/build.ML Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Tools/build.ML Thu Sep 28 15:11:32 2017 +0200
@@ -147,7 +147,7 @@
master_dir: Path.T,
theories: (Options.T * (string * Position.T) list) list,
global_theories: (string * string) list,
- loaded_theories: (string * string) list,
+ loaded_theories: string list,
known_theories: (string * string) list};
fun decode_args yxml =
@@ -162,7 +162,7 @@
(pair string
(pair (((list (pair Options.decode (list (pair string position))))))
(pair (list (pair string string))
- (pair (list (pair string string)) (list (pair string string)))))))))))))))
+ (pair (list string) (list (pair string string)))))))))))))))
(YXML.parse_body yxml);
in
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
--- a/src/Pure/Tools/build.scala Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/Tools/build.scala Thu Sep 28 15:11:32 2017 +0200
@@ -209,7 +209,7 @@
pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string, pair(Path.encode,
pair(list(pair(Options.encode, list(pair(string, properties)))),
- pair(list(pair(string, string)), pair(list(pair(string, string)),
+ pair(list(pair(string, string)), pair(list(string),
list(pair(string, string))))))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
(store.browser_info, (info.document_files, (File.standard_path(graph_file),