# HG changeset patch # User wenzelm # Date 1277714379 -7200 # Node ID 8ac597d6f3716510dd937df72401a3c32e804665 # Parent a47bb386b2382fd4c9cf5a3106791b0e45be2e71# Parent 1ae272fd4082fe82eeb01fc3dac07caa01d3f24f merged diff -r a47bb386b238 -r 8ac597d6f371 src/Pure/General/symbol.scala --- 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 diff -r a47bb386b238 -r 8ac597d6f371 src/Tools/jEdit/src/jedit/document_model.scala --- 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) diff -r a47bb386b238 -r 8ac597d6f371 src/Tools/jEdit/src/jedit/document_view.scala --- 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 */ diff -r a47bb386b238 -r 8ac597d6f371 src/Tools/jEdit/src/jedit/plugin.scala --- 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