# HG changeset patch # User wenzelm # Date 1446484154 -3600 # Node ID 57000ac6291fecc69a030a19a8882b045312f6dd # Parent 19d84de5f534c14a7ac4aa8a62d623a7c5df1913 clarified Query_Operation.State, with separate instance to avoid extra flush (see also 6ddeb83eb67a); diff -r 19d84de5f534 -r 57000ac6291f src/Pure/PIDE/query_operation.scala --- 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) } }