src/Tools/jEdit/src/jedit_resources.scala
changeset 57612 990ffb84489b
parent 56823 37be55461dbe
child 57622 2da79fca5708
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  
     1.5    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
     1.6    {
     1.7 -    Swing_Thread.now {
     1.8 +    GUI_Thread.now {
     1.9        JEdit_Lib.jedit_buffer(name) match {
    1.10          case Some(buffer) =>
    1.11            JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
    1.12 @@ -113,7 +113,7 @@
    1.13  
    1.14    override def commit(change: Session.Change)
    1.15    {
    1.16 -    if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
    1.17 +    if (change.syntax_changed) GUI_Thread.later { jEdit.propertiesChanged() }
    1.18    }
    1.19  }
    1.20