src/Tools/jEdit/src/document_view.scala
changeset 49406 38db4832b210
parent 49360 37c1297aa562
child 49407 215ba6884bdf
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 15:52:50 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 17:49:11 2012 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4      override def mouseMoved(e: MouseEvent) {
     1.5        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
     1.6        if (control && model.buffer.isLoaded) {
     1.7 -        Isabelle.buffer_lock(model.buffer) {
     1.8 +        JEdit_Lib.buffer_lock(model.buffer) {
     1.9            val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    1.10            val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
    1.11            active_areas.foreach(_.update_rendering(rendering, mouse_range))
    1.12 @@ -248,7 +248,7 @@
    1.13          val FOLD_MARKER_SIZE = 12
    1.14  
    1.15          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    1.16 -          Isabelle.buffer_lock(model.buffer) {
    1.17 +          JEdit_Lib.buffer_lock(model.buffer) {
    1.18              val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    1.19  
    1.20              for (i <- 0 until physical_lines.length) {
    1.21 @@ -308,7 +308,7 @@
    1.22          case changed: Session.Commands_Changed =>
    1.23            val buffer = model.buffer
    1.24            Swing_Thread.later {
    1.25 -            Isabelle.buffer_lock(buffer) {
    1.26 +            JEdit_Lib.buffer_lock(buffer) {
    1.27                if (model.buffer == text_area.getBuffer) {
    1.28                  val snapshot = model.snapshot()
    1.29