--- a/src/Pure/PIDE/query_operation.scala Mon Nov 02 16:03:03 2015 +0100
+++ b/src/Pure/PIDE/query_operation.scala Mon Nov 02 18:09:14 2015 +0100
@@ -16,6 +16,26 @@
val RUNNING = Value("running")
val FINISHED = Value("finished")
}
+
+ object State
+ {
+ val empty: State = State()
+
+ def make(command: Command, query: List[String]): State =
+ State(instance = Document_ID.make().toString,
+ location = Some(command),
+ query = query,
+ status = Status.WAITING)
+ }
+
+ sealed case class State(
+ instance: String = Document_ID.none.toString,
+ location: Option[Command] = None,
+ query: List[String] = Nil,
+ update_pending: Boolean = false,
+ output: List[XML.Tree] = Nil,
+ status: Status.Value = Status.FINISHED,
+ exec_id: Document_ID.Exec = Document_ID.none)
}
class Query_Operation[Editor_Context](
@@ -26,37 +46,19 @@
consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
{
private val print_function = operation_name + "_query"
- private val instance = Document_ID.make().toString
/* implicit state -- owned by GUI thread */
- @volatile private var current_location: Option[Command] = None
- @volatile private var current_query: List[String] = Nil
- @volatile private var current_update_pending = false
- @volatile private var current_output: List[XML.Tree] = Nil
- @volatile private var current_status = Query_Operation.Status.FINISHED
- @volatile private var current_exec_id = Document_ID.none
-
- def get_location: Option[Command] = current_location
+ private val current_state = Synchronized(Query_Operation.State.empty)
- private def reset_state()
- {
- current_location = None
- current_query = Nil
- current_update_pending = false
- current_output = Nil
- current_status = Query_Operation.Status.FINISHED
- current_exec_id = Document_ID.none
- }
+ def get_location: Option[Command] = current_state.value.location
private def remove_overlay()
{
- current_location match {
- case None =>
- case Some(command) =>
- editor.remove_overlay(command, print_function, instance :: current_query)
- editor.flush()
+ val state = current_state.value
+ for (command <- state.location) {
+ editor.remove_overlay(command, print_function, state.instance :: state.query)
}
}
@@ -70,29 +72,31 @@
/* snapshot */
- val (snapshot, command_results, removed) =
- current_location match {
+ val state0 = current_state.value
+
+ val (snapshot, command_results, results, removed) =
+ state0.location match {
case Some(cmd) =>
val snapshot = editor.node_snapshot(cmd.node_name)
val command_results = snapshot.state.command_results(snapshot.version, cmd)
+ val results =
+ (for {
+ (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
+ if props.contains((Markup.INSTANCE, state0.instance))
+ } yield elem).toList
val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
- (snapshot, command_results, removed)
+ (snapshot, command_results, results, removed)
case None =>
- (Document.Snapshot.init, Command.Results.empty, true)
+ (Document.Snapshot.init, Command.Results.empty, Nil, true)
}
- val results =
- (for {
- (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
- if props.contains((Markup.INSTANCE, instance))
- } yield elem).toList
/* resolve sendback: static command id */
def resolve_sendback(body: XML.Body): XML.Body =
{
- current_location match {
+ state0.location match {
case None => body
case Some(command) =>
def resolve(body: XML.Body): XML.Body =
@@ -101,7 +105,7 @@
case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
val props1 =
props.map({
- case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
+ case (Markup.ID, Properties.Value.Long(id)) if id == state0.exec_id =>
(Markup.ID, Properties.Value.Long(command.id))
case p => p
})
@@ -137,30 +141,32 @@
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
Query_Operation.Status.WAITING
+
+ /* state update */
+
if (new_status == Query_Operation.Status.RUNNING)
results.collectFirst(
{
case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
if elem.name == Markup.RUNNING => id
- }).foreach(id => current_exec_id = id)
-
-
- /* state update */
+ }).foreach(id => current_state.change(_.copy(exec_id = id)))
- if (current_output != new_output || current_status != new_status) {
+ if (state0.output != new_output || state0.status != new_status) {
if (snapshot.is_outdated)
- current_update_pending = true
+ current_state.change(_.copy(update_pending = true))
else {
- current_update_pending = false
- if (current_output != new_output && !removed) {
- current_output = new_output
+ current_state.change(_.copy(update_pending = false))
+ if (state0.output != new_output && !removed) {
+ current_state.change(_.copy(output = new_output))
consume_output(snapshot, command_results, new_output)
}
- if (current_status != new_status) {
- current_status = new_status
+ if (state0.status != new_status) {
+ current_state.change(_.copy(status = new_status))
consume_status(new_status)
- if (new_status == Query_Operation.Status.FINISHED)
+ if (new_status == Query_Operation.Status.FINISHED) {
remove_overlay()
+ editor.flush()
+ }
}
}
}
@@ -170,7 +176,7 @@
/* query operations */
def cancel_query(): Unit =
- GUI_Thread.require { editor.session.cancel_exec(current_exec_id) }
+ GUI_Thread.require { editor.session.cancel_exec(current_state.value.exec_id) }
def apply_query(query: List[String])
{
@@ -179,19 +185,18 @@
editor.current_node_snapshot(editor_context) match {
case Some(snapshot) =>
remove_overlay()
- reset_state()
+ current_state.change(_ => Query_Operation.State.empty)
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
if (!snapshot.is_outdated) {
editor.current_command(editor_context, snapshot) match {
case Some(command) =>
- current_location = Some(command)
- current_query = query
- current_status = Query_Operation.Status.WAITING
- editor.insert_overlay(command, print_function, instance :: query)
+ val state = Query_Operation.State.make(command, query)
+ current_state.change(_ => state)
+ editor.insert_overlay(command, print_function, state.instance :: query)
case None =>
}
}
- consume_status(current_status)
+ consume_status(current_state.value.status)
editor.flush()
case None =>
}
@@ -201,8 +206,9 @@
{
GUI_Thread.require {}
+ val state = current_state.value
for {
- command <- current_location
+ command <- state.location
snapshot = editor.node_snapshot(command.node_name)
link <- editor.hyperlink_command(true, snapshot, command)
} link.follow(editor_context)
@@ -214,10 +220,11 @@
private val main =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
case changed =>
- current_location match {
+ val state = current_state.value
+ state.location match {
case Some(command)
- if current_update_pending ||
- (current_status != Query_Operation.Status.FINISHED &&
+ if state.update_pending ||
+ (state.status != Query_Operation.Status.FINISHED &&
changed.commands.contains(command)) =>
GUI_Thread.later { content_update() }
case _ =>
@@ -231,8 +238,8 @@
def deactivate() {
editor.session.commands_changed -= main
remove_overlay()
- reset_state()
+ current_state.change(_ => Query_Operation.State.empty)
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
- consume_status(current_status)
+ consume_status(Query_Operation.Status.FINISHED)
}
}