src/Tools/jEdit/src/document_view.scala
changeset 46920 5f44c8bea84e
parent 46918 1752164d916b
child 46997 395b7277ed76
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Mar 14 15:23:50 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Mar 14 15:37:51 2012 +0100
     1.3 @@ -233,13 +233,15 @@
     1.4  
     1.5    private val mouse_motion_listener = new MouseMotionAdapter {
     1.6      override def mouseMoved(e: MouseEvent) {
     1.7 +      Swing_Thread.assert()
     1.8 +
     1.9        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
    1.10        val x = e.getX()
    1.11        val y = e.getY()
    1.12  
    1.13        if (!model.buffer.isLoaded) exit_control()
    1.14        else
    1.15 -        Isabelle.swing_buffer_lock(model.buffer) {
    1.16 +        Isabelle.buffer_lock(model.buffer) {
    1.17            val snapshot = update_snapshot()
    1.18  
    1.19            if (control) init_popup(snapshot, x, y)
    1.20 @@ -284,13 +286,15 @@
    1.21        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.22      {
    1.23        robust_body(()) {
    1.24 +        Swing_Thread.assert()
    1.25 +
    1.26          val gutter = text_area.getGutter
    1.27          val width = GutterOptionPane.getSelectionAreaWidth
    1.28          val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
    1.29          val FOLD_MARKER_SIZE = 12
    1.30  
    1.31          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    1.32 -          Isabelle.swing_buffer_lock(model.buffer) {
    1.33 +          Isabelle.buffer_lock(model.buffer) {
    1.34              val snapshot = update_snapshot()
    1.35              for (i <- 0 until physical_lines.length) {
    1.36                if (physical_lines(i) != -1) {