src/Tools/jEdit/src/protocol_dockable.scala
author wenzelm
Wed, 08 Jun 2011 21:40:54 +0200
changeset 43286 a319da4fbfb0
parent 43282 5d294220ca43
child 43520 cec9b95fa35d
permissions -rw-r--r--
simplified directory structure;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 39588
diff changeset
     1
/*  Title:      Tools/jEdit/src/protocol_dockable.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     2
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     3
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
     4
Dockable window for protocol messages.
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     5
*/
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     6
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     8
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
     9
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34791
diff changeset
    10
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34791
diff changeset
    11
34772
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    12
import scala.actors.Actor._
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    13
import scala.swing.{TextArea, ScrollPane}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    14
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    15
import org.gjt.sp.jedit.View
34424
c880492754d0 setPreferredSize for floating dockables;
wenzelm
parents: 34408
diff changeset
    16
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    17
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    18
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    19
{
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    20
  private val text_area = new TextArea
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    21
  set_content(new ScrollPane(text_area))
34772
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    22
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    23
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    24
  /* main actor */
34671
d179fcb04cbc output_info specific to prover
immler@in.tum.de
parents: 34424
diff changeset
    25
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    26
  private val main_actor = actor {
34772
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    27
    loop {
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    28
      react {
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    29
        case result: Isabelle_Process.Result =>
36987
8af34e160968 show fully detailed protocol messages;
wenzelm
parents: 36760
diff changeset
    30
          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
34772
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    31
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    32
        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
34772
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    33
      }
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    34
    }
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    35
  }
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    36
39588
507fcf86e1e0 just one Session.raw_messages event bus;
wenzelm
parents: 38423
diff changeset
    37
  override def init() { Isabelle.session.raw_messages += main_actor }
507fcf86e1e0 just one Session.raw_messages event bus;
wenzelm
parents: 38423
diff changeset
    38
  override def exit() { Isabelle.session.raw_messages -= main_actor }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    39
}