--- a/src/Pure/General/position.scala Tue Aug 12 13:18:17 2014 +0200
+++ b/src/Pure/General/position.scala Tue Aug 12 14:15:58 2014 +0200
@@ -54,7 +54,7 @@
object Range
{
- def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop)
+ def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
def unapply(pos: T): Option[Symbol.Range] =
(pos, pos) match {
case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 12 13:18:17 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 12 14:15:58 2014 +0200
@@ -161,8 +161,11 @@
def ship(span: List[Token])
{
val kind =
- if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
- Command_Span.Command_Span(span.head.source)
+ if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
+ val name = span.head.source
+ val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length))
+ Command_Span.Command_Span(name, pos)
+ }
else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
else Command_Span.Malformed_Span
result += Command_Span.Span(kind, span)
--- a/src/Pure/PIDE/command.scala Tue Aug 12 13:18:17 2014 +0200
+++ b/src/Pure/PIDE/command.scala Tue Aug 12 14:15:58 2014 +0200
@@ -317,13 +317,19 @@
val init_results: Command.Results,
val init_markup: Markup_Tree)
{
- /* name and classification */
+ /* name */
def name: String =
- span.kind match { case Command_Span.Command_Span(name) => name case _ => "" }
+ span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
+
+ def position: Position.T =
+ span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
override def toString = id + "/" + span.kind.toString
+
+ /* classification */
+
def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
--- a/src/Pure/PIDE/command_span.scala Tue Aug 12 13:18:17 2014 +0200
+++ b/src/Pure/PIDE/command_span.scala Tue Aug 12 14:15:58 2014 +0200
@@ -15,12 +15,12 @@
sealed abstract class Kind {
override def toString: String =
this match {
- case Command_Span(name) => if (name != "") name else "<command>"
+ case Command_Span(name, _) => if (name != "") name else "<command>"
case Ignored_Span => "<ignored>"
case Malformed_Span => "<malformed>"
}
}
- case class Command_Span(name: String) extends Kind
+ case class Command_Span(name: String, pos: Position.T) extends Kind
case object Ignored_Span extends Kind
case object Malformed_Span extends Kind
@@ -70,7 +70,7 @@
def span_files(syntax: Prover.Syntax, span: Span): List[String] =
span.kind match {
- case Command_Span(name) =>
+ case Command_Span(name, _) =>
syntax.load_command(name) match {
case Some(exts) =>
find_file(span.content) match {