incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
tuned signature;
--- a/src/Pure/PIDE/command.scala Sat Mar 01 13:05:46 2014 +0100
+++ b/src/Pure/PIDE/command.scala Sat Mar 01 15:58:47 2014 +0100
@@ -156,14 +156,11 @@
if id == command.id || id == alt_id =>
command.chunks.get(file_name) match {
case Some(chunk) =>
- chunk.decode(raw_range).try_restrict(chunk.range) match {
+ chunk.incorporate(raw_range) match {
case Some(range) =>
- if (!range.is_singularity) {
- val props = Position.purge(atts)
- val info = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(false, file_name, info)
- }
- else state
+ val props = Position.purge(atts)
+ val info = Text.Info(range, XML.Elem(Markup(name, props), args))
+ state.add_markup(false, file_name, info)
case None => bad(); state
}
case None => bad(); state
@@ -219,7 +216,17 @@
def file_name: String
def length: Int
def range: Text.Range
- def decode(r: Text.Range): Text.Range
+ def decode(raw_range: Text.Range): Text.Range
+
+ def incorporate(raw_range: Text.Range): Option[Text.Range] =
+ {
+ def inc(r: Text.Range): Option[Text.Range] =
+ range.try_restrict(decode(r)) match {
+ case Some(r1) if !r1.is_singularity => Some(r1)
+ case _ => None
+ }
+ inc(raw_range) orElse inc(raw_range - 1)
+ }
}
class File(val file_name: String, text: CharSequence) extends Chunk
@@ -227,7 +234,7 @@
val length = text.length
val range = Text.Range(0, length)
private val symbol_index = Symbol.Index(text)
- def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+ def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
override def toString: String = "Command.File(" + file_name + ")"
}
@@ -367,8 +374,8 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
private lazy val symbol_index = Symbol.Index(source)
- def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
- def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+ def decode(raw_offset: Text.Offset): Text.Offset = symbol_index.decode(raw_offset)
+ def decode(raw_range: Text.Range): Text.Range = symbol_index.decode(raw_range)
/* accumulated results */
--- a/src/Pure/PIDE/protocol.scala Sat Mar 01 13:05:46 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Sat Mar 01 15:58:47 2014 +0100
@@ -289,8 +289,8 @@
props match {
case Position.Reported(id, file_name, raw_range)
if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
- chunk.decode(raw_range).try_restrict(chunk.range) match {
- case Some(range) if !range.is_singularity => set + range
+ chunk.incorporate(raw_range) match {
+ case Some(range) => set + range
case _ => set
}
case _ => set
--- a/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 01 13:05:46 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 01 15:58:47 2014 +0100
@@ -156,7 +156,7 @@
override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
- override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
+ override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
: Option[Hyperlink] =
{
if (snapshot.is_outdated) None
@@ -167,8 +167,8 @@
val file_name = command.node_name.node
val sources =
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
- (if (offset == 0) Iterator.empty
- else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
+ (if (raw_offset == 0) Iterator.empty
+ else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
}