author | wenzelm |
Fri, 11 Oct 2013 23:12:04 +0200 | |
changeset 54327 | 148903e47b26 |
parent 54325 | 2c4155003352 |
child 54640 | bbd2fa353809 |
permissions | -rw-r--r-- |
52981 | 1 |
/* Title: Pure/PIDE/query_operation.scala |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
3 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
4 |
One-shot query operations via asynchronous print functions and temporary |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
5 |
document overlays. |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
6 |
*/ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
7 |
|
52981 | 8 |
package isabelle |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
9 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
10 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
11 |
import scala.actors.Actor._ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
12 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
13 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
14 |
object Query_Operation |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
15 |
{ |
52935 | 16 |
object Status extends Enumeration |
17 |
{ |
|
18 |
val WAITING = Value("waiting") |
|
19 |
val RUNNING = Value("running") |
|
20 |
val FINISHED = Value("finished") |
|
53872
6e69f9ca8f1c
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents:
53844
diff
changeset
|
21 |
val REMOVED = Value("removed") |
52935 | 22 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
23 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
24 |
|
52980 | 25 |
class Query_Operation[Editor_Context]( |
26 |
editor: Editor[Editor_Context], |
|
27 |
editor_context: Editor_Context, |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
28 |
operation_name: String, |
52935 | 29 |
consume_status: Query_Operation.Status.Value => Unit, |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
30 |
consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
31 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
32 |
private val instance = Document_ID.make().toString |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
33 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
34 |
|
52877 | 35 |
/* implicit state -- owned by Swing thread */ |
52874 | 36 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
37 |
private var current_location: Option[Command] = None |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
38 |
private var current_query: List[String] = Nil |
52876 | 39 |
private var current_update_pending = false |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
40 |
private var current_output: List[XML.Tree] = Nil |
53872
6e69f9ca8f1c
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents:
53844
diff
changeset
|
41 |
private var current_status = Query_Operation.Status.REMOVED |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
42 |
private var current_exec_id = Document_ID.none |
52876 | 43 |
|
44 |
private def reset_state() |
|
45 |
{ |
|
46 |
current_location = None |
|
47 |
current_query = Nil |
|
48 |
current_update_pending = false |
|
49 |
current_output = Nil |
|
53872
6e69f9ca8f1c
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents:
53844
diff
changeset
|
50 |
current_status = Query_Operation.Status.REMOVED |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
51 |
current_exec_id = Document_ID.none |
52876 | 52 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
53 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
54 |
private def remove_overlay() |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
55 |
{ |
54310
6ddeb83eb67a
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents:
53872
diff
changeset
|
56 |
current_location match { |
6ddeb83eb67a
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents:
53872
diff
changeset
|
57 |
case None => |
6ddeb83eb67a
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents:
53872
diff
changeset
|
58 |
case Some(command) => |
6ddeb83eb67a
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents:
53872
diff
changeset
|
59 |
editor.remove_overlay(command, operation_name, instance :: current_query) |
6ddeb83eb67a
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents:
53872
diff
changeset
|
60 |
editor.flush() |
6ddeb83eb67a
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents:
53872
diff
changeset
|
61 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
62 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
63 |
|
52877 | 64 |
|
65 |
/* content update */ |
|
66 |
||
67 |
private def content_update() |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
68 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
69 |
Swing_Thread.require() |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
70 |
|
52876 | 71 |
|
72 |
/* snapshot */ |
|
73 |
||
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
74 |
val (snapshot, state, removed) = |
52876 | 75 |
current_location match { |
76 |
case Some(cmd) => |
|
52974 | 77 |
val snapshot = editor.node_snapshot(cmd.node_name) |
52876 | 78 |
val state = snapshot.state.command_state(snapshot.version, cmd) |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
79 |
val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) |
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
80 |
(snapshot, state, removed) |
52876 | 81 |
case None => |
52972 | 82 |
(Document.Snapshot.init, Command.empty.init_state, true) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
83 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
84 |
|
52876 | 85 |
val results = |
86 |
(for { |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
87 |
(_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries |
52876 | 88 |
if props.contains((Markup.INSTANCE, instance)) |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
89 |
} yield elem).toList |
52876 | 90 |
|
91 |
||
92 |
/* output */ |
|
93 |
||
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
94 |
val new_output = |
52876 | 95 |
for { |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
96 |
XML.Elem(_, List(XML.Elem(markup, body))) <- results |
52876 | 97 |
if Markup.messages.contains(markup.name) |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
98 |
} yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body) |
52876 | 99 |
|
100 |
||
101 |
/* status */ |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
102 |
|
52935 | 103 |
def get_status(name: String, status: Query_Operation.Status.Value) |
104 |
: Option[Query_Operation.Status.Value] = |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
105 |
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
52876 | 106 |
|
107 |
val new_status = |
|
53872
6e69f9ca8f1c
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents:
53844
diff
changeset
|
108 |
if (removed) Query_Operation.Status.REMOVED |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
109 |
else |
52935 | 110 |
get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse |
111 |
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse |
|
112 |
Query_Operation.Status.WAITING |
|
52876 | 113 |
|
52935 | 114 |
if (new_status == Query_Operation.Status.RUNNING) |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
115 |
results.collectFirst( |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
116 |
{ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
117 |
case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem)) |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
118 |
if elem.name == Markup.RUNNING => id |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
119 |
}).foreach(id => current_exec_id = id) |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
120 |
|
52876 | 121 |
|
122 |
/* state update */ |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
123 |
|
52876 | 124 |
if (current_output != new_output || current_status != new_status) { |
125 |
if (snapshot.is_outdated) |
|
126 |
current_update_pending = true |
|
127 |
else { |
|
52877 | 128 |
current_update_pending = false |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
129 |
if (current_output != new_output && !removed) { |
52877 | 130 |
current_output = new_output |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
131 |
consume_output(snapshot, state.results, new_output) |
52877 | 132 |
} |
133 |
if (current_status != new_status) { |
|
134 |
current_status = new_status |
|
52935 | 135 |
consume_status(new_status) |
54310
6ddeb83eb67a
clarified remove_overlay: always flush in order to make sure that apply_query can make a fresh start with the same arguments (see also 6e69f9ca8f1c) -- NB: print functions are idempotent;
wenzelm
parents:
53872
diff
changeset
|
136 |
if (new_status == Query_Operation.Status.REMOVED) |
52877 | 137 |
remove_overlay() |
138 |
} |
|
52876 | 139 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
140 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
141 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
142 |
|
52877 | 143 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
144 |
/* query operations */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
145 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
146 |
def cancel_query(): Unit = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
52935
diff
changeset
|
147 |
Swing_Thread.require { editor.session.cancel_exec(current_exec_id) } |
52877 | 148 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
149 |
def apply_query(query: List[String]) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
150 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
151 |
Swing_Thread.require() |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
152 |
|
52980 | 153 |
editor.current_node_snapshot(editor_context) match { |
52978 | 154 |
case Some(snapshot) => |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
155 |
remove_overlay() |
52876 | 156 |
reset_state() |
52972 | 157 |
consume_output(Document.Snapshot.init, Command.Results.empty, Nil) |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
158 |
if (!snapshot.is_outdated) { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
159 |
editor.current_command(editor_context, snapshot) match { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
160 |
case Some(command) => |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
161 |
current_location = Some(command) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
162 |
current_query = query |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
163 |
current_status = Query_Operation.Status.WAITING |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
164 |
editor.insert_overlay(command, operation_name, instance :: query) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
165 |
case None => |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
166 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
167 |
} |
52935 | 168 |
consume_status(current_status) |
52974 | 169 |
editor.flush() |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
170 |
case None => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
171 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
172 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
173 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
174 |
def locate_query() |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
175 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
176 |
Swing_Thread.require() |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
177 |
|
52980 | 178 |
for { |
179 |
command <- current_location |
|
180 |
snapshot = editor.node_snapshot(command.node_name) |
|
181 |
link <- editor.hyperlink_command(snapshot, command) |
|
182 |
} link.follow(editor_context) |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
183 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
184 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
185 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
186 |
/* main actor */ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
187 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
188 |
private val main_actor = actor { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
189 |
loop { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
190 |
react { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
191 |
case changed: Session.Commands_Changed => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
192 |
current_location match { |
52876 | 193 |
case Some(command) |
194 |
if current_update_pending || |
|
53872
6e69f9ca8f1c
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
wenzelm
parents:
53844
diff
changeset
|
195 |
(current_status != Query_Operation.Status.REMOVED && |
52935 | 196 |
changed.commands.contains(command)) => |
52877 | 197 |
Swing_Thread.later { content_update() } |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
198 |
case _ => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
199 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
200 |
case bad => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
201 |
java.lang.System.err.println("Query_Operation: ignoring bad message " + bad) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
202 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
203 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
204 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
205 |
|
53840 | 206 |
def activate() { |
207 |
editor.session.commands_changed += main_actor |
|
208 |
} |
|
53000 | 209 |
|
210 |
def deactivate() { |
|
211 |
editor.session.commands_changed -= main_actor |
|
212 |
remove_overlay() |
|
54327
148903e47b26
more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
wenzelm
parents:
54325
diff
changeset
|
213 |
reset_state() |
148903e47b26
more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
wenzelm
parents:
54325
diff
changeset
|
214 |
consume_output(Document.Snapshot.init, Command.Results.empty, Nil) |
148903e47b26
more consistent state and GUI update, e.g. relevant for full-screen mode switch with its exit/init side-effect;
wenzelm
parents:
54325
diff
changeset
|
215 |
consume_status(current_status) |
53000 | 216 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
217 |
} |