# HG changeset patch # User wenzelm # Date 1606852023 -3600 # Node ID 85bcdd05c6d0168d690f5aa023bb78b056e3f9b0 # Parent 5dc7165e8a26653b55c9e2d03a9e185936432910 clarified signature --- more positions; diff -r 5dc7165e8a26 -r 85bcdd05c6d0 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Tue Dec 01 16:07:19 2020 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Tue Dec 01 20:47:03 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() diff -r 5dc7165e8a26 -r 85bcdd05c6d0 src/Pure/PIDE/command_span.scala --- a/src/Pure/PIDE/command_span.scala Tue Dec 01 16:07:19 2020 +0100 +++ b/src/Pure/PIDE/command_span.scala Tue Dec 01 20:47:03 2020 +0100 @@ -46,13 +46,13 @@ sealed abstract class Kind { override def toString: String = this match { - case Command_Span(name, _) => proper_string(name) getOrElse "" + case Command_Span(name, _, _) => proper_string(name) getOrElse "" case Ignored_Span => "" case Malformed_Span => "" case Theory_Span => "" } } - 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 {