# HG changeset patch
# User wenzelm
# Date 1393685927 -3600
# Node ID ccf2d784be97139bc82fc61c63a5b92b8e1acf44
# Parent  44055f07cbd8831d4b4d9704209834dacaeac2c5
incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
tuned signature;

diff -r 44055f07cbd8 -r ccf2d784be97 src/Pure/PIDE/command.scala
--- 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 */
diff -r 44055f07cbd8 -r ccf2d784be97 src/Pure/PIDE/protocol.scala
--- 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
diff -r 44055f07cbd8 -r ccf2d784be97 src/Tools/jEdit/src/jedit_editor.scala
--- 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) } })
       }