maintain Command_Range position as in ML;
authorwenzelm
Tue Aug 12 14:15:58 2014 +0200 (2014-08-12)
changeset 57910a50837b637dc
parent 57909 0fb331032f02
child 57911 dcb758188aa6
maintain Command_Range position as in ML;
src/Pure/General/position.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
     1.1 --- a/src/Pure/General/position.scala	Tue Aug 12 13:18:17 2014 +0200
     1.2 +++ b/src/Pure/General/position.scala	Tue Aug 12 14:15:58 2014 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5    object Range
     1.6    {
     1.7 -    def apply(range: Symbol.Range): T = Offset(range.start) ::: Offset(range.stop)
     1.8 +    def apply(range: Symbol.Range): T = Offset(range.start) ::: End_Offset(range.stop)
     1.9      def unapply(pos: T): Option[Symbol.Range] =
    1.10        (pos, pos) match {
    1.11          case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 13:18:17 2014 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 14:15:58 2014 +0200
     2.3 @@ -161,8 +161,11 @@
     2.4      def ship(span: List[Token])
     2.5      {
     2.6        val kind =
     2.7 -        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
     2.8 -          Command_Span.Command_Span(span.head.source)
     2.9 +        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error)) {
    2.10 +          val name = span.head.source
    2.11 +          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length))
    2.12 +          Command_Span.Command_Span(name, pos)
    2.13 +        }
    2.14          else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    2.15          else Command_Span.Malformed_Span
    2.16        result += Command_Span.Span(kind, span)
     3.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 12 13:18:17 2014 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 12 14:15:58 2014 +0200
     3.3 @@ -317,13 +317,19 @@
     3.4      val init_results: Command.Results,
     3.5      val init_markup: Markup_Tree)
     3.6  {
     3.7 -  /* name and classification */
     3.8 +  /* name */
     3.9  
    3.10    def name: String =
    3.11 -    span.kind match { case Command_Span.Command_Span(name) => name case _ => "" }
    3.12 +    span.kind match { case Command_Span.Command_Span(name, _) => name case _ => "" }
    3.13 +
    3.14 +  def position: Position.T =
    3.15 +    span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
    3.16  
    3.17    override def toString = id + "/" + span.kind.toString
    3.18  
    3.19 +
    3.20 +  /* classification */
    3.21 +
    3.22    def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
    3.23    def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
    3.24  
     4.1 --- a/src/Pure/PIDE/command_span.scala	Tue Aug 12 13:18:17 2014 +0200
     4.2 +++ b/src/Pure/PIDE/command_span.scala	Tue Aug 12 14:15:58 2014 +0200
     4.3 @@ -15,12 +15,12 @@
     4.4    sealed abstract class Kind {
     4.5      override def toString: String =
     4.6        this match {
     4.7 -        case Command_Span(name) => if (name != "") name else "<command>"
     4.8 +        case Command_Span(name, _) => if (name != "") name else "<command>"
     4.9          case Ignored_Span => "<ignored>"
    4.10          case Malformed_Span => "<malformed>"
    4.11        }
    4.12    }
    4.13 -  case class Command_Span(name: String) extends Kind
    4.14 +  case class Command_Span(name: String, pos: Position.T) extends Kind
    4.15    case object Ignored_Span extends Kind
    4.16    case object Malformed_Span extends Kind
    4.17  
    4.18 @@ -70,7 +70,7 @@
    4.19  
    4.20    def span_files(syntax: Prover.Syntax, span: Span): List[String] =
    4.21      span.kind match {
    4.22 -      case Command_Span(name) =>
    4.23 +      case Command_Span(name, _) =>
    4.24          syntax.load_command(name) match {
    4.25            case Some(exts) =>
    4.26              find_file(span.content) match {