author | paulson <lp15@cam.ac.uk> |
Wed, 18 Mar 2015 14:13:27 +0000 | |
changeset 59741 | 5b762cd73a8e |
parent 57612 | 990ffb84489b |
child 60893 | 3c8b9b4b577c |
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 |
} |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
19 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
20 |
|
52980 | 21 |
class Query_Operation[Editor_Context]( |
22 |
editor: Editor[Editor_Context], |
|
23 |
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
|
24 |
operation_name: String, |
52935 | 25 |
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
|
26 |
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
|
27 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
28 |
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
|
29 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
30 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
31 |
/* implicit state -- owned by GUI thread */ |
52874 | 32 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
33 |
@volatile private var current_location: Option[Command] = None |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
34 |
@volatile private var current_query: List[String] = Nil |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
35 |
@volatile private var current_update_pending = false |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
36 |
@volatile private var current_output: List[XML.Tree] = Nil |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
37 |
@volatile private var current_status = Query_Operation.Status.FINISHED |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
38 |
@volatile private var current_exec_id = Document_ID.none |
52876 | 39 |
|
40 |
private def reset_state() |
|
41 |
{ |
|
42 |
current_location = None |
|
43 |
current_query = Nil |
|
44 |
current_update_pending = false |
|
45 |
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
|
46 |
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
|
47 |
current_exec_id = Document_ID.none |
52876 | 48 |
} |
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 |
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
|
51 |
{ |
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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
58 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
59 |
|
52877 | 60 |
|
61 |
/* content update */ |
|
62 |
||
63 |
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
|
64 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
65 |
GUI_Thread.require {} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
66 |
|
52876 | 67 |
|
68 |
/* snapshot */ |
|
69 |
||
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55618
diff
changeset
|
70 |
val (snapshot, command_results, removed) = |
52876 | 71 |
current_location match { |
72 |
case Some(cmd) => |
|
52974 | 73 |
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
|
74 |
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
|
75 |
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
|
76 |
(snapshot, command_results, removed) |
52876 | 77 |
case None => |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55618
diff
changeset
|
78 |
(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
|
79 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
80 |
|
52876 | 81 |
val results = |
82 |
(for { |
|
56372
fadb0fef09d7
more explicit iterator terminology, in accordance to Scala 2.8 library;
wenzelm
parents:
56299
diff
changeset
|
83 |
(_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator |
52876 | 84 |
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
|
85 |
} yield elem).toList |
52876 | 86 |
|
87 |
||
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
|
88 |
/* 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
|
89 |
|
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 |
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
|
91 |
{ |
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 |
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
|
93 |
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
|
94 |
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
|
95 |
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
|
96 |
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
|
97 |
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
|
98 |
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
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
(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
|
103 |
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
|
104 |
}) |
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 |
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
|
106 |
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
|
107 |
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
|
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 |
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
|
110 |
} |
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 |
|
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 |
|
52876 | 114 |
/* output */ |
115 |
||
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
116 |
val new_output = |
52876 | 117 |
for { |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
118 |
XML.Elem(_, List(XML.Elem(markup, body))) <- results |
52876 | 119 |
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
|
120 |
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
|
121 |
} yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1) |
52876 | 122 |
|
123 |
||
124 |
/* status */ |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
125 |
|
52935 | 126 |
def get_status(name: String, status: Query_Operation.Status.Value) |
127 |
: 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
|
128 |
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
52876 | 129 |
|
130 |
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
|
131 |
if (removed) Query_Operation.Status.FINISHED |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
132 |
else |
52935 | 133 |
get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse |
134 |
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse |
|
135 |
Query_Operation.Status.WAITING |
|
52876 | 136 |
|
52935 | 137 |
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
|
138 |
results.collectFirst( |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
139 |
{ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
140 |
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
|
141 |
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
|
142 |
}).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
|
143 |
|
52876 | 144 |
|
145 |
/* 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
|
146 |
|
52876 | 147 |
if (current_output != new_output || current_status != new_status) { |
148 |
if (snapshot.is_outdated) |
|
149 |
current_update_pending = true |
|
150 |
else { |
|
52877 | 151 |
current_update_pending = false |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
152 |
if (current_output != new_output && !removed) { |
52877 | 153 |
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
|
154 |
consume_output(snapshot, command_results, new_output) |
52877 | 155 |
} |
156 |
if (current_status != new_status) { |
|
157 |
current_status = new_status |
|
52935 | 158 |
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
|
159 |
if (new_status == Query_Operation.Status.FINISHED) |
52877 | 160 |
remove_overlay() |
161 |
} |
|
52876 | 162 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
163 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
164 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
165 |
|
52877 | 166 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
167 |
/* query operations */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
168 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
169 |
def cancel_query(): Unit = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
170 |
GUI_Thread.require { editor.session.cancel_exec(current_exec_id) } |
52877 | 171 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
172 |
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
|
173 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
174 |
GUI_Thread.require {} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
175 |
|
52980 | 176 |
editor.current_node_snapshot(editor_context) match { |
52978 | 177 |
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
|
178 |
remove_overlay() |
52876 | 179 |
reset_state() |
52972 | 180 |
consume_output(Document.Snapshot.init, Command.Results.empty, Nil) |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
181 |
if (!snapshot.is_outdated) { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
182 |
editor.current_command(editor_context, snapshot) match { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
183 |
case Some(command) => |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
184 |
current_location = Some(command) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
185 |
current_query = query |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
186 |
current_status = Query_Operation.Status.WAITING |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
187 |
editor.insert_overlay(command, operation_name, instance :: query) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
188 |
case None => |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
54310
diff
changeset
|
189 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
190 |
} |
52935 | 191 |
consume_status(current_status) |
52974 | 192 |
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
|
193 |
case None => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
194 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
195 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
196 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
197 |
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
|
198 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
199 |
GUI_Thread.require {} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
200 |
|
52980 | 201 |
for { |
202 |
command <- current_location |
|
203 |
snapshot = editor.node_snapshot(command.node_name) |
|
204 |
link <- editor.hyperlink_command(snapshot, command) |
|
205 |
} 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
|
206 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
207 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
208 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
209 |
/* main */ |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
210 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
211 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
212 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
213 |
case changed => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
214 |
current_location match { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
215 |
case Some(command) |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
216 |
if current_update_pending || |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
217 |
(current_status != Query_Operation.Status.FINISHED && |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
218 |
changed.commands.contains(command)) => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
219 |
GUI_Thread.later { content_update() } |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
220 |
case _ => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
221 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
222 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
223 |
|
53840 | 224 |
def activate() { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
225 |
editor.session.commands_changed += main |
53840 | 226 |
} |
53000 | 227 |
|
228 |
def deactivate() { |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
229 |
editor.session.commands_changed -= main |
53000 | 230 |
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
|
231 |
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
|
232 |
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
|
233 |
consume_status(current_status) |
53000 | 234 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
235 |
} |