--- a/src/Tools/jEdit/src/document_model.scala Wed Mar 14 15:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Wed Mar 14 15:37:51 2012 +0100
@@ -61,12 +61,15 @@
/* header */
def node_header(): Document.Node_Header =
- Isabelle.swing_buffer_lock(buffer) {
+ {
+ Swing_Thread.require()
+ Isabelle.buffer_lock(buffer) {
Exn.capture {
Isabelle.thy_load.check_header(name,
Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
}
}
+ }
/* perspective */
--- a/src/Tools/jEdit/src/document_view.scala Wed Mar 14 15:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Wed Mar 14 15:37:51 2012 +0100
@@ -233,13 +233,15 @@
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseMoved(e: MouseEvent) {
+ Swing_Thread.assert()
+
control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
val x = e.getX()
val y = e.getY()
if (!model.buffer.isLoaded) exit_control()
else
- Isabelle.swing_buffer_lock(model.buffer) {
+ Isabelle.buffer_lock(model.buffer) {
val snapshot = update_snapshot()
if (control) init_popup(snapshot, x, y)
@@ -284,13 +286,15 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
robust_body(()) {
+ Swing_Thread.assert()
+
val gutter = text_area.getGutter
val width = GutterOptionPane.getSelectionAreaWidth
val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
val FOLD_MARKER_SIZE = 12
if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
- Isabelle.swing_buffer_lock(model.buffer) {
+ Isabelle.buffer_lock(model.buffer) {
val snapshot = update_snapshot()
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 14 15:23:50 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 14 15:37:51 2012 +0100
@@ -81,8 +81,10 @@
override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
{
+ Swing_Thread.assert()
+
val buffer = pane.getBuffer
- Isabelle.swing_buffer_lock(buffer) {
+ Isabelle.buffer_lock(buffer) {
Document_Model(buffer) match {
case None => null
case Some(model) =>