author | wenzelm |
Tue, 21 Apr 2020 19:07:11 +0200 | |
changeset 71774 | 491f185fd705 |
parent 71476 | ecefde4f9103 |
child 72761 | 4519eeefe3b5 |
permissions | -rw-r--r-- |
66098 | 1 |
/* Title: Tools/VSCode/src/state_panel.scala |
66096 | 2 |
Author: Makarius |
3 |
||
4 |
Show proof state. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
||
66098 | 13 |
object State_Panel |
66096 | 14 |
{ |
15 |
private val make_id = Counter.make() |
|
66098 | 16 |
private val instances = Synchronized(Map.empty[Counter.ID, State_Panel]) |
66096 | 17 |
|
18 |
def init(server: Server) |
|
19 |
{ |
|
66098 | 20 |
val instance = new State_Panel(server) |
66096 | 21 |
instances.change(_ + (instance.id -> instance)) |
22 |
instance.init() |
|
23 |
} |
|
24 |
||
25 |
def exit(id: Counter.ID) |
|
26 |
{ |
|
27 |
instances.change(map => |
|
28 |
map.get(id) match { |
|
29 |
case None => map |
|
30 |
case Some(instance) => instance.exit(); map - id |
|
31 |
}) |
|
32 |
} |
|
33 |
||
34 |
def locate(id: Counter.ID): Unit = |
|
35 |
instances.value.get(id).foreach(state => |
|
36 |
state.server.editor.send_dispatcher(state.locate())) |
|
37 |
||
38 |
def update(id: Counter.ID): Unit = |
|
39 |
instances.value.get(id).foreach(state => |
|
40 |
state.server.editor.send_dispatcher(state.update())) |
|
66211 | 41 |
|
42 |
def auto_update(id: Counter.ID, enabled: Boolean): Unit = |
|
43 |
instances.value.get(id).foreach(state => |
|
44 |
state.server.editor.send_dispatcher(state.auto_update(Some(enabled)))) |
|
66096 | 45 |
} |
46 |
||
47 |
||
66098 | 48 |
class State_Panel private(val server: Server) |
66096 | 49 |
{ |
50 |
/* output */ |
|
51 |
||
66098 | 52 |
val id: Counter.ID = State_Panel.make_id() |
66096 | 53 |
|
54 |
private def output(content: String): Unit = |
|
55 |
server.channel.write(Protocol.State_Output(id, content)) |
|
56 |
||
57 |
||
58 |
/* query operation */ |
|
59 |
||
66397 | 60 |
private val output_active = Synchronized(true) |
61 |
||
66096 | 62 |
private val print_state = |
63 |
new Query_Operation(server.editor, (), "print_state", _ => (), |
|
64 |
(snapshot, results, body) => |
|
66397 | 65 |
if (output_active.value) { |
66096 | 66 |
val text = server.resources.output_pretty_message(Pretty.separate(body)) |
67 |
val content = |
|
68 |
HTML.output_document( |
|
69 |
List(HTML.style(HTML.fonts_css()), |
|
66212 | 70 |
HTML.style_file(HTML.isabelle_css), |
66211 | 71 |
HTML.script(controls_script)), |
66201
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
72 |
List(controls, HTML.source(text)), |
67337
4254cfd15b00
more tight HTML output: avoid extra lines within <pre>;
wenzelm
parents:
66397
diff
changeset
|
73 |
css = "", structural = true) |
66096 | 74 |
output(content) |
75 |
}) |
|
76 |
||
77 |
def locate() { print_state.locate_query() } |
|
78 |
||
79 |
def update() |
|
80 |
{ |
|
81 |
server.editor.current_node_snapshot(()) match { |
|
82 |
case Some(snapshot) => |
|
83 |
(server.editor.current_command((), snapshot), print_state.get_location) match { |
|
84 |
case (Some(command1), Some(command2)) if command1.id == command2.id => |
|
85 |
case _ => print_state.apply_query(Nil) |
|
86 |
} |
|
87 |
case None => |
|
88 |
} |
|
89 |
} |
|
90 |
||
91 |
||
92 |
/* auto update */ |
|
93 |
||
94 |
private val auto_update_enabled = Synchronized(true) |
|
95 |
||
66211 | 96 |
def auto_update(set: Option[Boolean] = None) |
97 |
{ |
|
98 |
val enabled = |
|
99 |
auto_update_enabled.guarded_access(a => |
|
100 |
set match { |
|
101 |
case None => Some((a, a)) |
|
102 |
case Some(b) => Some((b, b)) |
|
103 |
}) |
|
104 |
if (enabled) update() |
|
105 |
} |
|
66096 | 106 |
|
107 |
||
66201
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
108 |
/* controls */ |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
109 |
|
66211 | 110 |
private def controls_script = |
111 |
""" |
|
71476
ecefde4f9103
proper message passing -- discontinued obsolete auxiliary commands;
wenzelm
parents:
70302
diff
changeset
|
112 |
const vscode = acquireVsCodeApi(); |
ecefde4f9103
proper message passing -- discontinued obsolete auxiliary commands;
wenzelm
parents:
70302
diff
changeset
|
113 |
|
66211 | 114 |
function invoke_auto_update(enabled) |
71476
ecefde4f9103
proper message passing -- discontinued obsolete auxiliary commands;
wenzelm
parents:
70302
diff
changeset
|
115 |
{ vscode.postMessage({'command': 'auto_update', 'enabled': enabled}) } |
66211 | 116 |
|
71476
ecefde4f9103
proper message passing -- discontinued obsolete auxiliary commands;
wenzelm
parents:
70302
diff
changeset
|
117 |
function invoke_update() |
ecefde4f9103
proper message passing -- discontinued obsolete auxiliary commands;
wenzelm
parents:
70302
diff
changeset
|
118 |
{ vscode.postMessage({'command': 'update'}) } |
66211 | 119 |
|
71476
ecefde4f9103
proper message passing -- discontinued obsolete auxiliary commands;
wenzelm
parents:
70302
diff
changeset
|
120 |
function invoke_locate() |
ecefde4f9103
proper message passing -- discontinued obsolete auxiliary commands;
wenzelm
parents:
70302
diff
changeset
|
121 |
{ vscode.postMessage({'command': 'locate'}) } |
66211 | 122 |
""" |
66201
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
123 |
|
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
124 |
private def auto_update_button: XML.Elem = |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
125 |
HTML.GUI.checkbox(HTML.text("Auto update"), |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
126 |
name = "auto_update", |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
127 |
tooltip = "Indicate automatic update following cursor movement", |
66211 | 128 |
selected = auto_update_enabled.value, |
129 |
script = "invoke_auto_update(this.checked)") |
|
66201
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
130 |
|
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
131 |
private def update_button: XML.Elem = |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
132 |
HTML.GUI.button(List(HTML.bold(HTML.text("Update"))), |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
133 |
name = "update", |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
134 |
tooltip = "Update display according to the command at cursor position", |
66211 | 135 |
script = "invoke_update()") |
66201
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
136 |
|
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
137 |
private def locate_button: XML.Elem = |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
138 |
HTML.GUI.button(HTML.text("Locate"), |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
139 |
name = "locate", |
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
140 |
tooltip = "Locate printed command within source text", |
66211 | 141 |
script = "invoke_locate()") |
66201
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
142 |
|
66213
9380ec9babfb
proper dynamic controls, notably for auto_update_enabled;
wenzelm
parents:
66212
diff
changeset
|
143 |
private def controls: XML.Elem = |
66211 | 144 |
HTML.Wrap_Panel(List(auto_update_button, update_button, locate_button)) |
66201
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
145 |
|
d8f2c745f572
GUI controls similar to Tools/jEdit/src/state_dockable.scala;
wenzelm
parents:
66099
diff
changeset
|
146 |
|
66096 | 147 |
/* main */ |
148 |
||
149 |
private val main = |
|
150 |
Session.Consumer[Any](getClass.getName) { |
|
66099 | 151 |
case changed: Session.Commands_Changed => |
152 |
if (changed.assignment) auto_update() |
|
153 |
||
154 |
case Session.Caret_Focus => |
|
155 |
auto_update() |
|
66096 | 156 |
} |
157 |
||
158 |
def init() |
|
159 |
{ |
|
160 |
server.session.commands_changed += main |
|
161 |
server.session.caret_focus += main |
|
162 |
server.editor.send_wait_dispatcher { print_state.activate() } |
|
163 |
server.editor.send_dispatcher { auto_update() } |
|
164 |
} |
|
165 |
||
166 |
def exit() |
|
167 |
{ |
|
66397 | 168 |
output_active.change(_ => false) |
66096 | 169 |
server.session.commands_changed -= main |
170 |
server.session.caret_focus -= main |
|
66397 | 171 |
server.editor.send_wait_dispatcher { print_state.deactivate() } |
66096 | 172 |
} |
173 |
} |