author | wenzelm |
Thu, 06 Jun 2024 11:53:52 +0200 | |
changeset 80266 | d52be75ae60b |
parent 78595 | b0abf5a9dada |
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 |
|
75393 | 11 |
object Query_Operation { |
78595 | 12 |
enum Status { case waiting, running, finished } |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
13 |
|
75393 | 14 |
object State { |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
15 |
val empty: State = State() |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
16 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
17 |
def make(command: Command, query: List[String]): State = |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
18 |
State(instance = Document_ID.make().toString, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
19 |
location = Some(command), |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
20 |
query = query, |
78595 | 21 |
status = Status.waiting) |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
22 |
} |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
23 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
24 |
sealed case class State( |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
25 |
instance: String = Document_ID.none.toString, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
26 |
location: Option[Command] = None, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
27 |
query: List[String] = Nil, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
28 |
update_pending: Boolean = false, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
29 |
output: List[XML.Tree] = Nil, |
78595 | 30 |
status: Status = Status.finished, |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
31 |
exec_id: Document_ID.Exec = Document_ID.none) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
32 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
33 |
|
52980 | 34 |
class Query_Operation[Editor_Context]( |
35 |
editor: Editor[Editor_Context], |
|
36 |
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
|
37 |
operation_name: String, |
78595 | 38 |
consume_status: Query_Operation.Status => Unit, |
75393 | 39 |
consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit |
40 |
) { |
|
61206
d5aeb401111a
more specific name to reduce danger of clash with direct uses of plain Command.print_function;
wenzelm
parents:
60893
diff
changeset
|
41 |
private val print_function = operation_name + "_query" |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
42 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
43 |
|
66094 | 44 |
/* implicit state -- owned by editor thread */ |
52874 | 45 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
46 |
private val current_state = Synchronized(Query_Operation.State.empty) |
61210 | 47 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
48 |
def get_location: Option[Command] = current_state.value.location |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
49 |
|
75393 | 50 |
private def remove_overlay(): Unit = { |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
51 |
val state = current_state.value |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
52 |
for (command <- state.location) { |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
53 |
editor.remove_overlay(command, print_function, state.instance :: state.query) |
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
|
54 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
55 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
56 |
|
52877 | 57 |
|
58 |
/* content update */ |
|
59 |
||
75393 | 60 |
private def content_update(): Unit = { |
66094 | 61 |
editor.require_dispatcher {} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
62 |
|
52876 | 63 |
|
64 |
/* snapshot */ |
|
65 |
||
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
66 |
val state0 = current_state.value |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
67 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
68 |
val (snapshot, command_results, results, removed) = |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
69 |
state0.location match { |
52876 | 70 |
case Some(cmd) => |
52974 | 71 |
val snapshot = editor.node_snapshot(cmd.node_name) |
65195 | 72 |
val command_results = snapshot.command_results(cmd) |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
73 |
val results = |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
74 |
(for { |
78592 | 75 |
case (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
76 |
if props.contains((Markup.INSTANCE, state0.instance)) |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
77 |
} yield elem).toList |
72823 | 78 |
val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd) |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
79 |
(snapshot, command_results, results, removed) |
52876 | 80 |
case None => |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
81 |
(Document.Snapshot.init, Command.Results.empty, Nil, true) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
82 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
83 |
|
52876 | 84 |
|
85 |
||
54640
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
86 |
/* resolve sendback: static command id */ |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
87 |
|
75393 | 88 |
def resolve_sendback(body: XML.Body): XML.Body = { |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
89 |
state0.location match { |
54640
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
90 |
case None => body |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
91 |
case Some(command) => |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
92 |
def resolve(body: XML.Body): XML.Body = |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
93 |
body map { |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
94 |
case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2)) |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
95 |
case XML.Elem(Markup(Markup.SENDBACK, props), b) => |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
96 |
val props1 = |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
97 |
props.map({ |
63805 | 98 |
case (Markup.ID, Value.Long(id)) if id == state0.exec_id => |
99 |
(Markup.ID, Value.Long(command.id)) |
|
54640
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
100 |
case p => p |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
101 |
}) |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
102 |
XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b)) |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
103 |
case XML.Elem(m, b) => XML.Elem(m, resolve(b)) |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
104 |
case t => t |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
105 |
} |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
106 |
resolve(body) |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
107 |
} |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
108 |
} |
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
109 |
|
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
110 |
|
52876 | 111 |
/* output */ |
112 |
||
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
113 |
val new_output = |
52876 | 114 |
for { |
78592 | 115 |
case XML.Elem(_, List(XML.Elem(markup, body))) <- results |
52876 | 116 |
if Markup.messages.contains(markup.name) |
54640
bbd2fa353809
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents:
54327
diff
changeset
|
117 |
body1 = resolve_sendback(body) |
76680 | 118 |
} yield Protocol.make_message(body1, markup.name, props = markup.properties) |
52876 | 119 |
|
120 |
||
121 |
/* status */ |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
122 |
|
78595 | 123 |
def get_status(name: String, status: Query_Operation.Status): Option[Query_Operation.Status] = |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
124 |
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
52876 | 125 |
|
126 |
val new_status = |
|
78595 | 127 |
if (removed) Query_Operation.Status.finished |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
128 |
else |
78595 | 129 |
get_status(Markup.FINISHED, Query_Operation.Status.finished) orElse |
130 |
get_status(Markup.RUNNING, Query_Operation.Status.running) getOrElse |
|
131 |
Query_Operation.Status.waiting |
|
52876 | 132 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
133 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
134 |
/* state update */ |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
135 |
|
78595 | 136 |
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
|
137 |
results.collectFirst( |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
138 |
{ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
139 |
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
|
140 |
if elem.name == Markup.RUNNING => id |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
141 |
}).foreach(id => current_state.change(_.copy(exec_id = id))) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
142 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
143 |
if (state0.output != new_output || state0.status != new_status) { |
52876 | 144 |
if (snapshot.is_outdated) |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
145 |
current_state.change(_.copy(update_pending = true)) |
52876 | 146 |
else { |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
147 |
current_state.change(_.copy(update_pending = false)) |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
148 |
if (state0.output != new_output && !removed) { |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
149 |
current_state.change(_.copy(output = new_output)) |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55618
diff
changeset
|
150 |
consume_output(snapshot, command_results, new_output) |
52877 | 151 |
} |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
152 |
if (state0.status != new_status) { |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
153 |
current_state.change(_.copy(status = new_status)) |
52935 | 154 |
consume_status(new_status) |
78595 | 155 |
if (new_status == Query_Operation.Status.finished) |
52877 | 156 |
remove_overlay() |
157 |
} |
|
52876 | 158 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
159 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
160 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
161 |
|
52877 | 162 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
163 |
/* query operations */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
164 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
165 |
def cancel_query(): Unit = |
66094 | 166 |
editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) } |
52877 | 167 |
|
75393 | 168 |
def apply_query(query: List[String]): Unit = { |
66094 | 169 |
editor.require_dispatcher {} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
170 |
|
52980 | 171 |
editor.current_node_snapshot(editor_context) match { |
52978 | 172 |
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
|
173 |
remove_overlay() |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
174 |
current_state.change(_ => Query_Operation.State.empty) |
52972 | 175 |
consume_output(Document.Snapshot.init, Command.Results.empty, Nil) |
66108
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
176 |
|
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
177 |
editor.current_command(editor_context, snapshot) match { |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
178 |
case Some(command) => |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
179 |
val state = Query_Operation.State.make(command, query) |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
180 |
current_state.change(_ => state) |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
181 |
editor.insert_overlay(command, print_function, state.instance :: query) |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
182 |
case None => |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
183 |
} |
66108
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
184 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
185 |
consume_status(current_state.value.status) |
52974 | 186 |
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
|
187 |
case None => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
188 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
189 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
190 |
|
75393 | 191 |
def locate_query(): Unit = { |
66094 | 192 |
editor.require_dispatcher {} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
193 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
194 |
val state = current_state.value |
52980 | 195 |
for { |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
196 |
command <- state.location |
52980 | 197 |
snapshot = editor.node_snapshot(command.node_name) |
64664 | 198 |
link <- editor.hyperlink_command(true, snapshot, command.id) |
52980 | 199 |
} 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
|
200 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
201 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
202 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
203 |
/* main */ |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
204 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
205 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
206 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
207 |
case changed => |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
208 |
val state = current_state.value |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
209 |
state.location match { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
210 |
case Some(command) |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
211 |
if state.update_pending || |
78595 | 212 |
(state.status != Query_Operation.Status.finished && |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
213 |
changed.commands.contains(command)) => |
66094 | 214 |
editor.send_dispatcher { content_update() } |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
215 |
case _ => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
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 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
218 |
|
75393 | 219 |
def activate(): Unit = { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
220 |
editor.session.commands_changed += main |
53840 | 221 |
} |
53000 | 222 |
|
75393 | 223 |
def deactivate(): Unit = { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
224 |
editor.session.commands_changed -= main |
53000 | 225 |
remove_overlay() |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
226 |
current_state.change(_ => Query_Operation.State.empty) |
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
|
227 |
consume_output(Document.Snapshot.init, Command.Results.empty, Nil) |
78595 | 228 |
consume_status(Query_Operation.Status.finished) |
53000 | 229 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
230 |
} |