| author | wenzelm |
| Tue, 17 Dec 2024 12:36:37 +0100 | |
| changeset 81615 | ebf954ceb4d1 |
| parent 81493 | 07e79b80e96d |
| child 81617 | 5c1059702995 |
| permissions | -rw-r--r-- |
| 61208 | 1 |
/* Title: Tools/jEdit/src/state_dockable.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Dockable window for proof state output. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import java.awt.BorderLayout |
|
13 |
import java.awt.event.{ComponentEvent, ComponentAdapter}
|
|
14 |
||
15 |
import org.gjt.sp.jedit.View |
|
16 |
||
17 |
||
| 75393 | 18 |
class State_Dockable(view: View, position: String) extends Dockable(view, position) {
|
|
81493
07e79b80e96d
clarified signature: avoid implicit functionality;
wenzelm
parents:
81489
diff
changeset
|
19 |
dockable => |
|
07e79b80e96d
clarified signature: avoid implicit functionality;
wenzelm
parents:
81489
diff
changeset
|
20 |
|
| 61208 | 21 |
GUI_Thread.require {}
|
22 |
||
23 |
||
| 81489 | 24 |
/* output text area */ |
| 61208 | 25 |
|
|
81615
ebf954ceb4d1
clarified split_pane layout: close on first display, open on first search;
wenzelm
parents:
81493
diff
changeset
|
26 |
private val output: Output_Area = |
|
ebf954ceb4d1
clarified split_pane layout: close on first display, open on first search;
wenzelm
parents:
81493
diff
changeset
|
27 |
new Output_Area(view) {
|
|
ebf954ceb4d1
clarified split_pane layout: close on first display, open on first search;
wenzelm
parents:
81493
diff
changeset
|
28 |
override def handle_shown(): Unit = split_pane_layout() |
|
ebf954ceb4d1
clarified split_pane layout: close on first display, open on first search;
wenzelm
parents:
81493
diff
changeset
|
29 |
} |
| 61208 | 30 |
|
| 81489 | 31 |
override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation |
| 61208 | 32 |
|
33 |
private val print_state = |
|
| 81489 | 34 |
new Query_Operation(PIDE.editor, view, "print_state", _ => (), output.pretty_text_area.update) |
| 61208 | 35 |
|
|
81493
07e79b80e96d
clarified signature: avoid implicit functionality;
wenzelm
parents:
81489
diff
changeset
|
36 |
output.setup(dockable) |
|
07e79b80e96d
clarified signature: avoid implicit functionality;
wenzelm
parents:
81489
diff
changeset
|
37 |
set_content(output.split_pane) |
| 61208 | 38 |
|
39 |
||
| 61211 | 40 |
/* update */ |
| 61210 | 41 |
|
| 61801 | 42 |
def update_request(): Unit = |
43 |
GUI_Thread.require { print_state.apply_query(Nil) }
|
|
| 61720 | 44 |
|
| 75393 | 45 |
def update(): Unit = {
|
| 61210 | 46 |
GUI_Thread.require {}
|
47 |
||
| 66091 | 48 |
PIDE.editor.current_node_snapshot(view) match {
|
| 61211 | 49 |
case Some(snapshot) => |
| 66082 | 50 |
(PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
|
| 61211 | 51 |
case (Some(command1), Some(command2)) if command1.id == command2.id => |
| 61801 | 52 |
case _ => update_request() |
| 61211 | 53 |
} |
54 |
case None => |
|
| 61210 | 55 |
} |
56 |
} |
|
57 |
||
58 |
||
| 61801 | 59 |
/* auto update */ |
60 |
||
61 |
private var auto_update_enabled = true |
|
62 |
||
63 |
private def auto_update(): Unit = |
|
64 |
GUI_Thread.require { if (auto_update_enabled) update() }
|
|
65 |
||
66 |
||
| 61208 | 67 |
/* controls */ |
68 |
||
| 75854 | 69 |
private val auto_update_button = new GUI.Check("Auto update", init = auto_update_enabled) {
|
| 61720 | 70 |
tooltip = "Indicate automatic update following cursor movement" |
| 75852 | 71 |
override def clicked(state: Boolean): Unit = {
|
72 |
auto_update_enabled = state |
|
73 |
auto_update() |
|
74 |
} |
|
| 61720 | 75 |
} |
76 |
||
| 75853 | 77 |
private val update_button = new GUI.Button("<html><b>Update</b></html>") {
|
| 61208 | 78 |
tooltip = "Update display according to the command at cursor position" |
| 75853 | 79 |
override def clicked(): Unit = update_request() |
| 61208 | 80 |
} |
81 |
||
| 75853 | 82 |
private val locate_button = new GUI.Button("Locate") {
|
| 61208 | 83 |
tooltip = "Locate printed command within source text" |
| 75853 | 84 |
override def clicked(): Unit = print_state.locate_query() |
| 61208 | 85 |
} |
86 |
||
87 |
private val controls = |
|
| 66205 | 88 |
Wrap_Panel( |
| 81379 | 89 |
List(auto_update_button, update_button, locate_button) ::: |
| 81489 | 90 |
output.pretty_text_area.search_zoom_components) |
| 66205 | 91 |
|
| 61208 | 92 |
add(controls.peer, BorderLayout.NORTH) |
93 |
||
94 |
||
95 |
/* main */ |
|
96 |
||
97 |
private val main = |
|
98 |
Session.Consumer[Any](getClass.getName) {
|
|
99 |
case _: Session.Global_Options => |
|
| 81489 | 100 |
GUI_Thread.later { output.handle_resize() }
|
| 61720 | 101 |
|
102 |
case changed: Session.Commands_Changed => |
|
| 61801 | 103 |
if (changed.assignment) GUI_Thread.later { auto_update() }
|
| 61720 | 104 |
|
105 |
case Session.Caret_Focus => |
|
| 61801 | 106 |
GUI_Thread.later { auto_update() }
|
| 61208 | 107 |
} |
108 |
||
| 75393 | 109 |
override def init(): Unit = {
|
| 61208 | 110 |
PIDE.session.global_options += main |
| 61720 | 111 |
PIDE.session.commands_changed += main |
112 |
PIDE.session.caret_focus += main |
|
| 81489 | 113 |
output.init() |
| 61208 | 114 |
print_state.activate() |
| 61801 | 115 |
auto_update() |
| 61208 | 116 |
} |
117 |
||
| 75393 | 118 |
override def exit(): Unit = {
|
| 61208 | 119 |
print_state.deactivate() |
| 61720 | 120 |
PIDE.session.caret_focus -= main |
| 61208 | 121 |
PIDE.session.global_options -= main |
| 61720 | 122 |
PIDE.session.commands_changed -= main |
| 81489 | 123 |
output.exit() |
| 61208 | 124 |
} |
125 |
} |