author | wenzelm |
Fri, 09 Aug 2013 13:51:34 +0200 | |
changeset 52935 | 6fc13c31c775 |
parent 52934 | bfb6873df88e |
child 52971 | 31926d2c04ee |
permissions | -rw-r--r-- |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/query_operation.scala |
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 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.jedit |
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 isabelle._ |
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 |
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
|
14 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.View |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
16 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
17 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
18 |
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
|
19 |
{ |
52935 | 20 |
object Status extends Enumeration |
21 |
{ |
|
22 |
val WAITING = Value("waiting") |
|
23 |
val RUNNING = Value("running") |
|
24 |
val FINISHED = Value("finished") |
|
25 |
} |
|
26 |
||
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
27 |
def apply( |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
28 |
view: View, |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
29 |
operation_name: String, |
52935 | 30 |
consume_status: Status.Value => Unit, |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
31 |
consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) = |
52935 | 32 |
new Query_Operation(view, operation_name, consume_status, consume_output) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
33 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
34 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
35 |
final class Query_Operation private( |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
36 |
view: View, |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
37 |
operation_name: String, |
52935 | 38 |
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
|
39 |
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
|
40 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
41 |
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
|
42 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
43 |
|
52877 | 44 |
/* implicit state -- owned by Swing thread */ |
52874 | 45 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
46 |
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
|
47 |
private var current_query: List[String] = Nil |
52876 | 48 |
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
|
49 |
private var current_output: List[XML.Tree] = Nil |
52935 | 50 |
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
|
51 |
private var current_exec_id = Document_ID.none |
52876 | 52 |
|
53 |
private def reset_state() |
|
54 |
{ |
|
55 |
current_location = None |
|
56 |
current_query = Nil |
|
57 |
current_update_pending = false |
|
58 |
current_output = Nil |
|
52935 | 59 |
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
|
60 |
current_exec_id = Document_ID.none |
52876 | 61 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
62 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
63 |
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
|
64 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
65 |
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
|
66 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
67 |
for { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
68 |
command <- current_location |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
69 |
buffer <- JEdit_Lib.jedit_buffer(command.node_name.node) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
70 |
model <- PIDE.document_model(buffer) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
71 |
} model.remove_overlay(command, operation_name, instance :: current_query) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
72 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
73 |
|
52877 | 74 |
|
75 |
/* content update */ |
|
76 |
||
77 |
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
|
78 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
79 |
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
|
80 |
|
52876 | 81 |
|
82 |
/* snapshot */ |
|
83 |
||
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
84 |
val (snapshot, state, removed) = |
52876 | 85 |
current_location match { |
86 |
case Some(cmd) => |
|
87 |
val snapshot = PIDE.document_snapshot(cmd.node_name) |
|
88 |
val state = snapshot.state.command_state(snapshot.version, cmd) |
|
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
89 |
val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) |
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
90 |
(snapshot, state, removed) |
52876 | 91 |
case None => |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
92 |
(Document.State.init.snapshot(), Command.empty.init_state, true) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
93 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
94 |
|
52876 | 95 |
val results = |
96 |
(for { |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
97 |
(_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries |
52876 | 98 |
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
|
99 |
} yield elem).toList |
52876 | 100 |
|
101 |
||
102 |
/* output */ |
|
103 |
||
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
104 |
val new_output = |
52876 | 105 |
for { |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
106 |
XML.Elem(_, List(XML.Elem(markup, body))) <- results |
52876 | 107 |
if Markup.messages.contains(markup.name) |
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
108 |
} yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body) |
52876 | 109 |
|
110 |
||
111 |
/* status */ |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
112 |
|
52935 | 113 |
def get_status(name: String, status: Query_Operation.Status.Value) |
114 |
: 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
|
115 |
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
52876 | 116 |
|
117 |
val new_status = |
|
52935 | 118 |
if (removed) Query_Operation.Status.FINISHED |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
119 |
else |
52935 | 120 |
get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse |
121 |
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse |
|
122 |
Query_Operation.Status.WAITING |
|
52876 | 123 |
|
52935 | 124 |
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
|
125 |
results.collectFirst( |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
126 |
{ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
127 |
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
|
128 |
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
|
129 |
}).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
|
130 |
|
52876 | 131 |
|
132 |
/* 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
|
133 |
|
52876 | 134 |
if (current_output != new_output || current_status != new_status) { |
135 |
if (snapshot.is_outdated) |
|
136 |
current_update_pending = true |
|
137 |
else { |
|
52877 | 138 |
current_update_pending = false |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
139 |
if (current_output != new_output && !removed) { |
52877 | 140 |
current_output = new_output |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
141 |
consume_output(snapshot, state.results, new_output) |
52877 | 142 |
} |
143 |
if (current_status != new_status) { |
|
144 |
current_status = new_status |
|
52935 | 145 |
consume_status(new_status) |
146 |
if (new_status == Query_Operation.Status.FINISHED) { |
|
52877 | 147 |
remove_overlay() |
148 |
PIDE.flush_buffers() |
|
52876 | 149 |
} |
52877 | 150 |
} |
52876 | 151 |
} |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
152 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
153 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
154 |
|
52877 | 155 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
156 |
/* query operations */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
157 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
158 |
def cancel_query(): Unit = |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52890
diff
changeset
|
159 |
Swing_Thread.require { PIDE.session.cancel_exec(current_exec_id) } |
52877 | 160 |
|
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
161 |
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
|
162 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
163 |
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
|
164 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
165 |
Document_View(view.getTextArea) match { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
166 |
case Some(doc_view) => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
167 |
val snapshot = doc_view.model.snapshot() |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
168 |
remove_overlay() |
52876 | 169 |
reset_state() |
52932
eb7d7c0034b5
removed command location is considered finished, and its overlay removed eventually;
wenzelm
parents:
52931
diff
changeset
|
170 |
consume_output(Document.State.init.snapshot(), Command.Results.empty, Nil) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
171 |
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
172 |
case Some(command) => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
173 |
current_location = Some(command) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
174 |
current_query = query |
52935 | 175 |
current_status = Query_Operation.Status.WAITING |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
176 |
doc_view.model.insert_overlay(command, operation_name, instance :: query) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
177 |
case None => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
178 |
} |
52935 | 179 |
consume_status(current_status) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
180 |
PIDE.flush_buffers() |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
181 |
case None => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
182 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
183 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
184 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
185 |
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
|
186 |
{ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
187 |
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
|
188 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
189 |
current_location match { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
190 |
case Some(command) => |
52876 | 191 |
val snapshot = PIDE.document_snapshot(command.node_name) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
192 |
val commands = snapshot.node.commands |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
193 |
if (commands.contains(command)) { |
52876 | 194 |
// FIXME revert offset (!?) |
52865
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
195 |
val sources = commands.iterator.takeWhile(_ != command).map(_.source) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
196 |
val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
197 |
Hyperlink(command.node_name.node, line, column).follow(view) |
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 |
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 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
204 |
/* main actor */ |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
205 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
206 |
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
|
207 |
loop { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
208 |
react { |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
209 |
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
|
210 |
current_location match { |
52876 | 211 |
case Some(command) |
212 |
if current_update_pending || |
|
52935 | 213 |
(current_status != Query_Operation.Status.FINISHED && |
214 |
changed.commands.contains(command)) => |
|
52877 | 215 |
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
|
216 |
case _ => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
217 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
218 |
case bad => |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
219 |
java.lang.System.err.println("Query_Operation: ignoring bad message " + bad) |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
220 |
} |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
221 |
} |
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 |
|
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
224 |
def activate() { PIDE.session.commands_changed += main_actor } |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
225 |
def deactivate() { PIDE.session.commands_changed -= main_actor } |
02a7e7180ee5
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents:
diff
changeset
|
226 |
} |