src/Tools/jEdit/src/document_model.scala
changeset 57612 990ffb84489b
parent 57610 518e28a7c74b
child 57615 df1b3452d71c
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 11:08:24 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 11:19:24 2014 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5    def apply(buffer: Buffer): Option[Document_Model] =
     1.6    {
     1.7 -    Swing_Thread.require {}
     1.8 +    GUI_Thread.require {}
     1.9      buffer.getProperty(key) match {
    1.10        case model: Document_Model => Some(model)
    1.11        case _ => None
    1.12 @@ -34,7 +34,7 @@
    1.13  
    1.14    def exit(buffer: Buffer)
    1.15    {
    1.16 -    Swing_Thread.require {}
    1.17 +    GUI_Thread.require {}
    1.18      apply(buffer) match {
    1.19        case None =>
    1.20        case Some(model) =>
    1.21 @@ -46,7 +46,7 @@
    1.22  
    1.23    def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
    1.24    {
    1.25 -    Swing_Thread.require {}
    1.26 +    GUI_Thread.require {}
    1.27      apply(buffer).map(_.deactivate)
    1.28      val model = new Document_Model(session, buffer, node_name)
    1.29      buffer.setProperty(key, model)
    1.30 @@ -65,7 +65,7 @@
    1.31  
    1.32    def node_header(): Document.Node.Header =
    1.33    {
    1.34 -    Swing_Thread.require {}
    1.35 +    GUI_Thread.require {}
    1.36  
    1.37      if (is_theory) {
    1.38        JEdit_Lib.buffer_lock(buffer) {
    1.39 @@ -83,12 +83,12 @@
    1.40  
    1.41    /* perspective */
    1.42  
    1.43 -  // owned by Swing thread
    1.44 +  // owned by GUI thread
    1.45    private var _node_required = false
    1.46    def node_required: Boolean = _node_required
    1.47    def node_required_=(b: Boolean)
    1.48    {
    1.49 -    Swing_Thread.require {}
    1.50 +    GUI_Thread.require {}
    1.51      if (_node_required != b && is_theory) {
    1.52        _node_required = b
    1.53        PIDE.options_changed()
    1.54 @@ -98,7 +98,7 @@
    1.55  
    1.56    def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
    1.57    {
    1.58 -    Swing_Thread.require {}
    1.59 +    GUI_Thread.require {}
    1.60  
    1.61      if (Isabelle.continuous_checking && is_theory) {
    1.62        val snapshot = this.snapshot()
    1.63 @@ -135,12 +135,12 @@
    1.64  
    1.65    /* blob */
    1.66  
    1.67 -  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by Swing thread
    1.68 +  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by GUI thread
    1.69  
    1.70 -  private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
    1.71 +  private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
    1.72  
    1.73    def get_blob(): Option[Document.Blob] =
    1.74 -    Swing_Thread.require {
    1.75 +    GUI_Thread.require {
    1.76        if (is_theory) None
    1.77        else {
    1.78          val (bytes, chunk) =
    1.79 @@ -184,7 +184,7 @@
    1.80  
    1.81    /* pending edits */
    1.82  
    1.83 -  private object pending_edits  // owned by Swing thread
    1.84 +  private object pending_edits  // owned by GUI thread
    1.85    {
    1.86      private var pending_clear = false
    1.87      private val pending = new mutable.ListBuffer[Text.Edit]
    1.88 @@ -221,10 +221,10 @@
    1.89    }
    1.90  
    1.91    def snapshot(): Document.Snapshot =
    1.92 -    Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
    1.93 +    GUI_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
    1.94  
    1.95    def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
    1.96 -    Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) }
    1.97 +    GUI_Thread.require { pending_edits.flushed_edits(doc_blobs) }
    1.98  
    1.99  
   1.100    /* buffer listener */