--- a/src/Pure/Isar/outer_syntax.scala Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Tue Dec 01 20:47:19 2020 +0100
@@ -165,25 +165,29 @@
val result = new mutable.ListBuffer[Command_Span.Span]
val content = new mutable.ListBuffer[Token]
val ignored = new mutable.ListBuffer[Token]
+ var start = 0
- def ship(span: List[Token])
+ def ship(content: List[Token])
{
val kind =
- if (span.forall(_.is_ignored)) Command_Span.Ignored_Span
- else if (span.exists(_.is_error)) Command_Span.Malformed_Span
+ if (content.forall(_.is_ignored)) Command_Span.Ignored_Span
+ else if (content.exists(_.is_error)) Command_Span.Malformed_Span
else
- span.find(_.is_command) match {
+ content.find(_.is_command) match {
case None => Command_Span.Malformed_Span
case Some(cmd) =>
val name = cmd.source
val offset =
- (0 /: span.takeWhile(_ != cmd)) {
+ (0 /: content.takeWhile(_ != cmd)) {
case (i, tok) => i + Symbol.length(tok.source) }
val end_offset = offset + Symbol.length(name)
- val pos = Position.Range(Text.Range(offset, end_offset) + 1)
- Command_Span.Command_Span(name, pos)
+ val range = Text.Range(offset, end_offset) + 1
+ val pos = Position.Range(range)
+ val abs_pos = Position.Range(range + start)
+ Command_Span.Command_Span(name, pos, abs_pos)
}
- result += Command_Span.Span(kind, span)
+ for (tok <- content) start += Symbol.length(tok.source)
+ result += Command_Span.Span(kind, content)
}
def flush()
--- a/src/Pure/PIDE/command_span.scala Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala Tue Dec 01 20:47:19 2020 +0100
@@ -46,13 +46,13 @@
sealed abstract class Kind {
override def toString: String =
this match {
- case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
+ case Command_Span(name, _, _) => proper_string(name) getOrElse "<command>"
case Ignored_Span => "<ignored>"
case Malformed_Span => "<malformed>"
case Theory_Span => "<theory>"
}
}
- case class Command_Span(name: String, pos: Position.T) extends Kind
+ case class Command_Span(name: String, pos: Position.T, abs_pos: Position.T) extends Kind
case object Ignored_Span extends Kind
case object Malformed_Span extends Kind
case object Theory_Span extends Kind
@@ -65,10 +65,13 @@
def is_theory: Boolean = kind == Theory_Span
def name: String =
- kind match { case Command_Span(name, _) => name case _ => "" }
+ kind match { case k: Command_Span => k.name case _ => "" }
def position: Position.T =
- kind match { case Command_Span(_, pos) => pos case _ => Position.none }
+ kind match { case k: Command_Span => k.pos case _ => Position.none }
+
+ def absolute_position: Position.T =
+ kind match { case k: Command_Span => k.abs_pos case _ => Position.none }
def keyword_pos(start: Token.Pos): Token.Pos =
kind match {
--- a/src/Pure/PIDE/headless.scala Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Tue Dec 01 20:47:19 2020 +0100
@@ -256,7 +256,7 @@
val dep_theories = dependencies.theories
val dep_theories_set = dep_theories.toSet
val dep_files =
- dependencies.loaded_files(false).flatMap(_._2).
+ dependencies.loaded_files.flatMap(_._2).
map(path => Document.Node.Name(resources.append("", path)))
val use_theories_state =
--- a/src/Pure/PIDE/resources.scala Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Tue Dec 01 20:47:19 2020 +0100
@@ -398,20 +398,17 @@
graph2.map_node(name, _ => syntax)
})
- def loaded_files(pure: Boolean): List[(String, List[Path])] =
+ def loaded_files: List[(String, List[Path])] =
{
- val loaded_files =
- theories.map(_.theory) zip
- Par_List.map((e: () => List[Path]) => e(),
- theories.map(name =>
- resources.loaded_files(loaded_theories.get_node(name.theory), name)))
-
- if (pure) {
- val pure_files = resources.pure_files(overall_syntax)
- loaded_files.map({ case (name, files) =>
- (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
- }
- else loaded_files
+ theories.zip(
+ Par_List.map((e: () => List[Path]) => e(),
+ theories.map(name =>
+ resources.loaded_files(loaded_theories.get_node(name.theory), name))))
+ .map({ case (name, files) =>
+ val files1 =
+ if (name.theory == Thy_Header.PURE) resources.pure_files(overall_syntax) ::: files
+ else files
+ (name.theory, files1) })
}
def imported_files: List[Path] =
--- a/src/Pure/Thy/sessions.scala Tue Dec 01 15:29:54 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Dec 01 20:47:19 2020 +0100
@@ -173,10 +173,7 @@
val theory_files = dependencies.theories.map(_.path)
val (loaded_files, loaded_files_errors) =
- try {
- if (inlined_files) (dependencies.loaded_files(Sessions.is_pure(info.name)), Nil)
- else (Nil, Nil)
- }
+ try { if (inlined_files) (dependencies.loaded_files, Nil) else (Nil, Nil) }
catch { case ERROR(msg) => (Nil, List(msg)) }
val session_files =