src/Tools/jEdit/src/document_view.scala
changeset 57612 990ffb84489b
parent 56883 38c6b70e5e53
child 58748 8f92f17d8781
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5    def apply(text_area: TextArea): Option[Document_View] =
     1.6    {
     1.7 -    Swing_Thread.require {}
     1.8 +    GUI_Thread.require {}
     1.9      text_area.getClientProperty(key) match {
    1.10        case doc_view: Document_View => Some(doc_view)
    1.11        case _ => None
    1.12 @@ -36,7 +36,7 @@
    1.13  
    1.14    def exit(text_area: JEditTextArea)
    1.15    {
    1.16 -    Swing_Thread.require {}
    1.17 +    GUI_Thread.require {}
    1.18      apply(text_area) match {
    1.19        case None =>
    1.20        case Some(doc_view) =>
    1.21 @@ -71,7 +71,7 @@
    1.22  
    1.23    def perspective(snapshot: Document.Snapshot): Text.Perspective =
    1.24    {
    1.25 -    Swing_Thread.require {}
    1.26 +    GUI_Thread.require {}
    1.27  
    1.28      val active_command =
    1.29      {
    1.30 @@ -125,7 +125,7 @@
    1.31        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.32      {
    1.33        rich_text_area.robust_body(()) {
    1.34 -        Swing_Thread.assert {}
    1.35 +        GUI_Thread.assert {}
    1.36  
    1.37          val gutter = text_area.getGutter
    1.38          val width = GutterOptionPane.getSelectionAreaWidth
    1.39 @@ -173,7 +173,7 @@
    1.40    /* caret handling */
    1.41  
    1.42    private val delay_caret_update =
    1.43 -    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    1.44 +    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    1.45        session.caret_focus.post(Session.Caret_Focus)
    1.46      }
    1.47  
    1.48 @@ -187,7 +187,7 @@
    1.49    private object overview extends Text_Overview(this)
    1.50    {
    1.51      val delay_repaint =
    1.52 -      Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
    1.53 +      GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
    1.54    }
    1.55  
    1.56  
    1.57 @@ -200,7 +200,7 @@
    1.58  
    1.59        case changed: Session.Commands_Changed =>
    1.60          val buffer = model.buffer
    1.61 -        Swing_Thread.later {
    1.62 +        GUI_Thread.later {
    1.63            JEdit_Lib.buffer_lock(buffer) {
    1.64              if (model.buffer == text_area.getBuffer) {
    1.65                val snapshot = model.snapshot()