# HG changeset patch # User wenzelm # Date 1282578373 -7200 # Node ID 5001ed24e129eef99eb637254e53d802c1ddc1b5 # Parent 0b1a63d0680586a6156129cce338e0dfbde6b9a3# Parent 7ab0ae836f74d7a6c56cf07d950e2771e9426dff merged diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/Concurrent/simple_thread.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/simple_thread.scala Mon Aug 23 17:46:13 2010 +0200 @@ -0,0 +1,37 @@ +/* Title: Pure/Concurrent/simple_thread.scala + Author: Makarius + +Simplified thread operations. +*/ + +package isabelle + + +import java.lang.Thread + +import scala.actors.Actor + + +object Simple_Thread +{ + /* plain thread */ + + def fork(name: String, daemon: Boolean = false)(body: => Unit): Thread = + { + val thread = new Thread(name) { override def run = body } + thread.setDaemon(daemon) + thread.start + thread + } + + + /* thread as actor */ + + def actor(name: String, daemon: Boolean = false)(body: => Unit): Actor = + { + val actor = Future.promise[Actor] + val thread = fork(name, daemon) { actor.fulfill(Actor.self); body } + actor.join + } +} + diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/General/table.ML Mon Aug 23 17:46:13 2010 +0200 @@ -392,6 +392,16 @@ fun merge_list eq = join (fn _ => Library.merge eq); +(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *) + +val _ = + PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab => + ml_pretty + (ML_Pretty.enum "," "{" "}" + (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty)) + (dest tab, depth))); + + (*final declarations of this structure!*) fun map f = map_table (K f); val map' = map_table; diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/IsaMakefile Mon Aug 23 17:46:13 2010 +0200 @@ -32,6 +32,7 @@ ML-Systems/polyml-5.2.ML \ ML-Systems/polyml.ML \ ML-Systems/polyml_common.ML \ + ML-Systems/pp_dummy.ML \ ML-Systems/pp_polyml.ML \ ML-Systems/proper_int.ML \ ML-Systems/single_assignment.ML \ diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/ML-Systems/ml_pretty.ML --- a/src/Pure/ML-Systems/ml_pretty.ML Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/ML-Systems/ml_pretty.ML Mon Aug 23 17:46:13 2010 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/ML-Systems/ml_pretty.ML Author: Makarius -Raw datatype for ML pretty printing. +Minimal support for raw ML pretty printing -- for boot-strapping only. *) structure ML_Pretty = @@ -12,5 +12,20 @@ String of string * int | Break of bool * int; +fun block prts = Block (("", ""), prts, 2); +fun str s = String (s, size s); +fun brk wd = Break (false, wd); + +fun pair pretty1 pretty2 ((x, y), depth: int) = + block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"]; + +fun enum sep lpar rpar pretty (args, depth) = + let + fun elems _ [] = [] + | elems 0 _ = [str "..."] + | elems d [x] = [pretty (x, d)] + | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs; + in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end; + end; diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/ML-Systems/polyml-5.2.1.ML --- a/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Aug 23 17:46:13 2010 +0200 @@ -25,4 +25,5 @@ use "ML-Systems/compiler_polyml-5.2.ML"; use "ML-Systems/pp_polyml.ML"; +use "ML-Systems/pp_dummy.ML"; diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/ML-Systems/polyml-5.2.ML --- a/src/Pure/ML-Systems/polyml-5.2.ML Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/ML-Systems/polyml-5.2.ML Mon Aug 23 17:46:13 2010 +0200 @@ -27,4 +27,5 @@ use "ML-Systems/compiler_polyml-5.2.ML"; use "ML-Systems/pp_polyml.ML"; +use "ML-Systems/pp_dummy.ML"; diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/ML-Systems/pp_dummy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/pp_dummy.ML Mon Aug 23 17:46:13 2010 +0200 @@ -0,0 +1,16 @@ +(* Title: Pure/ML-Systems/pp_dummy.ML + +Dummy setup for toplevel pretty printing. +*) + +fun ml_pretty _ = raise Fail "ml_pretty dummy"; +fun pretty_ml _ = raise Fail "pretty_ml dummy"; + +structure PolyML = +struct + fun addPrettyPrinter _ = (); + fun prettyRepresentation _ = + raise Fail "PolyML.prettyRepresentation dummy"; + open PolyML; +end; + diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Mon Aug 23 17:46:13 2010 +0200 @@ -18,6 +18,8 @@ use "ML-Systems/bash.ML"; use "ML-Systems/ml_name_space.ML"; use "ML-Systems/ml_pretty.ML"; +structure PolyML = struct end; +use "ML-Systems/pp_dummy.ML"; use "ML-Systems/use_context.ML"; diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/PIDE/command.scala Mon Aug 23 17:46:13 2010 +0200 @@ -8,10 +8,6 @@ package isabelle -import scala.actors.Actor, Actor._ -import scala.collection.mutable - - object Command { /** accumulated results from prover **/ @@ -40,7 +36,7 @@ def accumulate(message: XML.Tree): Command.State = message match { - case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit checks!? + case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit body check!? copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status) case XML.Elem(Markup(Markup.REPORT, _), msgs) => diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/ROOT.ML Mon Aug 23 17:46:13 2010 +0200 @@ -179,7 +179,8 @@ use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; use "Isar/runtime.ML"; -if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system +if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse + String.isPrefix "smlnj" ml_system then use "ML/ml_compiler.ML" else use "ML/ml_compiler_polyml-5.3.ML"; use "ML/ml_context.ML"; diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/System/isabelle_process.scala Mon Aug 23 17:46:13 2010 +0200 @@ -155,7 +155,7 @@ /* raw stdin */ private def stdin_actor(name: String, stream: OutputStream): Actor = - Library.thread_actor(name) { + Simple_Thread.actor(name) { val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset)) var finished = false while (!finished) { @@ -184,7 +184,7 @@ /* raw stdout */ private def stdout_actor(name: String, stream: InputStream): Actor = - Library.thread_actor(name) { + Simple_Thread.actor(name) { val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset)) var result = new StringBuilder(100) @@ -221,7 +221,7 @@ /* command input */ private def input_actor(name: String, raw_stream: OutputStream): Actor = - Library.thread_actor(name) { + Simple_Thread.actor(name) { val stream = new BufferedOutputStream(raw_stream) var finished = false while (!finished) { @@ -253,7 +253,7 @@ private class Protocol_Error(msg: String) extends Exception(msg) private def message_actor(name: String, stream: InputStream): Actor = - Library.thread_actor(name) { + Simple_Thread.actor(name) { val default_buffer = new Array[Byte](65536) var c = -1 @@ -344,7 +344,7 @@ /* exit process */ - Library.thread_actor("process_exit") { + Simple_Thread.actor("process_exit") { proc match { case None => case Some(p) => diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/System/session.scala Mon Aug 23 17:46:13 2010 +0200 @@ -69,8 +69,8 @@ private case class Started(timeout: Int, args: List[String]) private case object Stop - private lazy val session_actor = actor { - + private val session_actor = Simple_Thread.actor("session_actor", daemon = true) + { var prover: Isabelle_Process with Isar_Document = null @@ -199,8 +199,9 @@ /* main loop */ - loop { - react { + var finished = false + while (!finished) { + receive { case Started(timeout, args) => if (prover == null) { prover = new Isabelle_Process(system, self, args:_*) with Isar_Document @@ -211,10 +212,11 @@ } else reply(None) - case Stop => // FIXME clarify; synchronous + case Stop => // FIXME synchronous!? if (prover != null) { prover.kill prover = null + finished = true } case change: Document.Change if prover != null => @@ -235,7 +237,7 @@ /** buffered command changes (delay_first discipline) **/ - private lazy val command_change_buffer = actor + private val command_change_buffer = actor //{{{ { import scala.compat.Platform.currentTime @@ -286,36 +288,33 @@ private case class Edit_Version(edits: List[Document.Node_Text_Edit]) - private val editor_history = new Actor - { - @volatile private var history = Document.History.init + @volatile private var history = Document.History.init - def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = - history.snapshot(name, pending_edits, current_state()) + def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = + history.snapshot(name, pending_edits, current_state()) - def act - { - loop { - react { - case Edit_Version(edits) => - val prev = history.tip.current - val result = - isabelle.Future.fork { - val previous = prev.join - val former_assignment = current_state().the_assignment(previous).join // FIXME async!? - Thy_Syntax.text_edits(Session.this, previous, edits) - } - val change = new Document.Change(prev, edits, result) - history += change - change.current.map(_ => session_actor ! change) - reply(()) + private val editor_history = actor + { + loop { + react { + case Edit_Version(edits) => + val prev = history.tip.current + val result = + // FIXME potential denial-of-service concerning worker pool (!?!?) + isabelle.Future.fork { + val previous = prev.join + val former_assignment = current_state().the_assignment(previous).join // FIXME async!? + Thy_Syntax.text_edits(Session.this, previous, edits) + } + val change = new Document.Change(prev, edits, result) + history += change + change.current.map(_ => session_actor ! change) + reply(()) - case bad => System.err.println("editor_model: ignoring bad message " + bad) - } + case bad => System.err.println("editor_model: ignoring bad message " + bad) } } } - editor_history.start @@ -326,8 +325,5 @@ def stop() { session_actor ! Stop } - def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = - editor_history.snapshot(name, pending_edits) - def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) } } diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/build-jars --- a/src/Pure/build-jars Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/build-jars Mon Aug 23 17:46:13 2010 +0200 @@ -23,6 +23,7 @@ declare -a SOURCES=( Concurrent/future.scala + Concurrent/simple_thread.scala General/exn.scala General/linear_set.scala General/markup.scala diff -r 0b1a63d06805 -r 5001ed24e129 src/Pure/library.scala --- a/src/Pure/library.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Pure/library.scala Mon Aug 23 17:46:13 2010 +0200 @@ -7,11 +7,10 @@ package isabelle -import java.lang.{System, Thread} +import java.lang.System import java.awt.Component import javax.swing.JOptionPane -import scala.actors.Actor import scala.swing.ComboBox import scala.swing.event.SelectionChanged @@ -139,15 +138,4 @@ ((stop - start).toDouble / 1000000) + "ms elapsed time") Exn.release(result) } - - - /* thread as actor */ - - def thread_actor(name: String)(body: => Unit): Actor = - { - val actor = Future.promise[Actor] - val thread = new Thread(name) { override def run() = { actor.fulfill(Actor.self); body } } - thread.start - actor.join - } } diff -r 0b1a63d06805 -r 5001ed24e129 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 17:46:13 2010 +0200 @@ -10,7 +10,6 @@ import isabelle._ -import scala.actors.Actor, Actor._ import scala.collection.mutable import org.gjt.sp.jedit.Buffer @@ -260,61 +259,63 @@ // FIXME proper synchronization / thread context (!??) val snapshot = Swing_Thread.now { Document_Model.this.snapshot() } - 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) + 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) - val start = buffer.getLineStartOffset(line) - val stop = start + line_segment.count - val range = Text.Range(start, stop) - val former_range = snapshot.revert(range) + val start = buffer.getLineStartOffset(line) + val stop = start + line_segment.count + val range = Text.Range(start, stop) + val former_range = snapshot.revert(range) - /* FIXME - for (text_area <- Isabelle.jedit_text_areas(buffer) - if Document_View(text_area).isDefined) - Document_View(text_area).get.set_styles() - */ + /* FIXME + for (text_area <- Isabelle.jedit_text_areas(buffer) + if Document_View(text_area).isDefined) + Document_View(text_area).get.set_styles() + */ - def handle_token(style: Byte, offset: Text.Offset, length: Int) = - handler.handleToken(line_segment, style, offset, length, context) + def handle_token(style: Byte, offset: Text.Offset, length: Int) = + handler.handleToken(line_segment, style, offset, length, context) - val syntax = session.current_syntax() - val token_markup: PartialFunction[Text.Info[Any], Byte] = - { - case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)) - if syntax.keyword_kind(name).isDefined => - Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get) + val syntax = session.current_syntax() + val token_markup: PartialFunction[Text.Info[Any], Byte] = + { + case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)) + if syntax.keyword_kind(name).isDefined => + Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get) - case Text.Info(_, XML.Elem(Markup(name, _), _)) - if Document_Model.Token_Markup.token_style(name) != Token.NULL => - Document_Model.Token_Markup.token_style(name) - } + case Text.Info(_, XML.Elem(Markup(name, _), _)) + if Document_Model.Token_Markup.token_style(name) != Token.NULL => + Document_Model.Token_Markup.token_style(name) + } - var next_x = start - for { - (command, command_start) <- snapshot.node.command_range(former_range) - info <- snapshot.state(command).markup. - select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL) - val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start) - if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?) + var next_x = start + for { + (command, command_start) <- snapshot.node.command_range(former_range) + info <- snapshot.state(command).markup. + select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL) + val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start) + if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?) + } + { + val token_start = (abs_start - start) max 0 + val token_length = + (abs_stop - abs_start) - + ((start - abs_start) max 0) - + ((abs_stop - stop) max 0) + if (start + token_start > next_x) // FIXME ?? + handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x) + handle_token(info.info, token_start, token_length) + next_x = start + token_start + token_length + } + if (next_x < stop) // FIXME ?? + handle_token(Token.COMMENT1, next_x - start, stop - next_x) + + handle_token(Token.END, line_segment.count, 0) + handler.setLineContext(context) + context } - { - val token_start = (abs_start - start) max 0 - val token_length = - (abs_stop - abs_start) - - ((start - abs_start) max 0) - - ((abs_stop - stop) max 0) - if (start + token_start > next_x) // FIXME ?? - handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x) - handle_token(info.info, token_start, token_length) - next_x = start + token_start + token_length - } - if (next_x < stop) // FIXME ?? - handle_token(Token.COMMENT1, next_x - start, stop - next_x) - - handle_token(Token.END, line_segment.count, 0) - handler.setLineContext(context) - context } } diff -r 0b1a63d06805 -r 5001ed24e129 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 17:46:13 2010 +0200 @@ -106,8 +106,27 @@ Swing_Thread.now { // FIXME cover doc states as well!!? val snapshot = model.snapshot() - if (changed.exists(snapshot.node.commands.contains)) - full_repaint(snapshot, changed) + val buffer = model.buffer + Isabelle.buffer_read_lock(buffer) { + 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) + } + } + if (visible_change) model.buffer.propertiesChanged() + + overview.repaint() // FIXME paint here!? + } + } } case bad => System.err.println("command_change_actor: ignoring bad message " + bad) @@ -115,29 +134,6 @@ } } - def full_repaint(snapshot: Document.Snapshot, changed: Set[Command]) - { - Swing_Thread.require() - - val buffer = model.buffer - 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) - } - } - if (visible_change) model.buffer.propertiesChanged() - - overview.repaint() // FIXME paint here!? - } - /* text_area_extension */ @@ -269,20 +265,23 @@ override def paintComponent(gfx: Graphics) { super.paintComponent(gfx) + Swing_Thread.assert() val buffer = model.buffer - val snapshot = model.snapshot() - val saved_color = gfx.getColor // FIXME needed!? - try { - for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) { - val line1 = buffer.getLineOfOffset(snapshot.convert(start)) - val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1 - val y = line_to_y(line1) - val height = HEIGHT * (line2 - line1) - gfx.setColor(Document_View.choose_color(snapshot, command)) - gfx.fillRect(0, y, getWidth - 1, height) + Isabelle.buffer_read_lock(buffer) { + val snapshot = model.snapshot() + val saved_color = gfx.getColor // FIXME needed!? + try { + for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) { + val line1 = buffer.getLineOfOffset(snapshot.convert(start)) + val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1 + val y = line_to_y(line1) + val height = HEIGHT * (line2 - line1) + gfx.setColor(Document_View.choose_color(snapshot, command)) + gfx.fillRect(0, y, getWidth - 1, height) + } } + finally { gfx.setColor(saved_color) } } - finally { gfx.setColor(saved_color) } } private def line_to_y(line: Int): Int = diff -r 0b1a63d06805 -r 5001ed24e129 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 17:46:13 2010 +0200 @@ -40,6 +40,7 @@ { def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = { + // FIXME lock buffer (!??) Swing_Thread.assert() Document_Model(buffer) match { case Some(model) => diff -r 0b1a63d06805 -r 5001ed24e129 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 17:46:13 2010 +0200 @@ -44,7 +44,7 @@ stopped = false - // FIXME lock buffer !?? + // FIXME lock buffer (!??) val data = new SideKickParsedData(buffer.getName) val root = data.root data.getAsset(root).setEnd(buffer.getLength) @@ -66,6 +66,7 @@ override def complete(pane: EditPane, caret: Int): SideKickCompletion = { + // FIXME lock buffer (!?) val buffer = pane.getBuffer val line = buffer.getLineOfOffset(caret) diff -r 0b1a63d06805 -r 5001ed24e129 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 23 15:30:42 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 23 17:46:13 2010 +0200 @@ -118,6 +118,12 @@ def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = jedit_text_areas().filter(_.getBuffer == buffer) + def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A = + { + try { buffer.readLock(); body } + finally { buffer.readUnlock() } + } + /* dockable windows */