src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Wed, 21 May 2014 16:21:11 +0200
changeset 57044 042d6e58cb40
parent 57042 5576d22abf3c
child 57612 990ffb84489b
permissions -rw-r--r--
more uniform Font_Info.Zoom_Box; misc tuning and clarification;
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
53711
8ce7795256e1 improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents: 53177
diff changeset
    12
import scala.swing.{Button, CheckBox}
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    13
import scala.swing.event.ButtonClicked
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    14
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    15
import java.awt.BorderLayout
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    16
import java.awt.event.{ComponentEvent, ComponentAdapter}
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    17
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    18
import org.gjt.sp.jedit.View
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    19
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    20
49494
cbcccf2a0f6f renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
wenzelm
parents: 49473
diff changeset
    21
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
    22
{
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    23
  /* component state -- owned by Swing thread */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    24
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    25
  private var do_update = true
52972
8fd8e1c14988 tuned signature;
wenzelm
parents: 52845
diff changeset
    26
  private var current_snapshot = Document.Snapshot.init
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    27
  private var current_command = Command.empty
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    28
  private var current_results = Command.Results.empty
49415
8b402b550a80 proper separation of output messages;
wenzelm
parents: 49414
diff changeset
    29
  private var current_output: List[XML.Tree] = Nil
49398
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
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49701
diff changeset
    32
  /* pretty text area */
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    33
50541
021f054ff1fa tuned signature;
wenzelm
parents: 50501
diff changeset
    34
  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
    35
  set_content(pretty_text_area)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    36
56918
a442dc6d244d clarified detach_operation: ignore empty output;
wenzelm
parents: 56917
diff changeset
    37
  override def detach_operation = pretty_text_area.detach_operation
56906
408b526911f7 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents: 56886
diff changeset
    38
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    39
57044
042d6e58cb40 more uniform Font_Info.Zoom_Box;
wenzelm
parents: 57042
diff changeset
    40
  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
042d6e58cb40 more uniform Font_Info.Zoom_Box;
wenzelm
parents: 57042
diff changeset
    41
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    42
  private def handle_resize()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    43
  {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56299
diff changeset
    44
    Swing_Thread.require {}
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    45
55825
694833e3e4a0 tuned signature -- separate module Font_Info;
wenzelm
parents: 55618
diff changeset
    46
    pretty_text_area.resize(
57044
042d6e58cb40 more uniform Font_Info.Zoom_Box;
wenzelm
parents: 57042
diff changeset
    47
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    48
  }
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
  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
    51
  {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56299
diff changeset
    52
    Swing_Thread.require {}
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    53
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    54
    val (new_snapshot, new_command, new_results) =
52978
37fbb3fde380 prefer PIDE editor operations;
wenzelm
parents: 52972
diff changeset
    55
      PIDE.editor.current_node_snapshot(view) match {
37fbb3fde380 prefer PIDE editor operations;
wenzelm
parents: 52972
diff changeset
    56
        case Some(snapshot) =>
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    57
          if (follow && !snapshot.is_outdated) {
52978
37fbb3fde380 prefer PIDE editor operations;
wenzelm
parents: 52972
diff changeset
    58
            PIDE.editor.current_command(view, snapshot) match {
53844
71f103629327 skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents: 53711
diff changeset
    59
              case Some(cmd) =>
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    60
                (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd))
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    61
              case None =>
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    62
                (Document.Snapshot.init, Command.empty, Command.Results.empty)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    63
            }
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    64
          }
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    65
          else (current_snapshot, current_command, current_results)
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    66
        case None => (current_snapshot, current_command, current_results)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    67
      }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    68
50409
5eaebd8e52f4 discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
wenzelm
parents: 50207
diff changeset
    69
    val new_output =
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    70
      if (!restriction.isDefined || restriction.get.contains(new_command)) {
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50499
diff changeset
    71
        val rendering = Rendering(new_snapshot, PIDE.options.value)
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    72
        rendering.output_messages(new_results)
50499
f496b2b7bafb rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm
parents: 50409
diff changeset
    73
      }
50409
5eaebd8e52f4 discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
wenzelm
parents: 50207
diff changeset
    74
      else current_output
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    75
49415
8b402b550a80 proper separation of output messages;
wenzelm
parents: 49414
diff changeset
    76
    if (new_output != current_output)
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    77
      pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output))
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    78
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49418
diff changeset
    79
    current_snapshot = new_snapshot
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    80
    current_command = new_command
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55825
diff changeset
    81
    current_results = new_results
49415
8b402b550a80 proper separation of output messages;
wenzelm
parents: 49414
diff changeset
    82
    current_output = new_output
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    83
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    84
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    85
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    86
  /* main */
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    87
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    88
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    89
    Session.Consumer[Any](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    90
      case _: Session.Global_Options =>
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    91
        Swing_Thread.later { handle_resize() }
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 52978
diff changeset
    92
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    93
      case changed: Session.Commands_Changed =>
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    94
        val restriction = if (changed.assignment) None else Some(changed.commands)
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    95
        Swing_Thread.later { handle_update(do_update, restriction) }
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 52978
diff changeset
    96
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    97
      case Session.Caret_Focus =>
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    98
        Swing_Thread.later { handle_update(do_update, None) }
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    99
    }
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
  override def init()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   102
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   103
    PIDE.session.global_options += main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   104
    PIDE.session.commands_changed += main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   105
    PIDE.session.caret_focus += main
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   106
    handle_update(true, None)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   107
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   108
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   109
  override def exit()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   110
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   111
    PIDE.session.global_options -= main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   112
    PIDE.session.commands_changed -= main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   113
    PIDE.session.caret_focus -= main
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   114
    delay_resize.revoke()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   115
  }
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
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   118
  /* resize */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   119
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   120
  private val delay_resize =
50207
54be125d8cdc tuned signature;
wenzelm
parents: 50206
diff changeset
   121
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   122
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   123
  addComponentListener(new ComponentAdapter {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   124
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   125
  })
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
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   128
  /* controls */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   129
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   130
  private val auto_update = new CheckBox("Auto update") {
52845
wenzelm
parents: 51616
diff changeset
   131
    tooltip = "Indicate automatic update following cursor movement"
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   132
    reactions += {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   133
      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
52845
wenzelm
parents: 51616
diff changeset
   134
    selected = do_update
49398
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
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   137
  private val update = new Button("Update") {
52845
wenzelm
parents: 51616
diff changeset
   138
    tooltip = "Update display according to the command at cursor position"
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   139
    reactions += { case ButtonClicked(_) => handle_update(true, None) }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   140
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   141
53711
8ce7795256e1 improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents: 53177
diff changeset
   142
  private val controls =
56907
0f3c375fd27c enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
wenzelm
parents: 56906
diff changeset
   143
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
57042
5576d22abf3c tuned signature;
wenzelm
parents: 56931
diff changeset
   144
      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   145
  add(controls.peer, BorderLayout.NORTH)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   146
}