author | wenzelm |
Mon, 01 Mar 2021 22:22:12 +0100 | |
changeset 73340 | 0ffcad1f6130 |
parent 71704 | b9a5eb0f3b43 |
child 73987 | fc363a3b690a |
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 |
||
71601 | 32 |
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation |
61208 | 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 = |
|
71704 | 43 |
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } |
61208 | 44 |
|
45 |
addComponentListener(new ComponentAdapter { |
|
73340 | 46 |
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
47 |
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() |
|
61208 | 48 |
}) |
49 |
||
73340 | 50 |
private def handle_resize(): Unit = |
61208 | 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 |
|
73340 | 64 |
def update(): Unit = |
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 |
||
73340 | 129 |
override def init(): Unit = |
61208 | 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 |
||
73340 | 139 |
override def exit(): Unit = |
61208 | 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 |
} |