author | wenzelm |
Sun, 29 Nov 2020 15:44:53 +0100 | |
changeset 72776 | 27a464537fb0 |
parent 66108 | 8b433b6f302f |
child 72823 | ab1a49ac456b |
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 |
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
|
12 |
{ |
52935 | 13 |
object Status extends Enumeration |
14 |
{ |
|
15 |
val WAITING = Value("waiting") |
|
16 |
val RUNNING = Value("running") |
|
17 |
val FINISHED = Value("finished") |
|
18 |
} |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
19 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
20 |
object State |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
21 |
{ |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
22 |
val empty: State = State() |
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 |
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
|
25 |
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
|
26 |
location = Some(command), |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
27 |
query = query, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
28 |
status = Status.WAITING) |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
29 |
} |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
30 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
31 |
sealed case class State( |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
32 |
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
|
33 |
location: Option[Command] = None, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
34 |
query: List[String] = Nil, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
35 |
update_pending: Boolean = false, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
36 |
output: List[XML.Tree] = Nil, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
37 |
status: Status.Value = Status.FINISHED, |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
38 |
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
|
39 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
40 |
|
52980 | 41 |
class Query_Operation[Editor_Context]( |
42 |
editor: Editor[Editor_Context], |
|
43 |
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
|
44 |
operation_name: String, |
52935 | 45 |
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
|
46 |
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
|
47 |
{ |
61206
d5aeb401111a
more specific name to reduce danger of clash with direct uses of plain Command.print_function;
wenzelm
parents:
60893
diff
changeset
|
48 |
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
|
49 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
50 |
|
66094 | 51 |
/* implicit state -- owned by editor thread */ |
52874 | 52 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
53 |
private val current_state = Synchronized(Query_Operation.State.empty) |
61210 | 54 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
55 |
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
|
56 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
57 |
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
|
58 |
{ |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
59 |
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
|
60 |
for (command <- state.location) { |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
61 |
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
|
62 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
63 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
64 |
|
52877 | 65 |
|
66 |
/* content update */ |
|
67 |
||
68 |
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
|
69 |
{ |
66094 | 70 |
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
|
71 |
|
52876 | 72 |
|
73 |
/* snapshot */ |
|
74 |
||
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
75 |
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
|
76 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
77 |
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
|
78 |
state0.location match { |
52876 | 79 |
case Some(cmd) => |
52974 | 80 |
val snapshot = editor.node_snapshot(cmd.node_name) |
65195 | 81 |
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
|
82 |
val results = |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
83 |
(for { |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
84 |
(_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
85 |
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
|
86 |
} yield elem).toList |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
87 |
val removed = !snapshot.version.nodes(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
|
88 |
(snapshot, command_results, results, removed) |
52876 | 89 |
case None => |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
90 |
(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
|
91 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
92 |
|
52876 | 93 |
|
94 |
||
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
|
95 |
/* 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
|
96 |
|
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 |
def resolve_sendback(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
|
98 |
{ |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
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
|
103 |
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
|
104 |
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
|
105 |
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
|
106 |
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
|
107 |
props.map({ |
63805 | 108 |
case (Markup.ID, Value.Long(id)) if id == state0.exec_id => |
109 |
(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
|
110 |
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
|
111 |
}) |
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
|
112 |
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
|
113 |
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
|
114 |
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
|
115 |
} |
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
|
116 |
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
|
117 |
} |
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
|
118 |
} |
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
|
119 |
|
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
|
120 |
|
52876 | 121 |
/* output */ |
122 |
||
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
123 |
val new_output = |
52876 | 124 |
for { |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
125 |
XML.Elem(_, List(XML.Elem(markup, body))) <- results |
52876 | 126 |
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
|
127 |
body1 = resolve_sendback(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
|
128 |
} yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1) |
52876 | 129 |
|
130 |
||
131 |
/* status */ |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
132 |
|
52935 | 133 |
def get_status(name: String, status: Query_Operation.Status.Value) |
134 |
: 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
|
135 |
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
52876 | 136 |
|
137 |
val new_status = |
|
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
|
138 |
if (removed) Query_Operation.Status.FINISHED |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
139 |
else |
52935 | 140 |
get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse |
141 |
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse |
|
142 |
Query_Operation.Status.WAITING |
|
52876 | 143 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
144 |
|
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
145 |
/* state update */ |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
146 |
|
52935 | 147 |
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
|
148 |
results.collectFirst( |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
149 |
{ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
150 |
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
|
151 |
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
|
152 |
}).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
|
153 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
154 |
if (state0.output != new_output || state0.status != new_status) { |
52876 | 155 |
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
|
156 |
current_state.change(_.copy(update_pending = true)) |
52876 | 157 |
else { |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
consume_output(snapshot, command_results, new_output) |
52877 | 162 |
} |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
163 |
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
|
164 |
current_state.change(_.copy(status = new_status)) |
52935 | 165 |
consume_status(new_status) |
61547
8494a947fa65
avoid premature flushing and thus flashing of text area;
wenzelm
parents:
61545
diff
changeset
|
166 |
if (new_status == Query_Operation.Status.FINISHED) |
52877 | 167 |
remove_overlay() |
168 |
} |
|
52876 | 169 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
170 |
} |
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 |
|
52877 | 173 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
174 |
/* query operations */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
175 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
176 |
def cancel_query(): Unit = |
66094 | 177 |
editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) } |
52877 | 178 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
179 |
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
|
180 |
{ |
66094 | 181 |
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
|
182 |
|
52980 | 183 |
editor.current_node_snapshot(editor_context) match { |
52978 | 184 |
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
|
185 |
remove_overlay() |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
186 |
current_state.change(_ => Query_Operation.State.empty) |
52972 | 187 |
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
|
188 |
|
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
189 |
editor.current_command(editor_context, snapshot) match { |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
190 |
case Some(command) => |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
191 |
val state = Query_Operation.State.make(command, query) |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
192 |
current_state.change(_ => state) |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
193 |
editor.insert_overlay(command, print_function, state.instance :: query) |
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
194 |
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
|
195 |
} |
66108
8b433b6f302f
more permissive: avoid situations where query is silently ignored;
wenzelm
parents:
66094
diff
changeset
|
196 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
197 |
consume_status(current_state.value.status) |
52974 | 198 |
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
|
199 |
case None => |
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 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
203 |
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
|
204 |
{ |
66094 | 205 |
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
|
206 |
|
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
207 |
val state = current_state.value |
52980 | 208 |
for { |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
209 |
command <- state.location |
52980 | 210 |
snapshot = editor.node_snapshot(command.node_name) |
64664 | 211 |
link <- editor.hyperlink_command(true, snapshot, command.id) |
52980 | 212 |
} 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
|
213 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
214 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
215 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
216 |
/* main */ |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
217 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
218 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
219 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
220 |
case changed => |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
221 |
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
|
222 |
state.location match { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
223 |
case Some(command) |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
224 |
if state.update_pending || |
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
225 |
(state.status != Query_Operation.Status.FINISHED && |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
226 |
changed.commands.contains(command)) => |
66094 | 227 |
editor.send_dispatcher { content_update() } |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
228 |
case _ => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
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 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
231 |
|
53840 | 232 |
def activate() { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
233 |
editor.session.commands_changed += main |
53840 | 234 |
} |
53000 | 235 |
|
236 |
def deactivate() { |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
237 |
editor.session.commands_changed -= main |
53000 | 238 |
remove_overlay() |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
239 |
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
|
240 |
consume_output(Document.Snapshot.init, Command.Results.empty, Nil) |
61545
57000ac6291f
clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a);
wenzelm
parents:
61210
diff
changeset
|
241 |
consume_status(Query_Operation.Status.FINISHED) |
53000 | 242 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
243 |
} |