author | wenzelm |
Thu, 08 May 2014 11:47:38 +0200 | |
changeset 56907 | 0f3c375fd27c |
parent 56906 | 408b526911f7 |
child 56917 | 7b65f4da136d |
permissions | -rw-r--r-- |
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 zoom_factor = 100 |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
26 |
private var do_update = true |
52972 | 27 |
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
|
28 |
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
|
29 |
private var current_results = Command.Results.empty |
49415 | 30 |
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
|
31 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
32 |
|
49726 | 33 |
/* pretty text area */ |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
34 |
|
50541 | 35 |
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
|
36 |
set_content(pretty_text_area) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
37 |
|
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
56886
diff
changeset
|
38 |
override val detach_operation = Some(() => pretty_text_area.detach) |
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
56886
diff
changeset
|
39 |
|
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
40 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
41 |
private def handle_resize() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
42 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56299
diff
changeset
|
43 |
Swing_Thread.require {} |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
44 |
|
55825 | 45 |
pretty_text_area.resize( |
46 |
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
|
47 |
} |
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 |
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
|
50 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56299
diff
changeset
|
51 |
Swing_Thread.require {} |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
52 |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
53 |
val (new_snapshot, new_command, new_results) = |
52978 | 54 |
PIDE.editor.current_node_snapshot(view) match { |
55 |
case Some(snapshot) => |
|
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
56 |
if (follow && !snapshot.is_outdated) { |
52978 | 57 |
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
|
58 |
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
|
59 |
(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
|
60 |
case None => |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
61 |
(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
|
62 |
} |
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
63 |
} |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
67 |
|
50409
5eaebd8e52f4
discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
wenzelm
parents:
50207
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
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
|
72 |
} |
50409
5eaebd8e52f4
discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
wenzelm
parents:
50207
diff
changeset
|
73 |
else current_output |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
74 |
|
49415 | 75 |
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
|
76 |
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
|
77 |
|
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
current_results = new_results |
49415 | 81 |
current_output = new_output |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
82 |
} |
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 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
85 |
/* main */ |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
86 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
87 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
88 |
Session.Consumer[Any](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
89 |
case _: Session.Global_Options => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
90 |
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
|
91 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
92 |
case changed: Session.Commands_Changed => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
93 |
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
|
94 |
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
|
95 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
96 |
case Session.Caret_Focus => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
97 |
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
|
98 |
} |
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 |
override def init() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
101 |
{ |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
102 |
PIDE.session.global_options += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
103 |
PIDE.session.commands_changed += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
104 |
PIDE.session.caret_focus += main |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
105 |
handle_update(true, None) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
106 |
} |
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 |
override def exit() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
109 |
{ |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
110 |
PIDE.session.global_options -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
111 |
PIDE.session.commands_changed -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
112 |
PIDE.session.caret_focus -= main |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
113 |
delay_resize.revoke() |
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 |
|
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 |
/* resize */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
118 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
119 |
private val delay_resize = |
50207 | 120 |
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
|
121 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
122 |
addComponentListener(new ComponentAdapter { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
123 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
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 |
|
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 |
/* controls */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
128 |
|
52845 | 129 |
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) { |
130 |
tooltip = "Zoom factor for output font size" |
|
131 |
} |
|
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
132 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
133 |
private val auto_update = new CheckBox("Auto update") { |
52845 | 134 |
tooltip = "Indicate automatic update following cursor movement" |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
135 |
reactions += { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
136 |
case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } |
52845 | 137 |
selected = do_update |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
138 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
139 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
140 |
private val update = new Button("Update") { |
52845 | 141 |
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
|
142 |
reactions += { case ButtonClicked(_) => handle_update(true, None) } |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
143 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
144 |
|
53711
8ce7795256e1
improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents:
53177
diff
changeset
|
145 |
private val controls = |
56907
0f3c375fd27c
enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
wenzelm
parents:
56906
diff
changeset
|
146 |
new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, |
56886 | 147 |
pretty_text_area.search_label, pretty_text_area.search_pattern, zoom) |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
148 |
add(controls.peer, BorderLayout.NORTH) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
149 |
} |