--- a/src/Pure/PIDE/command.scala Sun Nov 29 15:58:43 2020 +0100
+++ b/src/Pure/PIDE/command.scala Sun Nov 29 16:11:52 2020 +0100
@@ -419,10 +419,10 @@
val imports_pos = header.imports_pos
val raw_imports =
try {
- val read_imports = Thy_Header.read(node_name, reader).imports
+ val read_imports = Thy_Header.read(node_name, reader).imports.map(_._1)
if (imports_pos.length == read_imports.length) read_imports else error("")
}
- catch { case _: Throwable => List.fill(imports_pos.length)("") }
+ catch { case _: Throwable => List.fill(header.imports.length)("") }
val errors =
for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
--- a/src/Pure/PIDE/resources.scala Sun Nov 29 15:58:43 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Sun Nov 29 16:11:52 2020 +0100
@@ -220,15 +220,14 @@
if (node_name.is_theory && reader.source.length > 0) {
try {
val header = Thy_Header.read(node_name, reader, command = command, strict = strict)
-
- val imports_pos =
- header.imports_pos.map({ case (s, pos) =>
+ val imports =
+ header.imports.map({ case (s, pos) =>
val name = import_name(node_name, s)
if (Sessions.exclude_theory(name.theory_base_name))
error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
(name, pos)
})
- Document.Node.Header(imports_pos, header.keywords, header.abbrevs)
+ Document.Node.Header(imports, header.keywords, header.abbrevs)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
}
--- a/src/Pure/Thy/thy_header.scala Sun Nov 29 15:58:43 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala Sun Nov 29 16:11:52 2020 +0100
@@ -162,7 +162,7 @@
{ case None => Nil case Some(_ ~ xs) => xs }) ~
(opt($$$(ABBREVS) ~! abbrevs) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
- $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a, b, c, d).map(Symbol.decode) }
+ $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a._1, a._2, b, c, d).map(Symbol.decode) }
val heading =
(command(CHAPTER) |
@@ -230,18 +230,15 @@
}
sealed case class Thy_Header(
- name_pos: (String, Position.T),
- imports_pos: List[(String, Position.T)],
+ name: String,
+ pos: Position.T,
+ imports: List[(String, Position.T)],
keywords: Thy_Header.Keywords,
abbrevs: Thy_Header.Abbrevs)
{
- def name: String = name_pos._1
- def pos: Position.T = name_pos._2
- def imports: List[String] = imports_pos.map(_._1)
-
def map(f: String => String): Thy_Header =
- Thy_Header((f(name), pos),
- imports_pos.map({ case (a, b) => (f(a), b) }),
+ Thy_Header(f(name), pos,
+ imports.map({ case (a, b) => (f(a), b) }),
keywords.map({ case (a, spec) => (f(a), spec.map(f)) }),
abbrevs.map({ case (a, b) => (f(a), f(b)) }))