src/Tools/jEdit/src/protocol_dockable.scala
author wenzelm
Wed, 23 Jul 2014 11:19:24 +0200
changeset 57612 990ffb84489b
parent 56715 52125652e82a
child 60074 38a64cc17403
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
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
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    12
import scala.swing.{TextArea, ScrollPane}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    13
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    14
import org.gjt.sp.jedit.View
34424
c880492754d0 setPreferredSize for floating dockables;
wenzelm
parents: 34408
diff changeset
    15
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    16
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    17
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    18
{
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    19
  private val text_area = new TextArea
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    20
  set_content(new ScrollPane(text_area))
34772
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    21
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    22
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56391
diff changeset
    23
  /* main */
34671
d179fcb04cbc output_info specific to prover
immler@in.tum.de
parents: 34424
diff changeset
    24
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56391
diff changeset
    25
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56391
diff changeset
    26
    Session.Consumer[Prover.Message](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56391
diff changeset
    27
      case input: Prover.Input =>
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56715
diff changeset
    28
        GUI_Thread.later { text_area.append(input.toString + "\n\n") }
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43520
diff changeset
    29
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56391
diff changeset
    30
      case output: Prover.Output =>
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56715
diff changeset
    31
        GUI_Thread.later { text_area.append(output.message.toString + "\n\n") }
34772
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    32
    }
1a79c9b9af82 proper actor wiring for raw process output;
wenzelm
parents: 34760
diff changeset
    33
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56391
diff changeset
    34
  override def init() { PIDE.session.all_messages += main }
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56391
diff changeset
    35
  override def exit() { PIDE.session.all_messages -= main }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    36
}