incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
authorwenzelm
Sat Mar 01 15:58:47 2014 +0100 (2014-03-01)
changeset 55822ccf2d784be97
parent 55821 44055f07cbd8
child 55823 0331b6d2ab0c
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Mar 01 13:05:46 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Mar 01 15:58:47 2014 +0100
     1.3 @@ -156,14 +156,11 @@
     1.4                  if id == command.id || id == alt_id =>
     1.5                    command.chunks.get(file_name) match {
     1.6                      case Some(chunk) =>
     1.7 -                      chunk.decode(raw_range).try_restrict(chunk.range) match {
     1.8 +                      chunk.incorporate(raw_range) match {
     1.9                          case Some(range) =>
    1.10 -                          if (!range.is_singularity) {
    1.11 -                            val props = Position.purge(atts)
    1.12 -                            val info = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.13 -                            state.add_markup(false, file_name, info)
    1.14 -                          }
    1.15 -                          else state
    1.16 +                          val props = Position.purge(atts)
    1.17 +                          val info = Text.Info(range, XML.Elem(Markup(name, props), args))
    1.18 +                          state.add_markup(false, file_name, info)
    1.19                          case None => bad(); state
    1.20                        }
    1.21                      case None => bad(); state
    1.22 @@ -219,7 +216,17 @@
    1.23      def file_name: String
    1.24      def length: Int
    1.25      def range: Text.Range
    1.26 -    def decode(r: Text.Range): Text.Range
    1.27 +    def decode(raw_range: Text.Range): Text.Range
    1.28 +
    1.29 +    def incorporate(raw_range: Text.Range): Option[Text.Range] =
    1.30 +    {
    1.31 +      def inc(r: Text.Range): Option[Text.Range] =
    1.32 +        range.try_restrict(decode(r)) match {
    1.33 +          case Some(r1) if !r1.is_singularity => Some(r1)
    1.34 +          case _ => None
    1.35 +        }
    1.36 +     inc(raw_range) orElse inc(raw_range - 1)
    1.37 +    }
    1.38    }
    1.39  
    1.40    class File(val file_name: String, text: CharSequence) extends Chunk
    1.41 @@ -227,7 +234,7 @@
    1.42      val length = text.length
    1.43      val range = Text.Range(0, length)
    1.44      private val symbol_index = Symbol.Index(text)
    1.45 -    def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
    1.46 +    def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
    1.47  
    1.48      override def toString: String = "Command.File(" + file_name + ")"
    1.49    }
    1.50 @@ -367,8 +374,8 @@
    1.51    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.52  
    1.53    private lazy val symbol_index = Symbol.Index(source)
    1.54 -  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
    1.55 -  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
    1.56 +  def decode(raw_offset: Text.Offset): Text.Offset = symbol_index.decode(raw_offset)
    1.57 +  def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
    1.58  
    1.59  
    1.60    /* accumulated results */
     2.1 --- a/src/Pure/PIDE/protocol.scala	Sat Mar 01 13:05:46 2014 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Mar 01 15:58:47 2014 +0100
     2.3 @@ -289,8 +289,8 @@
     2.4        props match {
     2.5          case Position.Reported(id, file_name, raw_range)
     2.6          if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
     2.7 -          chunk.decode(raw_range).try_restrict(chunk.range) match {
     2.8 -            case Some(range) if !range.is_singularity => set + range
     2.9 +          chunk.incorporate(raw_range) match {
    2.10 +            case Some(range) => set + range
    2.11              case _ => set
    2.12            }
    2.13          case _ => set
     3.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 01 13:05:46 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Mar 01 15:58:47 2014 +0100
     3.3 @@ -156,7 +156,7 @@
     3.4    override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     3.5      new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
     3.6  
     3.7 -  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
     3.8 +  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
     3.9      : Option[Hyperlink] =
    3.10    {
    3.11      if (snapshot.is_outdated) None
    3.12 @@ -167,8 +167,8 @@
    3.13            val file_name = command.node_name.node
    3.14            val sources =
    3.15              node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    3.16 -              (if (offset == 0) Iterator.empty
    3.17 -               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
    3.18 +              (if (raw_offset == 0) Iterator.empty
    3.19 +               else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
    3.20            val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    3.21            Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
    3.22        }