# HG changeset patch
# User wenzelm
# Date 1331735871 -3600
# Node ID 5f44c8bea84effd8a3099cce90fc549d720bc401
# Parent  82fc322fc30a183395f3f051aa331a549e8d6df7
more explicit indication of swing thread context;

diff -r 82fc322fc30a -r 5f44c8bea84e src/Tools/jEdit/src/document_model.scala
--- 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 */
diff -r 82fc322fc30a -r 5f44c8bea84e src/Tools/jEdit/src/document_view.scala
--- 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) {
diff -r 82fc322fc30a -r 5f44c8bea84e src/Tools/jEdit/src/isabelle_sidekick.scala
--- 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) =>