--- a/NEWS Fri Sep 29 16:55:08 2017 +0100
+++ b/NEWS Fri Sep 29 22:45:58 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/Isar/outer_syntax.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Fri Sep 29 22:45:58 2017 +0200
@@ -18,6 +18,10 @@
def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
+ def merge(syns: List[Outer_Syntax]): Outer_Syntax =
+ if (syns.isEmpty) Thy_Header.bootstrap_syntax
+ else (syns.head /: syns.tail)(_ ++ _)
+
/* string literals */
@@ -98,7 +102,10 @@
}
- /* merge */
+ /* build */
+
+ def + (header: Document.Node.Header): Outer_Syntax =
+ add_keywords(header.keywords).add_abbrevs(header.abbrevs)
def ++ (other: Outer_Syntax): Outer_Syntax =
if (this eq other) this
--- a/src/Pure/ML/ml_process.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Sep 29 22:45:58 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.keys) +
", known_theories = " + print_table(base.dest_known_theories) + "}")
}
--- a/src/Pure/PIDE/document.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/document.scala Fri Sep 29 22:45:58 2017 +0200
@@ -116,6 +116,8 @@
case _ => false
}
+ def path: Path = Path.explode(node)
+
def is_theory: Boolean = theory.nonEmpty
def theory_base_name: String = Long_Name.base_name(theory)
@@ -126,6 +128,11 @@
def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
}
+ sealed case class Entry(name: Node.Name, header: Node.Header)
+ {
+ override def toString: String = name.toString
+ }
+
/* node overlays */
--- a/src/Pure/PIDE/protocol.ML Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/protocol.ML Fri Sep 29 22:45:58 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 Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/protocol.scala Fri Sep 29 22:45:58 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.keys),
encode_table(base.dest_known_theories))
}
--- a/src/Pure/PIDE/resources.ML Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/resources.ML Fri Sep 29 22:45:58 2017 +0200
@@ -9,19 +9,18 @@
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
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
val thy_path: Path.T -> Path.T
val theory_qualifier: string -> string
- val import_name: string -> Path.T -> string ->
- {node_name: Path.T, master_dir: Path.T, theory_name: string}
+ val import_name: string -> Path.T -> string -> {master_dir: Path.T, theory_name: string}
val check_thy: Path.T -> string ->
{master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -40,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 =
@@ -50,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 () =
@@ -63,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;
@@ -108,26 +107,24 @@
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
- (true, theory) =>
- {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
+ (true, theory) => {master_dir = Path.current, theory_name = theory}
| (false, theory) =>
let val node_name =
(case known_theory theory of
SOME node_name => node_name
| NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
- in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end);
+ in {master_dir = Path.dir node_name, theory_name = theory} end);
fun check_file dir file = File.check_file (File.full_path dir file);
--- a/src/Pure/PIDE/resources.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Sep 29 22:45:58 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 =
@@ -118,7 +117,7 @@
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
- val path = File.check_file(Path.explode(name.node))
+ val path = File.check_file(name.path)
val reader = Scan.byte_reader(path.file)
try { f(reader) } finally { reader.close }
}
@@ -128,7 +127,7 @@
{
if (node_name.is_theory && reader.source.length > 0) {
try {
- val header = Thy_Header.read(reader, start, strict).decode_symbols
+ val header = Thy_Header.read(reader, start, strict)
val base_name = node_name.theory_base_name
val (name, pos) = header.name
--- a/src/Pure/PIDE/session.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/session.scala Fri Sep 29 22:45:58 2017 +0200
@@ -220,7 +220,7 @@
def recent_syntax(name: Document.Node.Name): Outer_Syntax =
global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
- resources.session_base.syntax
+ resources.session_base.overall_syntax
/* pipelined change parsing */
--- a/src/Pure/Thy/sessions.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Sep 29 22:45:58 2017 +0200
@@ -40,8 +40,7 @@
def local_theories_iterator =
{
val local_path = local_dir.canonical_file.toPath
- theories.iterator.filter(name =>
- Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
+ theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
}
val known_theories =
@@ -62,7 +61,7 @@
(Map.empty[JFile, List[Document.Node.Name]] /:
(bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
case (known, name) =>
- val file = Path.explode(name.node).canonical_file
+ val file = name.path.canonical_file
val theories1 = known.getOrElse(file, Nil)
if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
known
@@ -103,22 +102,18 @@
object Base
{
- def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
-
def bootstrap(global_theories: Map[String, String]): Base =
Base(
global_theories = global_theories,
- keywords = Thy_Header.bootstrap_header,
- syntax = Thy_Header.bootstrap_syntax)
+ overall_syntax = Thy_Header.bootstrap_syntax)
}
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: Graph[String, Outer_Syntax] = Graph.string,
known: Known = Known.empty,
- keywords: Thy_Header.Keywords = Nil,
- syntax: Outer_Syntax = Outer_Syntax.empty,
+ overall_syntax: Outer_Syntax = Outer_Syntax.empty,
sources: List[(Path, SHA1.Digest)] = Nil,
session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
errors: List[String] = Nil,
@@ -127,8 +122,16 @@
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.defined(name)
+ def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
+
+ def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
+ if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
+ def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
+ loaded_theory_syntax(name.theory)
+
+ def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Option[Outer_Syntax] =
+ nodes(name).syntax orElse loaded_theory_syntax(name)
def known_theory(name: String): Option[Document.Node.Name] =
known.theories.get(name)
@@ -203,13 +206,13 @@
resources.thy_info.dependencies(root_theories)
}
- val syntax = thy_deps.syntax
+ val overall_syntax = thy_deps.overall_syntax
- val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
+ val theory_files = thy_deps.names.map(_.path)
val loaded_files =
if (inlined_files) {
if (Sessions.is_pure(info.name)) {
- (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
+ (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
}
else thy_deps.loaded_files
@@ -224,8 +227,10 @@
if (list_files)
progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
- if (check_keywords.nonEmpty)
- Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
+ if (check_keywords.nonEmpty) {
+ Check_Keywords.check_keywords(
+ progress, overall_syntax.keywords, check_keywords, theory_files)
+ }
val session_graph: Graph_Display.Graph =
{
@@ -251,18 +256,18 @@
val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
- (graph0 /: thy_deps.deps)(
- { case (g, dep) =>
- val a = node(dep.name)
+ (graph0 /: thy_deps.entries)(
+ { case (g, entry) =>
+ val a = node(entry.name)
val bs =
- dep.header.imports.map({ case (name, _) => node(name) }).
+ entry.header.imports.map({ case (name, _) => node(name) }).
filterNot(_ == a)
((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
}
val known =
Known.make(info.dir, List(imports_base),
- theories = thy_deps.deps.map(_.name),
+ theories = thy_deps.names,
loaded_files = loaded_files)
val sources =
@@ -276,8 +281,7 @@
global_theories = global_theories,
loaded_theories = thy_deps.loaded_theories,
known = known,
- keywords = thy_deps.keywords,
- syntax = syntax,
+ overall_syntax = overall_syntax,
sources = sources,
session_graph = session_graph,
errors = thy_deps.errors ::: sources_errors,
--- a/src/Pure/Thy/thy_header.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala Fri Sep 29 22:45:58 2017 +0200
@@ -138,7 +138,14 @@
(opt($$$(ABBREVS) ~! abbrevs) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
$$$(BEGIN) ^^
- { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
+ { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
+ val f = Symbol.decode _
+ Thy_Header((f(name), pos),
+ imports.map({ case (a, b) => (f(a), b) }),
+ keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
+ (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
+ abbrevs.map({ case (a, b) => (f(a), f(b)) }))
+ }
val heading =
(command(CHAPTER) |
@@ -197,20 +204,8 @@
}
}
-
sealed case class Thy_Header(
name: (String, Position.T),
imports: List[(String, Position.T)],
keywords: Thy_Header.Keywords,
abbrevs: Thy_Header.Abbrevs)
-{
- def decode_symbols: Thy_Header =
- {
- val f = Symbol.decode _
- Thy_Header((f(name._1), name._2),
- imports.map({ case (a, b) => (f(a), b) }),
- keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
- (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
- abbrevs.map({ case (a, b) => (f(a), f(b)) }))
- }
-}
--- a/src/Pure/Thy/thy_info.ML Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Sep 29 22:45:58 2017 +0200
@@ -160,7 +160,7 @@
in res :: map Exn.Exn exns end;
datatype task =
- Task of Path.T * string list * (theory list -> result) |
+ Task of string list * (theory list -> result) |
Finished of theory;
fun task_finished (Task _) = false
@@ -171,7 +171,7 @@
val schedule_seq =
String_Graph.schedule (fn deps => fn (_, task) =>
(case task of
- Task (_, parents, body) =>
+ Task (parents, body) =>
let
val result = body (task_parents deps parents);
val _ = Par_Exn.release_all (join_theory result);
@@ -185,7 +185,7 @@
val futures = tasks
|> String_Graph.schedule (fn deps => fn (name, task) =>
(case task of
- Task (_, parents, body) =>
+ Task (parents, body) =>
(singleton o Future.forks)
{name = "theory:" ^ name, group = NONE,
deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
@@ -335,19 +335,10 @@
|>> forall I
and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
let
- val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
- fun check_entry (Task (node_name', _, _)) =
- if op = (apply2 File.platform_path (node_name, node_name'))
- then ()
- else
- error ("Incoherent imports for theory " ^ quote theory_name ^
- Position.here require_pos ^ ":\n" ^
- " " ^ Path.print node_name ^ "\n" ^
- " " ^ Path.print node_name')
- | check_entry _ = ();
+ val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
in
(case try (String_Graph.get_node tasks) theory_name of
- SOME task => (check_entry task; (task_finished task, tasks))
+ SOME task => (task_finished task, tasks)
| NONE =>
let
val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
@@ -378,7 +369,7 @@
val load =
load_thy document symbols last_timing initiators update_time dep
text (theory_name, theory_pos) keywords;
- in Task (node_name, parents, load) end);
+ in Task (parents, load) end);
val tasks'' = new_entry theory_name parents task tasks';
in (all_current, tasks'') end)
--- a/src/Pure/Thy/thy_info.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_info.scala Fri Sep 29 22:45:58 2017 +0200
@@ -7,18 +7,6 @@
package isabelle
-object Thy_Info
-{
- /* dependencies */
-
- sealed case class Dep(
- name: Document.Node.Name,
- header: Document.Node.Header)
- {
- override def toString: String = name.toString
- }
-}
-
class Thy_Info(resources: Resources)
{
/* messages */
@@ -38,64 +26,50 @@
object Dependencies
{
- val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty)
+ val empty = new Dependencies(Nil, Set.empty)
}
final class Dependencies private(
- rev_deps: List[Thy_Info.Dep],
- val keywords: Thy_Header.Keywords,
- val abbrevs: Thy_Header.Abbrevs,
- val seen: Set[Document.Node.Name],
- val seen_theory: Multi_Map[String, (Document.Node.Name, Position.T)])
+ rev_entries: List[Document.Node.Entry],
+ val seen: Set[Document.Node.Name])
{
- def :: (dep: Thy_Info.Dep): Dependencies =
- new Dependencies(
- dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
- seen, seen_theory)
+ def :: (entry: Document.Node.Entry): Dependencies =
+ new Dependencies(entry :: rev_entries, seen)
- def + (thy: (Document.Node.Name, Position.T)): Dependencies =
- {
- val (name, _) = thy
- new Dependencies(rev_deps, keywords, abbrevs, seen + name, seen_theory + (name.theory -> thy))
- }
+ def + (name: Document.Node.Name): Dependencies =
+ new Dependencies(rev_entries, seen + name)
- def deps: List[Thy_Info.Dep] = rev_deps.reverse
+ def entries: List[Document.Node.Entry] = rev_entries.reverse
+ def names: List[Document.Node.Name] = entries.map(_.name)
+
+ def errors: List[String] = entries.flatMap(_.header.errors)
- def errors: List[String] =
- {
- val header_errors = deps.flatMap(dep => dep.header.errors)
- val import_errors =
- (for {
- (theory, imports) <- seen_theory.iterator_list
- if !resources.session_base.loaded_theories.isDefinedAt(theory)
- if imports.length > 1
- } yield {
- "Incoherent imports for theory " + quote(theory) + ":\n" +
- cat_lines(imports.map({ case (name, pos) =>
- " " + quote(name.node) + Position.here(pos) }))
- }).toList
- header_errors ::: import_errors
- }
+ lazy val loaded_theories: Graph[String, Outer_Syntax] =
+ (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
+ val name = entry.name.theory
+ val imports = entry.header.imports.map(p => p._1.theory)
- lazy val syntax: Outer_Syntax =
- resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
+ if (graph.defined(name))
+ error("Duplicate loaded theory entry " + quote(name))
- 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
- }
+ for (dep <- imports if !graph.defined(dep))
+ error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
+
+ val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
+ (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
+ })
def loaded_files: List[(String, List[Path])] =
{
- val names = deps.map(_.name)
names.map(_.theory) zip
- Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
+ Par_List.map((e: () => List[Path]) => e(),
+ names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
}
- override def toString: String = deps.toString
+ lazy val overall_syntax: Outer_Syntax =
+ Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
+
+ override def toString: String = entries.toString
}
private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
@@ -105,13 +79,13 @@
private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
thy: (Document.Node.Name, Position.T)): Dependencies =
{
- val (name, require_pos) = thy
+ val (name, pos) = thy
def message: String =
"The error(s) above occurred for theory " + quote(name.theory) +
- required_by(initiators) + Position.here(require_pos)
+ required_by(initiators) + Position.here(pos)
- val required1 = required + thy
+ val required1 = required + name
if (required.seen(name)) required
else if (resources.session_base.loaded_theory(name)) required1
else {
@@ -120,11 +94,12 @@
val header =
try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
- Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
+ Document.Node.Entry(name, header) ::
+ require_thys(name :: initiators, required1, header.imports)
}
catch {
case e: Throwable =>
- Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
+ Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
}
}
}
--- a/src/Pure/Thy/thy_syntax.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Fri Sep 29 22:45:58 2017 +0200
@@ -100,9 +100,10 @@
if (node.is_empty) None
else {
val header = node.header
- val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
- Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
- .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
+ val imports_syntax =
+ Outer_Syntax.merge(
+ header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
+ Some(imports_syntax + header)
}
nodes += (name -> node.update_syntax(syntax))
}
@@ -324,7 +325,9 @@
node_edits foreach {
case (name, edits) =>
val node = nodes(name)
- val syntax = node.syntax getOrElse resources.session_base.syntax
+ val syntax =
+ resources.session_base.node_syntax(nodes, name) getOrElse
+ Thy_Header.bootstrap_syntax
val commands = node.commands
val node1 =
--- a/src/Pure/Tools/build.ML Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Tools/build.ML Fri Sep 29 22:45:58 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 Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Tools/build.scala Fri Sep 29 22:45:58 2017 +0200
@@ -209,13 +209,13 @@
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),
(parent, (info.chapter, (name, (Path.current,
(info.theories,
- (base.global_theories.toList, (base.loaded_theories.toList,
+ (base.global_theories.toList, (base.loaded_theories.keys,
base.dest_known_theories)))))))))))))))
})
--- a/src/Pure/Tools/imports.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Tools/imports.scala Fri Sep 29 22:45:58 2017 +0200
@@ -105,7 +105,7 @@
(for {
(_, a) <- session_resources.session_base.known.theories.iterator
if session_resources.theory_qualifier(a) == info.theory_qualifier
- b <- deps.all_known.get_file(Path.explode(a.node).file)
+ b <- deps.all_known.get_file(a.path.file)
qualifier = session_resources.theory_qualifier(b)
if !declared_imports.contains(qualifier)
} yield qualifier).toSet
@@ -146,7 +146,7 @@
val s1 =
if (imports_base.loaded_theory(name)) name.theory
else {
- imports_base.known.get_file(Path.explode(name.node).file) match {
+ imports_base.known.get_file(name.path.file) match {
case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
name1.theory
case Some(name1) if Thy_Header.is_base_name(s) =>
@@ -170,7 +170,7 @@
(_, name) <- session_base.known.theories_local.toList
if session_resources.theory_qualifier(name) == info.theory_qualifier
(_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
- upd <- update_name(session_base.syntax.keywords, pos,
+ upd <- update_name(session_base.overall_syntax.keywords, pos,
standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
} yield upd
--- a/src/Tools/VSCode/src/build_vscode.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala Fri Sep 29 22:45:58 2017 +0200
@@ -20,7 +20,7 @@
def build_grammar(options: Options, progress: Progress = No_Progress)
{
val logic = Grammar.default_logic
- val keywords = Sessions.session_base(options, logic).syntax.keywords
+ val keywords = Sessions.session_base(options, logic).overall_syntax.keywords
val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
progress.echo(output_path.implode)
--- a/src/Tools/VSCode/src/grammar.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Fri Sep 29 22:45:58 2017 +0200
@@ -157,7 +157,7 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val keywords = Sessions.session_base(Options.init(), logic, dirs).syntax.keywords
+ val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords
val output_path = output getOrElse Path.explode(default_output(logic))
Output.writeln(output_path.implode)
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Sep 29 22:45:58 2017 +0200
@@ -216,7 +216,7 @@
(for ((_, model) <- st.models.iterator if model.is_theory)
yield (model.node_name, Position.none)).toList
- val thy_files = thy_info.dependencies(thys).deps.map(_.name)
+ val thy_files = thy_info.dependencies(thys).names
/* auxiliary files */
--- a/src/Tools/jEdit/src/document_model.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Sep 29 22:45:58 2017 +0200
@@ -253,7 +253,7 @@
val pending_nodes = for ((node_name, None) <- purged) yield node_name
(open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
}
- val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
+ val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet
for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
yield edit
--- a/src/Tools/jEdit/src/isabelle.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Sep 29 22:45:58 2017 +0200
@@ -50,7 +50,7 @@
def mode_syntax(mode: String): Option[Outer_Syntax] =
mode match {
- case "isabelle" => Some(PIDE.resources.session_base.syntax)
+ case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Sessions.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
--- a/src/Tools/jEdit/src/plugin.scala Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Sep 29 22:45:58 2017 +0200
@@ -126,7 +126,7 @@
val thys =
(for ((node_name, model) <- models.iterator if model.is_theory)
yield (node_name, Position.none)).toList
- val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
+ val thy_files = resources.thy_info.dependencies(thys).names
val aux_files =
if (options.bool("jedit_auto_resolve")) {