src/Tools/jEdit/src/jedit_editor.scala
changeset 57612 990ffb84489b
parent 57611 b6256ea3b7c5
child 57615 df1b3452d71c
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -22,15 +22,15 @@
     1.4  
     1.5    override def session: Session = PIDE.session
     1.6  
     1.7 -  // owned by Swing thread
     1.8 +  // owned by GUI thread
     1.9    private var removed_nodes = Set.empty[Document.Node.Name]
    1.10  
    1.11    def remove_node(name: Document.Node.Name): Unit =
    1.12 -    Swing_Thread.require { removed_nodes += name }
    1.13 +    GUI_Thread.require { removed_nodes += name }
    1.14  
    1.15    override def flush()
    1.16    {
    1.17 -    Swing_Thread.require {}
    1.18 +    GUI_Thread.require {}
    1.19  
    1.20      val doc_blobs = PIDE.document_blobs()
    1.21      val models = PIDE.document_models()
    1.22 @@ -45,7 +45,7 @@
    1.23    }
    1.24  
    1.25    private val delay_flush =
    1.26 -    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    1.27 +    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    1.28  
    1.29    def invoke(): Unit = delay_flush.invoke()
    1.30  
    1.31 @@ -53,17 +53,17 @@
    1.32    /* current situation */
    1.33  
    1.34    override def current_context: View =
    1.35 -    Swing_Thread.require { jEdit.getActiveView() }
    1.36 +    GUI_Thread.require { jEdit.getActiveView() }
    1.37  
    1.38    override def current_node(view: View): Option[Document.Node.Name] =
    1.39 -    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    1.40 +    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    1.41  
    1.42    override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    1.43 -    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    1.44 +    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    1.45  
    1.46    override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    1.47    {
    1.48 -    Swing_Thread.require {}
    1.49 +    GUI_Thread.require {}
    1.50  
    1.51      JEdit_Lib.jedit_buffer(name) match {
    1.52        case Some(buffer) =>
    1.53 @@ -77,7 +77,7 @@
    1.54  
    1.55    override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    1.56    {
    1.57 -    Swing_Thread.require {}
    1.58 +    GUI_Thread.require {}
    1.59  
    1.60      val text_area = view.getTextArea
    1.61      val buffer = view.getBuffer
    1.62 @@ -138,7 +138,7 @@
    1.63  
    1.64    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    1.65    {
    1.66 -    Swing_Thread.require {}
    1.67 +    GUI_Thread.require {}
    1.68  
    1.69      push_position(view)
    1.70