--- 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)
--- 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 {
--- 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
+ }
}
}
}
--- 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 */