author | wenzelm |
Thu, 03 Apr 2014 21:55:48 +0200 | |
changeset 56395 | 0546e036d1c0 |
parent 56372 | fadb0fef09d7 |
child 56662 | f373fb77e0a4 |
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") |
|
21 |
} |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
22 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
23 |
|
52980 | 24 |
class Query_Operation[Editor_Context]( |
25 |
editor: Editor[Editor_Context], |
|
26 |
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
|
27 |
operation_name: String, |
52935 | 28 |
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
|
29 |
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
|
30 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
31 |
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
|
32 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
33 |
|
52877 | 34 |
/* implicit state -- owned by Swing thread */ |
52874 | 35 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
36 |
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
|
37 |
private var current_query: List[String] = Nil |
52876 | 38 |
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
|
39 |
private var current_output: List[XML.Tree] = Nil |
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
|
40 |
private var current_status = Query_Operation.Status.FINISHED |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
41 |
private var current_exec_id = Document_ID.none |
52876 | 42 |
|
43 |
private def reset_state() |
|
44 |
{ |
|
45 |
current_location = None |
|
46 |
current_query = Nil |
|
47 |
current_update_pending = false |
|
48 |
current_output = Nil |
|
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
|
49 |
current_status = Query_Operation.Status.FINISHED |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
50 |
current_exec_id = Document_ID.none |
52876 | 51 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
52 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
53 |
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
|
54 |
{ |
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
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
61 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
62 |
|
52877 | 63 |
|
64 |
/* content update */ |
|
65 |
||
66 |
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
|
67 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
68 |
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
|
69 |
|
52876 | 70 |
|
71 |
/* snapshot */ |
|
72 |
||
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55618
diff
changeset
|
73 |
val (snapshot, command_results, removed) = |
52876 | 74 |
current_location match { |
75 |
case Some(cmd) => |
|
52974 | 76 |
val snapshot = editor.node_snapshot(cmd.node_name) |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55618
diff
changeset
|
77 |
val command_results = snapshot.state.command_results(snapshot.version, cmd) |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
78 |
val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55618
diff
changeset
|
79 |
(snapshot, command_results, removed) |
52876 | 80 |
case None => |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55618
diff
changeset
|
81 |
(Document.Snapshot.init, Command.Results.empty, 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 |
val results = |
85 |
(for { |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56299
diff
changeset
|
86 |
(_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator |
52876 | 87 |
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
|
88 |
} yield elem).toList |
52876 | 89 |
|
90 |
||
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
|
91 |
/* 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
|
92 |
|
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 |
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
|
94 |
{ |
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 |
current_location match { |
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 |
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
|
97 |
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
|
98 |
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
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
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
|
103 |
props.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 (Markup.ID, Properties.Value.Long(id)) if id == current_exec_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
|
105 |
(Markup.ID, Properties.Value.Long(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
|
106 |
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
|
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 |
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
|
109 |
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
|
110 |
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
|
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 |
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
|
113 |
} |
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 |
} |
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 |
|
52876 | 117 |
/* output */ |
118 |
||
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
119 |
val new_output = |
52876 | 120 |
for { |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
121 |
XML.Elem(_, List(XML.Elem(markup, body))) <- results |
52876 | 122 |
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
|
123 |
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
|
124 |
} yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1) |
52876 | 125 |
|
126 |
||
127 |
/* status */ |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
128 |
|
52935 | 129 |
def get_status(name: String, status: Query_Operation.Status.Value) |
130 |
: 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
|
131 |
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
52876 | 132 |
|
133 |
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
|
134 |
if (removed) Query_Operation.Status.FINISHED |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
135 |
else |
52935 | 136 |
get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse |
137 |
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse |
|
138 |
Query_Operation.Status.WAITING |
|
52876 | 139 |
|
52935 | 140 |
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
|
141 |
results.collectFirst( |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
142 |
{ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
143 |
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
|
144 |
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
|
145 |
}).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
|
146 |
|
52876 | 147 |
|
148 |
/* 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
|
149 |
|
52876 | 150 |
if (current_output != new_output || current_status != new_status) { |
151 |
if (snapshot.is_outdated) |
|
152 |
current_update_pending = true |
|
153 |
else { |
|
52877 | 154 |
current_update_pending = false |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
155 |
if (current_output != new_output && !removed) { |
52877 | 156 |
current_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
|
157 |
consume_output(snapshot, command_results, new_output) |
52877 | 158 |
} |
159 |
if (current_status != new_status) { |
|
160 |
current_status = new_status |
|
52935 | 161 |
consume_status(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
|
162 |
if (new_status == Query_Operation.Status.FINISHED) |
52877 | 163 |
remove_overlay() |
164 |
} |
|
52876 | 165 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
166 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
167 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
168 |
|
52877 | 169 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
170 |
/* query operations */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
171 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
172 |
def cancel_query(): Unit = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
52935
diff
changeset
|
173 |
Swing_Thread.require { editor.session.cancel_exec(current_exec_id) } |
52877 | 174 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
175 |
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
|
176 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
177 |
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
|
178 |
|
52980 | 179 |
editor.current_node_snapshot(editor_context) match { |
52978 | 180 |
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
|
181 |
remove_overlay() |
52876 | 182 |
reset_state() |
52972 | 183 |
consume_output(Document.Snapshot.init, Command.Results.empty, Nil) |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
184 |
if (!snapshot.is_outdated) { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
185 |
editor.current_command(editor_context, snapshot) match { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
186 |
case Some(command) => |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
187 |
current_location = Some(command) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
188 |
current_query = query |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
189 |
current_status = Query_Operation.Status.WAITING |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
190 |
editor.insert_overlay(command, operation_name, instance :: query) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
191 |
case None => |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
192 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
193 |
} |
52935 | 194 |
consume_status(current_status) |
52974 | 195 |
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
|
196 |
case None => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
197 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
198 |
} |
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 |
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
|
201 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
202 |
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
|
203 |
|
52980 | 204 |
for { |
205 |
command <- current_location |
|
206 |
snapshot = editor.node_snapshot(command.node_name) |
|
207 |
link <- editor.hyperlink_command(snapshot, command) |
|
208 |
} 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
|
209 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
210 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
211 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
212 |
/* main actor */ |
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 |
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
|
215 |
loop { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
216 |
react { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
217 |
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
|
218 |
current_location match { |
52876 | 219 |
case Some(command) |
220 |
if current_update_pending || |
|
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
|
221 |
(current_status != Query_Operation.Status.FINISHED && |
52935 | 222 |
changed.commands.contains(command)) => |
52877 | 223 |
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
|
224 |
case _ => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
225 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
226 |
case bad => |
55618 | 227 |
System.err.println("Query_Operation: ignoring bad message " + bad) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
228 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
229 |
} |
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() { |
233 |
editor.session.commands_changed += main_actor |
|
234 |
} |
|
53000 | 235 |
|
236 |
def deactivate() { |
|
237 |
editor.session.commands_changed -= main_actor |
|
238 |
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
|
239 |
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
|
240 |
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
|
241 |
consume_status(current_status) |
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 |
} |