# HG changeset patch
# User wenzelm
# Date 1407845758 -7200
# Node ID a50837b637dcbbdf9871f8d4c038b0c2dc66bd55
# Parent  0fb331032f02d67b7df49a219e2f08ae18b157cf
maintain Command_Range position as in ML;

diff -r 0fb331032f02 -r a50837b637dc src/Pure/General/position.scala
--- 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))
diff -r 0fb331032f02 -r a50837b637dc src/Pure/Isar/outer_syntax.scala
--- 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)
diff -r 0fb331032f02 -r a50837b637dc src/Pure/PIDE/command.scala
--- 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
 
diff -r 0fb331032f02 -r a50837b637dc src/Pure/PIDE/command_span.scala
--- 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 {