src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Sun, 07 Oct 2012 16:05:31 +0200
changeset 49726 2074197dc274
parent 49701 e2762f962042
child 49827 77582720af96
permissions -rw-r--r--
detach tooltip as dockable window;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49494
cbcccf2a0f6f renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
wenzelm
parents: 49473
diff changeset
     1
/*  Title:      Tools/jEdit/src/output_dockable.scala
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     3
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     4
Dockable window with result message output.
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     5
*/
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     6
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     8
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     9
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    10
import isabelle._
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    11
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    12
import scala.actors.Actor._
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    13
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    14
import scala.swing.{FlowPanel, Button, CheckBox}
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    15
import scala.swing.event.ButtonClicked
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    16
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    17
import java.lang.System
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    18
import java.awt.BorderLayout
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    19
import java.awt.event.{ComponentEvent, ComponentAdapter}
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    20
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    21
import org.gjt.sp.jedit.View
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    22
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    23
49494
cbcccf2a0f6f renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
wenzelm
parents: 49473
diff changeset
    24
class Output_Dockable(view: View, position: String) extends Dockable(view, position)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    25
{
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    26
  Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    27
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    28
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    29
  /* component state -- owned by Swing thread */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    30
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    31
  private var zoom_factor = 100
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    32
  private var show_tracing = false
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    33
  private var do_update = true
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    34
  private var current_snapshot = Document.State.init.snapshot()
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49412
diff changeset
    35
  private var current_state = Command.empty.init_state
49415
8b402b550a80 proper separation of output messages;
wenzelm
parents: 49414
diff changeset
    36
  private var current_output: List[XML.Tree] = Nil
49646
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    37
  private var current_tracing = 0
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    38
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    39
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49701
diff changeset
    40
  /* pretty text area */
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    41
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    42
  private val pretty_text_area = new Pretty_Text_Area(view)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    43
  set_content(pretty_text_area)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    44
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    45
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    46
  private def handle_resize()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    47
  {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    48
    Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    49
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    50
    pretty_text_area.resize(Isabelle.font_family(),
49701
e2762f962042 refined rich tooltip options;
wenzelm
parents: 49647
diff changeset
    51
      scala.math.round(Isabelle.font_size("jedit_font_scale") * zoom_factor / 100))
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    52
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    53
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    54
  private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    55
  {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    56
    Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    57
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    58
    val (new_snapshot, new_state) =
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    59
      Document_View(view.getTextArea) match {
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    60
        case Some(doc_view) =>
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    61
          val snapshot = doc_view.model.snapshot()
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    62
          if (follow && !snapshot.is_outdated) {
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    63
            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    64
              case Some(cmd) =>
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    65
                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    66
              case None =>
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    67
                (Document.State.init.snapshot(), Command.empty.init_state)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    68
            }
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    69
          }
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    70
          else (current_snapshot, current_state)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    71
        case None => (current_snapshot, current_state)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    72
      }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    73
49646
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    74
    val (new_output, new_tracing) =
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    75
      if (!restriction.isDefined || restriction.get.contains(new_state.command))
49646
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    76
      {
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    77
        val new_output =
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    78
          new_state.results.iterator.map(_._2)
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49646
diff changeset
    79
            .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList
49646
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    80
        val new_tracing =
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    81
          new_state.results.iterator.map(_._2).filter(Protocol.is_tracing(_)).length
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    82
        (new_output, new_tracing)
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    83
      }
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    84
      else (current_output, current_tracing)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    85
49415
8b402b550a80 proper separation of output messages;
wenzelm
parents: 49414
diff changeset
    86
    if (new_output != current_output)
49473
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49419
diff changeset
    87
      pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output))
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    88
49646
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    89
    if (new_tracing != current_tracing)
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    90
      tracing.text = tracing_text(new_tracing)
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    91
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    92
    current_snapshot = new_snapshot
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    93
    current_state = new_state
49415
8b402b550a80 proper separation of output messages;
wenzelm
parents: 49414
diff changeset
    94
    current_output = new_output
49646
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
    95
    current_tracing = new_tracing
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    96
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    97
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    98
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    99
  /* main actor */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   100
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   101
  private val main_actor = actor {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   102
    loop {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   103
      react {
49523
dc0670364008 tuned signature;
wenzelm
parents: 49513
diff changeset
   104
        case Session.Global_Options =>
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   105
          Swing_Thread.later { handle_resize() }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   106
        case changed: Session.Commands_Changed =>
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   107
          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   108
        case Session.Caret_Focus =>
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   109
          Swing_Thread.later { handle_update(do_update, None) }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   110
        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   111
      }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   112
    }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   113
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   114
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   115
  override def init()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   116
  {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   117
    Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   118
49523
dc0670364008 tuned signature;
wenzelm
parents: 49513
diff changeset
   119
    Isabelle.session.global_options += main_actor
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   120
    Isabelle.session.commands_changed += main_actor
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   121
    Isabelle.session.caret_focus += main_actor
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   122
    handle_update(true, None)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   123
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   124
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   125
  override def exit()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   126
  {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   127
    Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   128
49523
dc0670364008 tuned signature;
wenzelm
parents: 49513
diff changeset
   129
    Isabelle.session.global_options -= main_actor
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   130
    Isabelle.session.commands_changed -= main_actor
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   131
    Isabelle.session.caret_focus -= main_actor
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   132
    delay_resize.revoke()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   133
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   134
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   135
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   136
  /* resize */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   137
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   138
  private val delay_resize =
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   139
    Swing_Thread.delay_first(
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   140
      Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   141
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   142
  addComponentListener(new ComponentAdapter {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   143
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   144
  })
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   145
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   146
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   147
  /* controls */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   148
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   149
  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   150
  zoom.tooltip = "Zoom factor for basic font size"
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   151
49647
21ae8500d261 smarter handling of tracing messages;
wenzelm
parents: 49646
diff changeset
   152
  private def tracing_text(n: Int): String = "Tracing (" + n.toString + ")"
49646
77a0a53caa2f display number of tracing messages;
wenzelm
parents: 49523
diff changeset
   153
  private val tracing = new CheckBox(tracing_text(current_tracing)) {
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   154
    reactions += {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   155
      case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   156
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   157
  tracing.selected = show_tracing
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   158
  tracing.tooltip = "Indicate output of tracing messages"
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   159
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   160
  private val auto_update = new CheckBox("Auto update") {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   161
    reactions += {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   162
      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   163
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   164
  auto_update.selected = do_update
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   165
  auto_update.tooltip = "Indicate automatic update following cursor movement"
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   166
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   167
  private val update = new Button("Update") {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   168
    reactions += { case ButtonClicked(_) => handle_update(true, None) }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   169
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   170
  update.tooltip = "Update display according to the command at cursor position"
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   171
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   172
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   173
  add(controls.peer, BorderLayout.NORTH)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   174
}