further refinement of jEdit line range, avoiding lack of final \n;
authorwenzelm
Fri Oct 12 23:38:48 2012 +0200 (2012-10-12)
changeset 49843afddf4e26fac
parent 49842 a974f66062c8
child 49844 19ea3242ec37
further refinement of jEdit line range, avoiding lack of final \n;
src/Pure/General/pretty.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/General/pretty.scala	Fri Oct 12 22:53:20 2012 +0200
     1.2 +++ b/src/Pure/General/pretty.scala	Fri Oct 12 23:38:48 2012 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4    val FBreak = XML.Text("\n")
     1.5  
     1.6    val Separator = List(XML.elem(Isabelle_Markup.SEPARATOR, List(XML.Text(space))), FBreak)
     1.7 -  def separate(ts: List[XML.Tree]): XML.Body = ts.map(t => t :: Separator).flatten
     1.8 +  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
     1.9  
    1.10  
    1.11    /* formatted output */
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Oct 12 22:53:20 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 12 23:38:48 2012 +0200
     2.3 @@ -126,7 +126,7 @@
     2.4  
     2.5              for (i <- 0 until physical_lines.length) {
     2.6                if (physical_lines(i) != -1) {
     2.7 -                val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
     2.8 +                val line_range = Text.Range(start(i), end(i))
     2.9  
    2.10                  // gutter icons
    2.11                  rendering.gutter_message(line_range) match {
    2.12 @@ -201,7 +201,7 @@
    2.13                            line <- 0 until text_area.getVisibleLines
    2.14                            start = text_area.getScreenLineStartOffset(line) if start >= 0
    2.15                            end = text_area.getScreenLineEndOffset(line) if end >= 0
    2.16 -                          range = JEdit_Lib.proper_line_range(buffer, start, end)
    2.17 +                          range = Text.Range(start, end)
    2.18                            line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    2.19                            if line_cmds.exists(changed.commands)
    2.20                          } text_area.invalidateScreenLineRange(line, line)
     3.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 12 22:53:20 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Oct 12 23:38:48 2012 +0200
     3.3 @@ -109,13 +109,6 @@
     3.4      }
     3.5  
     3.6  
     3.7 -  /* proper line range */
     3.8 -
     3.9 -  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
    3.10 -  def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range =
    3.11 -    Text.Range(start, end min buffer.getLength)
    3.12 -
    3.13 -
    3.14    /* visible text range */
    3.15  
    3.16    def visible_range(text_area: TextArea): Option[Text.Range] =
    3.17 @@ -125,7 +118,8 @@
    3.18      if (n > 0) {
    3.19        val start = text_area.getScreenLineStartOffset(0)
    3.20        val raw_end = text_area.getScreenLineEndOffset(n - 1)
    3.21 -      Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength))
    3.22 +      val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
    3.23 +      Some(Text.Range(start, end))
    3.24      }
    3.25      else None
    3.26    }
    3.27 @@ -154,7 +148,7 @@
    3.28  
    3.29    class Gfx_Range(val x: Int, val y: Int, val length: Int)
    3.30  
    3.31 -  // NB: jEdit already normalizes \r\n and \r to \n
    3.32 +  // NB: jEdit always normalizes \r\n and \r to \n
    3.33    // NB: last line lacks \n
    3.34    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    3.35    {
    3.36 @@ -165,7 +159,7 @@
    3.37      val end = buffer.getLength
    3.38      val stop = range.stop
    3.39      val (q, r) =
    3.40 -      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
    3.41 +      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))
    3.42        else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
    3.43          (text_area.offsetToXY(stop - 1), char_width(text_area))
    3.44        else (text_area.offsetToXY(stop), 0)
     4.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 12 22:53:20 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Oct 12 23:38:48 2012 +0200
     4.3 @@ -230,7 +230,7 @@
     4.4  
     4.5          for (i <- 0 until physical_lines.length) {
     4.6            if (physical_lines(i) != -1) {
     4.7 -            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
     4.8 +            val line_range = Text.Range(start(i), end(i))
     4.9  
    4.10              // line background color
    4.11              for { (color, separator) <- rendering.line_background(line_range) }
    4.12 @@ -415,7 +415,7 @@
    4.13        robust_rendering { rendering =>
    4.14          for (i <- 0 until physical_lines.length) {
    4.15            if (physical_lines(i) != -1) {
    4.16 -            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
    4.17 +            val line_range = Text.Range(start(i), end(i))
    4.18  
    4.19              // foreground color
    4.20              for {