# HG changeset patch
# User wenzelm
# Date 1350077928 -7200
# Node ID afddf4e26facfb2c9c134138c300595b42e325e0
# Parent  a974f66062c87aeb6d9028a78800b45b9fea51f3
further refinement of jEdit line range, avoiding lack of final \n;

diff -r a974f66062c8 -r afddf4e26fac src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri Oct 12 22:53:20 2012 +0200
+++ b/src/Pure/General/pretty.scala	Fri Oct 12 23:38:48 2012 +0200
@@ -60,7 +60,7 @@
   val FBreak = XML.Text("\n")
 
   val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak)
-  def separate(ts: List[XML.Tree]): XML.Body = ts.map(t => t :: Separator).flatten
+  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
 
 
   /* formatted output */
diff -r a974f66062c8 -r afddf4e26fac src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Oct 12 22:53:20 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 12 23:38:48 2012 +0200
@@ -126,7 +126,7 @@
 
             for (i <- 0 until physical_lines.length) {
               if (physical_lines(i) != -1) {
-                val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+                val line_range = Text.Range(start(i), end(i))
 
                 // gutter icons
                 rendering.gutter_message(line_range) match {
@@ -201,7 +201,7 @@
                           line <- 0 until text_area.getVisibleLines
                           start = text_area.getScreenLineStartOffset(line) if start >= 0
                           end = text_area.getScreenLineEndOffset(line) if end >= 0
-                          range = JEdit_Lib.proper_line_range(buffer, start, end)
+                          range = Text.Range(start, end)
                           line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
                           if line_cmds.exists(changed.commands)
                         } text_area.invalidateScreenLineRange(line, line)
diff -r a974f66062c8 -r afddf4e26fac src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 12 22:53:20 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 12 23:38:48 2012 +0200
@@ -109,13 +109,6 @@
     }
 
 
-  /* proper line range */
-
-  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
-  def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range =
-    Text.Range(start, end min buffer.getLength)
-
-
   /* visible text range */
 
   def visible_range(text_area: TextArea): Option[Text.Range] =
@@ -125,7 +118,8 @@
     if (n > 0) {
       val start = text_area.getScreenLineStartOffset(0)
       val raw_end = text_area.getScreenLineEndOffset(n - 1)
-      Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength))
+      val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
+      Some(Text.Range(start, end))
     }
     else None
   }
@@ -154,7 +148,7 @@
 
   class Gfx_Range(val x: Int, val y: Int, val length: Int)
 
-  // NB: jEdit already normalizes \r\n and \r to \n
+  // NB: jEdit always normalizes \r\n and \r to \n
   // NB: last line lacks \n
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {
@@ -165,7 +159,7 @@
     val end = buffer.getLength
     val stop = range.stop
     val (q, r) =
-      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
+      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
       else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
         (text_area.offsetToXY(stop - 1), char_width(text_area))
       else (text_area.offsetToXY(stop), 0)
diff -r a974f66062c8 -r afddf4e26fac src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 12 22:53:20 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 12 23:38:48 2012 +0200
@@ -230,7 +230,7 @@
 
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
-            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+            val line_range = Text.Range(start(i), end(i))
 
             // line background color
             for { (color, separator) <- rendering.line_background(line_range) }
@@ -415,7 +415,7 @@
       robust_rendering { rendering =>
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
-            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+            val line_range = Text.Range(start(i), end(i))
 
             // foreground color
             for {