merged

--- a/src/Pure/General/symbol.scala	Mon Jun 28 09:48:36 2010 +0200
+++ b/src/Pure/General/symbol.scala	Mon Jun 28 10:39:39 2010 +0200
@@ -31,7 +31,9 @@
   /* Symbol regexps */
 
   private val plain = new Regex("""(?xs)
-    [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+      [^\r\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
+
+  private val newline = new Regex("""(?xs) \r\n | \r """)
 
   private val symbol = new Regex("""(?xs)
       \\ < (?:
@@ -39,17 +41,17 @@
       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
 
   // FIXME cover bad surrogates!?
-  // FIXME check wrt. ML version
+  // FIXME check wrt. Isabelle/ML version
   private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
     """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
 
   // total pattern
-  val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
+  val regex = new Regex(plain + "|" + newline + "|" + symbol + "|" + bad_symbol + "| .")
 
 
   /* basic matching */
 
-  def is_plain(c: Char): Boolean = !(c == '\\' || '\ud800' <= c && c <= '\udfff')
+  def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
 
   def is_wellformed(s: CharSequence): Boolean =
     s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jun 28 09:48:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jun 28 10:39:39 2010 +0200
@@ -56,6 +56,19 @@
 
 class Document_Model(val session: Session, val buffer: Buffer)
 {
+  /* visible line end */
+
+  // simplify slightly odd result of TextArea.getLineEndOffset
+  // NB: jEdit already normalizes \r\n and \r to \n
+  def visible_line_end(start: Int, end: Int): Int =
+  {
+    val end1 = end - 1
+    if (start <= end1 && end1 < buffer.getLength &&
+        buffer.getSegment(end1, 1).charAt(0) == '\n') end1
+    else end
+  }
+
+
   /* history */
 
   private val document_0 = session.begin_document(buffer.getName)
@@ -127,9 +140,11 @@
 
   /* activation */
 
+  private val token_marker = new Isabelle_Token_Marker(this)
+
   def activate()
   {
-    buffer.setTokenMarker(new Isabelle_Token_Marker(this))
+    buffer.setTokenMarker(token_marker)
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
 
@@ -137,6 +152,11 @@
     edits_delay()
   }
 
+  def refresh()
+  {
+    buffer.setTokenMarker(token_marker)
+  }
+
   def deactivate()
   {
     buffer.setTokenMarker(buffer.getMode.getTokenMarker)

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jun 28 09:48:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jun 28 10:39:39 2010 +0200
@@ -129,16 +129,20 @@
       val document = model.recent_document()
       def from_current(pos: Int) = model.from_current(document, pos)
       def to_current(pos: Int) = model.to_current(document, pos)
-      val metrics = text_area.getPainter.getFontMetrics
+
+      val line_end = model.visible_line_end(start, end)
+      val line_height = text_area.getPainter.getFontMetrics.getHeight
+
       val saved_color = gfx.getColor
       try {
         for ((command, command_start) <-
-          document.command_range(from_current(start), from_current(end)) if !command.is_ignored)
+          document.command_range(from_current(start), from_current(line_end)) if !command.is_ignored)
         {
-          val begin = start max to_current(command_start)
-          val finish = (end - 1) min to_current(command_start + command.length)
-          encolor(gfx, y, metrics.getHeight, begin, finish,
-            Document_View.choose_color(document, command), true)
+          val p = text_area.offsetToXY(start max to_current(command_start))
+          val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
+          assert(p.y == q.y)
+          gfx.setColor(Document_View.choose_color(document, command))
+          gfx.fillRect(p.x, y, q.x - p.x, line_height)
         }
       }
       finally { gfx.setColor(saved_color) }
@@ -205,26 +209,6 @@
     text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
       text_area.getLastPhysicalLine)
 
-  private def encolor(gfx: Graphics2D,
-    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
-  {
-    val start = text_area.offsetToXY(begin)
-    val stop =
-      if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
-      else {
-        val p = text_area.offsetToXY(finish - 1)
-        val metrics = text_area.getPainter.getFontMetrics
-        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
-        p
-      }
-
-    if (start != null && stop != null) {
-      gfx.setColor(color)
-      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
-      else gfx.drawRect(start.x, y, stop.x - start.x, height)
-    }
-  }
-
 
   /* overview of command status left of scrollbar */
 

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Mon Jun 28 09:48:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Mon Jun 28 10:39:39 2010 +0200
@@ -20,7 +20,7 @@
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
+import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
@@ -203,6 +203,13 @@
   override def handleMessage(message: EBMessage)
   {
     message match {
+      case msg: BufferUpdate
+        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+        Document_Model(msg.getBuffer) match {
+          case Some(model) => model.refresh()
+          case _ =>
+        }
+
       case msg: EditPaneUpdate =>
         val edit_pane = msg.getEditPane
         val buffer = edit_pane.getBuffer