author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73987 | fc363a3b690a |
child 75809 | 1dd5d4f4b69e |
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 |
|
75393 | 21 |
class Output_Dockable(view: View, position: String) extends Dockable(view, position) { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
22 |
/* component state -- owned by GUI thread */ |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
23 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
24 |
private var do_update = true |
49415 | 25 |
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
|
26 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
27 |
|
49726 | 28 |
/* pretty text area */ |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
29 |
|
50541 | 30 |
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
|
31 |
set_content(pretty_text_area) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
32 |
|
71601 | 33 |
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation |
56906
408b526911f7
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents:
56886
diff
changeset
|
34 |
|
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
35 |
|
75393 | 36 |
private def handle_resize(): Unit = { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
37 |
GUI_Thread.require {} |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
38 |
|
55825 | 39 |
pretty_text_area.resize( |
57044 | 40 |
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
|
41 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
42 |
|
75393 | 43 |
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
44 |
GUI_Thread.require {} |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
45 |
|
65194 | 46 |
for { |
66082 | 47 |
snapshot <- PIDE.editor.current_node_snapshot(view) |
65194 | 48 |
if follow && !snapshot.is_outdated |
49 |
} { |
|
50 |
val (command, results) = |
|
66082 | 51 |
PIDE.editor.current_command(view, snapshot) match { |
65195 | 52 |
case Some(command) => (command, snapshot.command_results(command)) |
65194 | 53 |
case None => (Command.empty, Command.Results.empty) |
54 |
} |
|
55 |
||
56 |
val new_output = |
|
71601 | 57 |
if (restriction.isEmpty || restriction.get.contains(command)) |
65194 | 58 |
Rendering.output_messages(results) |
59 |
else current_output |
|
60 |
||
61 |
if (current_output != new_output) { |
|
62 |
pretty_text_area.update(snapshot, results, Pretty.separate(new_output)) |
|
63 |
current_output = new_output |
|
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
64 |
} |
65194 | 65 |
} |
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 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
68 |
|
61205 | 69 |
/* controls */ |
70 |
||
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
71 |
private def output_state: Boolean = PIDE.options.bool("editor_output_state") |
75393 | 72 |
private def output_state_=(b: Boolean): Unit = { |
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
73 |
if (output_state != b) { |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
74 |
PIDE.options.bool("editor_output_state") = b |
61725 | 75 |
PIDE.session.update_options(PIDE.options.value) |
66084 | 76 |
PIDE.editor.flush_edits(hidden = true) |
66082 | 77 |
PIDE.editor.flush() |
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
78 |
} |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
79 |
} |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
80 |
|
75393 | 81 |
private val output_state_button = new CheckBox("Proof state") { |
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61725
diff
changeset
|
82 |
tooltip = "Output of proof state (normally shown on State panel)" |
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
83 |
reactions += { case ButtonClicked(_) => output_state = selected } |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
84 |
selected = output_state |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
85 |
} |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
86 |
|
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
87 |
private val auto_update_button = new CheckBox("Auto update") { |
61205 | 88 |
tooltip = "Indicate automatic update following cursor movement" |
89 |
reactions += { |
|
90 |
case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } |
|
91 |
selected = do_update |
|
92 |
} |
|
93 |
||
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
94 |
private val update_button = new Button("Update") { |
61205 | 95 |
tooltip = "Update display according to the command at cursor position" |
96 |
reactions += { case ButtonClicked(_) => handle_update(true, None) } |
|
97 |
} |
|
98 |
||
99 |
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } |
|
100 |
||
101 |
private val controls = |
|
66205 | 102 |
Wrap_Panel( |
103 |
List(output_state_button, auto_update_button, |
|
66206 | 104 |
update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
66205 | 105 |
|
61205 | 106 |
add(controls.peer, BorderLayout.NORTH) |
107 |
||
108 |
||
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
109 |
/* main */ |
49398
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 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
112 |
Session.Consumer[Any](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
113 |
case _: Session.Global_Options => |
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
114 |
GUI_Thread.later { |
62259 | 115 |
handle_resize() |
61717
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
116 |
output_state_button.selected = output_state |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
117 |
handle_update(do_update, None) |
5922db0430f1
more direct access to option "editor_output_state";
wenzelm
parents:
61205
diff
changeset
|
118 |
} |
53177
dcac8d837b9c
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents:
52978
diff
changeset
|
119 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
120 |
case changed: Session.Commands_Changed => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
121 |
val restriction = if (changed.assignment) None else Some(changed.commands) |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
122 |
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
|
123 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
124 |
case Session.Caret_Focus => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
125 |
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
|
126 |
} |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
127 |
|
75393 | 128 |
override def init(): Unit = { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
129 |
PIDE.session.global_options += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
130 |
PIDE.session.commands_changed += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
131 |
PIDE.session.caret_focus += main |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
132 |
handle_update(true, None) |
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 |
|
75393 | 135 |
override def exit(): Unit = { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
136 |
PIDE.session.global_options -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
137 |
PIDE.session.commands_changed -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
138 |
PIDE.session.caret_focus -= main |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
139 |
delay_resize.revoke() |
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 |
|
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 |
/* resize */ |
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 |
private val delay_resize = |
71704 | 146 |
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } |
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
147 |
|
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
148 |
addComponentListener(new ComponentAdapter { |
73340 | 149 |
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
150 |
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() |
|
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
151 |
}) |
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset
|
152 |
} |