src/Tools/jEdit/src/raw_output_dockable.scala
author wenzelm
Tue, 06 Sep 2011 11:25:27 +0200
changeset 44734 7313e2db3d39
parent 44297 b3bd26fd22d3
child 45633 2cb7e34f6096
permissions -rw-r--r--
more specific message channels to avoid potential bottle-neck of raw_messages;
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/raw_output_dockable.scala
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     3
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     4
Dockable window for raw process output (stdout).
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     5
*/
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     6
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     8
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
     9
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    10
import isabelle._
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    11
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43282
diff changeset
    12
import java.lang.System
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43282
diff changeset
    13
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    14
import scala.actors.Actor._
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    15
import scala.swing.{TextArea, ScrollPane}
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    16
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    17
import org.gjt.sp.jedit.View
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    18
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    19
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    20
class Raw_Output_Dockable(view: View, position: String)
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    21
  extends Dockable(view: View, position: String)
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    22
{
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    23
  private val text_area = new TextArea
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    24
  set_content(new ScrollPane(text_area))
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    25
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    26
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    27
  /* main actor */
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    28
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    29
  private val main_actor = actor {
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    30
    loop {
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    31
      react {
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    32
        case result: Isabelle_Process.Result =>
39588
507fcf86e1e0 just one Session.raw_messages event bus;
wenzelm
parents: 39516
diff changeset
    33
          if (result.is_stdout)
507fcf86e1e0 just one Session.raw_messages event bus;
wenzelm
parents: 39516
diff changeset
    34
            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    35
37067
31093f3687b5 simplified dockables using class Dockable;
wenzelm
parents: 37065
diff changeset
    36
        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    37
      }
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    38
    }
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    39
  }
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    40
44734
7313e2db3d39 more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents: 44297
diff changeset
    41
  override def init() { Isabelle.session.raw_output_messages += main_actor }
7313e2db3d39 more specific message channels to avoid potential bottle-neck of raw_messages;
wenzelm
parents: 44297
diff changeset
    42
  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
37065
2a73253b5898 separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff changeset
    43
}