src/Tools/jEdit/src/protocol_dockable.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 43721 fad8634cee62
child 46120 f7ee2e5a83dd
permissions -rw-r--r--
propagate editor perspective through document model;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/protocol_dockable.scala
wenzelm@36760
     2
    Author:     Makarius
wenzelm@36760
     3
wenzelm@37067
     4
Dockable window for protocol messages.
wenzelm@36760
     5
*/
wenzelm@34408
     6
wenzelm@34318
     7
package isabelle.jedit
wenzelm@34318
     8
wenzelm@34318
     9
wenzelm@36015
    10
import isabelle._
wenzelm@36015
    11
wenzelm@43520
    12
import java.lang.System
wenzelm@43520
    13
wenzelm@34772
    14
import scala.actors.Actor._
wenzelm@37067
    15
import scala.swing.{TextArea, ScrollPane}
wenzelm@34318
    16
wenzelm@34318
    17
import org.gjt.sp.jedit.View
wenzelm@34424
    18
wenzelm@34318
    19
wenzelm@37067
    20
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@34760
    21
{
wenzelm@37067
    22
  private val text_area = new TextArea
wenzelm@37067
    23
  set_content(new ScrollPane(text_area))
wenzelm@34772
    24
wenzelm@34772
    25
wenzelm@37067
    26
  /* main actor */
immler@34671
    27
wenzelm@37067
    28
  private val main_actor = actor {
wenzelm@34772
    29
    loop {
wenzelm@34772
    30
      react {
wenzelm@43721
    31
        case input: Isabelle_Process.Input =>
wenzelm@43721
    32
          Swing_Thread.now { text_area.append(input.toString + "\n") }
wenzelm@43721
    33
wenzelm@34772
    34
        case result: Isabelle_Process.Result =>
wenzelm@36987
    35
          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
wenzelm@34772
    36
wenzelm@37067
    37
        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
wenzelm@34772
    38
      }
wenzelm@34772
    39
    }
wenzelm@34772
    40
  }
wenzelm@34772
    41
wenzelm@39588
    42
  override def init() { Isabelle.session.raw_messages += main_actor }
wenzelm@39588
    43
  override def exit() { Isabelle.session.raw_messages -= main_actor }
wenzelm@34318
    44
}