author | wenzelm |
Sat, 21 Nov 2015 14:10:32 +0100 | |
changeset 61717 | 5922db0430f1 |
parent 61205 | c0a5ebecc68b |
child 61725 | 1529c3eb6bac |
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 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
23 |
/* component state -- owned by GUI thread */ |
49398
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 | 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 | 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 | 32 |
/* pretty text area */ |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
33 |
|
50541 | 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 | 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 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
40 |
private def handle_resize() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
41 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
42 |
GUI_Thread.require {} |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
43 |
|
55825 | 44 |
pretty_text_area.resize( |
57044 | 45 |
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
|
46 |
} |
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 |
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
|
49 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
50 |
GUI_Thread.require {} |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
51 |
|
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
52 |
val (new_snapshot, new_command, new_results) = |
52978 | 53 |
PIDE.editor.current_node_snapshot(view) match { |
54 |
case Some(snapshot) => |
|
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
55 |
if (follow && !snapshot.is_outdated) { |
52978 | 56 |
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
|
57 |
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
|
58 |
(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
|
59 |
case None => |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
60 |
(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
|
61 |
} |
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
62 |
} |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
63 |
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
|
64 |
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
|
65 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
66 |
|
50409
5eaebd8e52f4
discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
wenzelm
parents:
50207
diff
changeset
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
} |
50409
5eaebd8e52f4
discontinued obsolete "Tracing" button -- limited tracing channel works sufficiently well;
wenzelm
parents:
50207
diff
changeset
|
72 |
else current_output |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
73 |
|
49415 | 74 |
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
|
75 |
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
|
76 |
|
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49418
diff
changeset
|
77 |
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
|
78 |
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
|
79 |
current_results = new_results |
49415 | 80 |
current_output = new_output |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
81 |
} |
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 |
|
61205 | 84 |
/* controls */ |
85 |
||
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
86 |
/* output state */ |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
87 |
|
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
88 |
private def output_state: Boolean = PIDE.options.bool("editor_output_state") |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
89 |
private def output_state_=(b: Boolean) |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
90 |
{ |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
91 |
if (output_state != b) { |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
92 |
PIDE.options.bool("editor_output_state") = b |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
93 |
PIDE.options_changed() |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
94 |
PIDE.editor.flush() |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
95 |
} |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
96 |
} |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
97 |
|
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
98 |
private val output_state_button = new CheckBox("Output state") |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
99 |
{ |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
100 |
tooltip = "Implicit output of proof state" |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
101 |
reactions += { case ButtonClicked(_) => output_state = selected } |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
102 |
selected = output_state |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
103 |
} |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
104 |
|
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
105 |
private val auto_update_button = new CheckBox("Auto update") { |
61205 | 106 |
tooltip = "Indicate automatic update following cursor movement" |
107 |
reactions += { |
|
108 |
case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } |
|
109 |
selected = do_update |
|
110 |
} |
|
111 |
||
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
112 |
private val update_button = new Button("Update") { |
61205 | 113 |
tooltip = "Update display according to the command at cursor position" |
114 |
reactions += { case ButtonClicked(_) => handle_update(true, None) } |
|
115 |
} |
|
116 |
||
117 |
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } |
|
118 |
||
119 |
private val controls = |
|
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
120 |
new Wrap_Panel(Wrap_Panel.Alignment.Right)(output_state_button, auto_update_button, |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
121 |
update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom) |
61205 | 122 |
add(controls.peer, BorderLayout.NORTH) |
123 |
||
124 |
||
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
125 |
/* main */ |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
126 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
127 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
128 |
Session.Consumer[Any](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
129 |
case _: Session.Global_Options => |
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
130 |
GUI_Thread.later { |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
131 |
output_state_button.selected = output_state |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
132 |
handle_update(do_update, None) |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
133 |
} |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52978
diff
changeset
|
134 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
135 |
case changed: Session.Commands_Changed => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
136 |
val restriction = if (changed.assignment) None else Some(changed.commands) |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
137 |
GUI_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
|
138 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
139 |
case Session.Caret_Focus => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
140 |
GUI_Thread.later { handle_update(do_update, None) } |
49398
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 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
143 |
override def init() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
144 |
{ |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
145 |
PIDE.session.global_options += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
146 |
PIDE.session.commands_changed += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
147 |
PIDE.session.caret_focus += main |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
148 |
handle_update(true, None) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
149 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
150 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
151 |
override def exit() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
152 |
{ |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
153 |
PIDE.session.global_options -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
154 |
PIDE.session.commands_changed -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
155 |
PIDE.session.caret_focus -= main |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
156 |
delay_resize.revoke() |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
157 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
158 |
|
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 |
/* resize */ |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
161 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
162 |
private val delay_resize = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
163 |
GUI_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
|
164 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
165 |
addComponentListener(new ComponentAdapter { |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
166 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
60750 | 167 |
override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
168 |
}) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
169 |
} |