# HG changeset patch
# User wenzelm
# Date 1330881345 -3600
# Node ID 3d55ef732cd7362b96f4f17e9e3e6187cb71640e
# Parent  03a2dc9e06241f867fd51ddf90c5478a80de897e
clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";

diff -r 03a2dc9e0624 -r 3d55ef732cd7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Mar 04 16:02:14 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Mar 04 18:15:45 2012 +0100
@@ -164,7 +164,6 @@
       tree match {
         case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
         if include_pos(name) && id == command.id =>
-          // FIXME handle message range outside command range (!??!)
           val range = command.decode(raw_range).restrict(command.range)
           body.foldLeft(if (range.is_singularity) set else set + range)(positions)
         case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
diff -r 03a2dc9e0624 -r 3d55ef732cd7 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sun Mar 04 16:02:14 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sun Mar 04 18:15:45 2012 +0100
@@ -92,13 +92,9 @@
 
   /* visible text range */
 
-  // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
-  // NB: jEdit already normalizes \r\n and \r to \n
+  // FIXME remove!?
   def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
-  {
-    val stop = if (start < end) end - 1 else end min model.buffer.getLength
-    Text.Range(start, stop)
-  }
+    Text.Range(start, end min model.buffer.getLength)
 
   def visible_range(): Option[Text.Range] =
   {
diff -r 03a2dc9e0624 -r 3d55ef732cd7 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Sun Mar 04 16:02:14 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Sun Mar 04 18:15:45 2012 +0100
@@ -28,14 +28,32 @@
 
   /* graphics range */
 
+  private def char_width(): Int =
+  {
+    val painter = text_area.getPainter
+    val font = painter.getFont
+    val font_context = painter.getFontRenderContext
+    font.getStringBounds(" ", font_context).getWidth.round.toInt
+  }
+
   private class Gfx_Range(val x: Int, val y: Int, val length: Int)
 
+  // NB: jEdit already normalizes \r\n and \r to \n
+  // NB: last line lacks \n
   private def gfx_range(range: Text.Range): Option[Gfx_Range] =
   {
     val p = text_area.offsetToXY(range.start)
-    val q = text_area.offsetToXY(range.stop)
-    if (p != null && q != null && p.x < q.x && p.y == q.y)
-      Some(new Gfx_Range(p.x, p.y, q.x - p.x))
+
+    val end = buffer.getLength
+    val stop = range.stop
+    val (q, r) =
+      if (stop >= end) (text_area.offsetToXY(end), char_width())
+      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
+        (text_area.offsetToXY(stop - 1), char_width())
+      else (text_area.offsetToXY(stop), 0)
+
+    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
+      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
     else None
   }
 
@@ -143,14 +161,6 @@
 
   /* text */
 
-  private def char_width(): Int =
-  {
-    val painter = text_area.getPainter
-    val font = painter.getFont
-    val font_context = painter.getFontRenderContext
-    font.getStringBounds(" ", font_context).getWidth.round.toInt
-  }
-
   private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
   {
     val painter = text_area.getPainter