# HG changeset patch # User wenzelm # Date 1283019881 -7200 # Node ID d95522496593419c8d9d70dd675b330d74517db0 # Parent f762b33e082139089bb39a09d285a3040b45d3b7 more careful locking of jEdit buffer; diff -r f762b33e0821 -r d95522496593 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 28 17:37:57 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 28 20:24:41 2010 +0200 @@ -256,10 +256,9 @@ override def markTokens(prev: TokenMarker.LineContext, handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = { - // FIXME proper synchronization / thread context (!??) - val snapshot = Swing_Thread.now { Document_Model.this.snapshot() } + Isabelle.swing_buffer_lock(buffer) { + val snapshot = Document_Model.this.snapshot() - Isabelle.buffer_read_lock(buffer) { val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext] val line = if (prev == null) 0 else previous.line + 1 val context = new Document_Model.Token_Markup.LineContext(line, previous) diff -r f762b33e0821 -r d95522496593 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Sat Aug 28 17:37:57 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Sat Aug 28 20:24:41 2010 +0200 @@ -103,29 +103,26 @@ loop { react { case Session.Commands_Changed(changed) => - Swing_Thread.now { - // FIXME cover doc states as well!!? + val buffer = model.buffer + Isabelle.swing_buffer_lock(buffer) { val snapshot = model.snapshot() - val buffer = model.buffer - Isabelle.buffer_read_lock(buffer) { - if (changed.exists(snapshot.node.commands.contains)) { - var visible_change = false + if (changed.exists(snapshot.node.commands.contains)) { + var visible_change = false + for ((command, start) <- snapshot.node.command_starts) { + if (changed(command)) { + val stop = start + command.length + val line1 = buffer.getLineOfOffset(snapshot.convert(start)) + val line2 = buffer.getLineOfOffset(snapshot.convert(stop)) + if (line2 >= text_area.getFirstLine && + line1 <= text_area.getFirstLine + text_area.getVisibleLines) + visible_change = true + text_area.invalidateLineRange(line1, line2) + } + } + // FIXME danger of deadlock!? + if (visible_change) model.buffer.propertiesChanged() - for ((command, start) <- snapshot.node.command_starts) { - if (changed(command)) { - val stop = start + command.length - val line1 = buffer.getLineOfOffset(snapshot.convert(start)) - val line2 = buffer.getLineOfOffset(snapshot.convert(stop)) - if (line2 >= text_area.getFirstLine && - line1 <= text_area.getFirstLine + text_area.getVisibleLines) - visible_change = true - text_area.invalidateLineRange(line1, line2) - } - } - if (visible_change) model.buffer.propertiesChanged() - - overview.repaint() // FIXME paint here!? - } + overview.repaint() // FIXME really paint here!? } } @@ -143,51 +140,51 @@ first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y0: Int, line_height: Int) { - Swing_Thread.assert() + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot() - val snapshot = model.snapshot() + val command_range: Iterable[(Command, Text.Offset)] = + { + val range = snapshot.node.command_range(snapshot.revert(start(0))) + if (range.hasNext) { + val (cmd0, start0) = range.next + new Iterable[(Command, Text.Offset)] { + def iterator = + Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0) + } + } + else Iterable.empty + } - val command_range: Iterable[(Command, Text.Offset)] = - { - val range = snapshot.node.command_range(snapshot.revert(start(0))) - if (range.hasNext) { - val (cmd0, start0) = range.next - new Iterable[(Command, Text.Offset)] { - def iterator = - Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0) + val saved_color = gfx.getColor + try { + var y = y0 + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + val line_start = start(i) + val line_end = model.visible_line_end(line_start, end(i)) + + val a = snapshot.revert(line_start) + val b = snapshot.revert(line_end) + val cmds = command_range.iterator. + dropWhile { case (cmd, c) => c + cmd.length <= a } . + takeWhile { case (_, c) => c < b } + + for ((command, command_start) <- cmds if !command.is_ignored) { + val p = + text_area.offsetToXY(line_start max snapshot.convert(command_start)) + val q = + text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length)) + assert(p.y == q.y) + gfx.setColor(Document_View.choose_color(snapshot, command)) + gfx.fillRect(p.x, y, q.x - p.x, line_height) + } + } + y += line_height } } - else Iterable.empty + finally { gfx.setColor(saved_color) } } - - val saved_color = gfx.getColor - try { - var y = y0 - for (i <- 0 until physical_lines.length) { - if (physical_lines(i) != -1) { - val line_start = start(i) - val line_end = model.visible_line_end(line_start, end(i)) - - val a = snapshot.revert(line_start) - val b = snapshot.revert(line_end) - val cmds = command_range.iterator. - dropWhile { case (cmd, c) => c + cmd.length <= a } . - takeWhile { case (_, c) => c < b } - - for ((command, command_start) <- cmds if !command.is_ignored) { - val p = - text_area.offsetToXY(line_start max snapshot.convert(command_start)) - val q = - text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length)) - assert(p.y == q.y) - gfx.setColor(Document_View.choose_color(snapshot, command)) - gfx.fillRect(p.x, y, q.x - p.x, line_height) - } - } - y += line_height - } - } - finally { gfx.setColor(saved_color) } } override def getToolTipText(x: Int, y: Int): String = @@ -268,7 +265,7 @@ super.paintComponent(gfx) Swing_Thread.assert() val buffer = model.buffer - Isabelle.buffer_read_lock(buffer) { + Isabelle.buffer_lock(buffer) { val snapshot = model.snapshot() val saved_color = gfx.getColor // FIXME needed!? try { diff -r f762b33e0821 -r d95522496593 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sat Aug 28 17:37:57 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sat Aug 28 20:24:41 2010 +0200 @@ -40,44 +40,45 @@ { def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = { - // FIXME lock buffer (!??) Swing_Thread.assert() - Document_Model(buffer) match { - case Some(model) => - val snapshot = model.snapshot() - val offset = snapshot.revert(buffer_offset) - snapshot.node.command_at(offset) match { - case Some((command, command_start)) => - // FIXME Isar_Document.Hyperlink extractor - (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) { - case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _), - List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) => - val Text.Range(begin, end) = snapshot.convert(info_range + command_start) - val line = buffer.getLineOfOffset(begin) + Isabelle.buffer_lock(buffer) { + Document_Model(buffer) match { + case Some(model) => + val snapshot = model.snapshot() + val offset = snapshot.revert(buffer_offset) + snapshot.node.command_at(offset) match { + case Some((command, command_start)) => + // FIXME Isar_Document.Hyperlink extractor + (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) { + case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _), + List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) => + val Text.Range(begin, end) = snapshot.convert(info_range + command_start) + val line = buffer.getLineOfOffset(begin) - (Position.File.unapply(props), Position.Line.unapply(props)) match { - case (Some(ref_file), Some(ref_line)) => - new External_Hyperlink(begin, end, line, ref_file, ref_line) - case _ => - (Position.Id.unapply(props), Position.Offset.unapply(props)) match { - case (Some(ref_id), Some(ref_offset)) => - snapshot.lookup_command(ref_id) match { - case Some(ref_cmd) => - snapshot.node.command_start(ref_cmd) match { - case Some(ref_cmd_start) => - new Internal_Hyperlink(begin, end, line, - snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset))) - case None => null - } - case None => null - } - case _ => null - } - } - } { null }).head.info - case None => null - } - case None => null + (Position.File.unapply(props), Position.Line.unapply(props)) match { + case (Some(ref_file), Some(ref_line)) => + new External_Hyperlink(begin, end, line, ref_file, ref_line) + case _ => + (Position.Id.unapply(props), Position.Offset.unapply(props)) match { + case (Some(ref_id), Some(ref_offset)) => + snapshot.lookup_command(ref_id) match { + case Some(ref_cmd) => + snapshot.node.command_start(ref_cmd) match { + case Some(ref_cmd_start) => + new Internal_Hyperlink(begin, end, line, + snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset))) + case None => null + } + case None => null + } + case _ => null + } + } + } { null }).head.info + case None => null + } + case None => null + } } } } diff -r f762b33e0821 -r d95522496593 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Sat Aug 28 17:37:57 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Sat Aug 28 20:24:41 2010 +0200 @@ -118,12 +118,15 @@ def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = jedit_text_areas().filter(_.getBuffer == buffer) - def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A = + def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.readLock(); body } finally { buffer.readUnlock() } } + def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = + Swing_Thread.now { buffer_lock(buffer) { body } } + /* dockable windows */