| author | wenzelm |
| Fri, 01 Sep 2017 15:15:29 +0200 | |
| changeset 66591 | 6efa351190d0 |
| parent 66206 | 2d2082db735a |
| child 71601 | 97ccf48c2f0c |
| 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._ |
|
|
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
66206
diff
changeset
|
11 |
import isabelle.jedit_base.Dockable |
| 61208 | 12 |
|
13 |
import scala.swing.{Button, CheckBox}
|
|
14 |
import scala.swing.event.ButtonClicked |
|
15 |
||
16 |
import java.awt.BorderLayout |
|
17 |
import java.awt.event.{ComponentEvent, ComponentAdapter}
|
|
18 |
||
19 |
import org.gjt.sp.jedit.View |
|
20 |
||
21 |
||
22 |
class State_Dockable(view: View, position: String) extends Dockable(view, position) |
|
23 |
{
|
|
24 |
GUI_Thread.require {}
|
|
25 |
||
26 |
||
27 |
/* text area */ |
|
28 |
||
29 |
val pretty_text_area = new Pretty_Text_Area(view) |
|
30 |
set_content(pretty_text_area) |
|
31 |
||
32 |
override def detach_operation = pretty_text_area.detach_operation |
|
33 |
||
34 |
private val print_state = |
|
| 66082 | 35 |
new Query_Operation(PIDE.editor, view, "print_state", _ => (), |
| 61208 | 36 |
(snapshot, results, body) => |
37 |
pretty_text_area.update(snapshot, results, Pretty.separate(body))) |
|
38 |
||
39 |
||
40 |
/* resize */ |
|
41 |
||
42 |
private val delay_resize = |
|
43 |
GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
|
|
44 |
||
45 |
addComponentListener(new ComponentAdapter {
|
|
46 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
|
|
47 |
override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
|
|
48 |
}) |
|
49 |
||
50 |
private def handle_resize() |
|
51 |
{
|
|
52 |
GUI_Thread.require {}
|
|
53 |
||
54 |
pretty_text_area.resize( |
|
55 |
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
|
|
56 |
} |
|
57 |
||
58 |
||
| 61211 | 59 |
/* update */ |
| 61210 | 60 |
|
| 61801 | 61 |
def update_request(): Unit = |
62 |
GUI_Thread.require { print_state.apply_query(Nil) }
|
|
| 61720 | 63 |
|
| 61211 | 64 |
def update() |
| 61210 | 65 |
{
|
66 |
GUI_Thread.require {}
|
|
67 |
||
| 66091 | 68 |
PIDE.editor.current_node_snapshot(view) match {
|
| 61211 | 69 |
case Some(snapshot) => |
| 66082 | 70 |
(PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
|
| 61211 | 71 |
case (Some(command1), Some(command2)) if command1.id == command2.id => |
| 61801 | 72 |
case _ => update_request() |
| 61211 | 73 |
} |
74 |
case None => |
|
| 61210 | 75 |
} |
76 |
} |
|
77 |
||
78 |
||
| 61801 | 79 |
/* auto update */ |
80 |
||
81 |
private var auto_update_enabled = true |
|
82 |
||
83 |
private def auto_update(): Unit = |
|
84 |
GUI_Thread.require { if (auto_update_enabled) update() }
|
|
85 |
||
86 |
||
| 61208 | 87 |
/* controls */ |
88 |
||
| 61720 | 89 |
private val auto_update_button = new CheckBox("Auto update") {
|
90 |
tooltip = "Indicate automatic update following cursor movement" |
|
| 61801 | 91 |
reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() }
|
92 |
selected = auto_update_enabled |
|
| 61720 | 93 |
} |
94 |
||
| 61220 | 95 |
private val update_button = new Button("<html><b>Update</b></html>") {
|
| 61208 | 96 |
tooltip = "Update display according to the command at cursor position" |
| 61801 | 97 |
reactions += { case ButtonClicked(_) => update_request() }
|
| 61208 | 98 |
} |
99 |
||
| 61211 | 100 |
private val locate_button = new Button("Locate") {
|
| 61208 | 101 |
tooltip = "Locate printed command within source text" |
102 |
reactions += { case ButtonClicked(_) => print_state.locate_query() }
|
|
103 |
} |
|
104 |
||
105 |
private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
|
|
106 |
||
107 |
private val controls = |
|
| 66205 | 108 |
Wrap_Panel( |
109 |
List(auto_update_button, update_button, |
|
| 66206 | 110 |
locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
| 66205 | 111 |
|
| 61208 | 112 |
add(controls.peer, BorderLayout.NORTH) |
113 |
||
114 |
||
115 |
/* main */ |
|
116 |
||
117 |
private val main = |
|
118 |
Session.Consumer[Any](getClass.getName) {
|
|
119 |
case _: Session.Global_Options => |
|
120 |
GUI_Thread.later { handle_resize() }
|
|
| 61720 | 121 |
|
122 |
case changed: Session.Commands_Changed => |
|
| 61801 | 123 |
if (changed.assignment) GUI_Thread.later { auto_update() }
|
| 61720 | 124 |
|
125 |
case Session.Caret_Focus => |
|
| 61801 | 126 |
GUI_Thread.later { auto_update() }
|
| 61208 | 127 |
} |
128 |
||
129 |
override def init() |
|
130 |
{
|
|
131 |
PIDE.session.global_options += main |
|
| 61720 | 132 |
PIDE.session.commands_changed += main |
133 |
PIDE.session.caret_focus += main |
|
| 61208 | 134 |
handle_resize() |
135 |
print_state.activate() |
|
| 61801 | 136 |
auto_update() |
| 61208 | 137 |
} |
138 |
||
139 |
override def exit() |
|
140 |
{
|
|
141 |
print_state.deactivate() |
|
| 61720 | 142 |
PIDE.session.caret_focus -= main |
| 61208 | 143 |
PIDE.session.global_options -= main |
| 61720 | 144 |
PIDE.session.commands_changed -= main |
| 61208 | 145 |
delay_resize.revoke() |
146 |
} |
|
147 |
} |