--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/query_operation.scala Mon Aug 12 17:17:49 2013 +0200
@@ -0,0 +1,203 @@
+/* Title: Pure/PIDE/query_operation.scala
+ Author: Makarius
+
+One-shot query operations via asynchronous print functions and temporary
+document overlays.
+*/
+
+package isabelle
+
+
+import scala.actors.Actor._
+
+
+object Query_Operation
+{
+ object Status extends Enumeration
+ {
+ val WAITING = Value("waiting")
+ val RUNNING = Value("running")
+ val FINISHED = Value("finished")
+ }
+}
+
+class Query_Operation[Editor_Context](
+ editor: Editor[Editor_Context],
+ editor_context: Editor_Context,
+ operation_name: String,
+ consume_status: Query_Operation.Status.Value => Unit,
+ consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
+{
+ private val instance = Document_ID.make().toString
+
+
+ /* implicit state -- owned by Swing thread */
+
+ private var current_location: Option[Command] = None
+ private var current_query: List[String] = Nil
+ private var current_update_pending = false
+ private var current_output: List[XML.Tree] = Nil
+ private var current_status = Query_Operation.Status.FINISHED
+ private var current_exec_id = Document_ID.none
+
+ 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
+ }
+
+ private def remove_overlay()
+ {
+ current_location.foreach(command =>
+ editor.remove_overlay(command, operation_name, instance :: current_query))
+ }
+
+
+ /* content update */
+
+ private def content_update()
+ {
+ Swing_Thread.require()
+
+
+ /* snapshot */
+
+ val (snapshot, state, removed) =
+ current_location match {
+ case Some(cmd) =>
+ val snapshot = editor.node_snapshot(cmd.node_name)
+ val state = snapshot.state.command_state(snapshot.version, cmd)
+ val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
+ (snapshot, state, removed)
+ case None =>
+ (Document.Snapshot.init, Command.empty.init_state, true)
+ }
+
+ val results =
+ (for {
+ (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
+ if props.contains((Markup.INSTANCE, instance))
+ } yield elem).toList
+
+
+ /* output */
+
+ val new_output =
+ for {
+ XML.Elem(_, List(XML.Elem(markup, body))) <- results
+ if Markup.messages.contains(markup.name)
+ } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
+
+
+ /* status */
+
+ def get_status(name: String, status: Query_Operation.Status.Value)
+ : Option[Query_Operation.Status.Value] =
+ results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
+
+ val new_status =
+ if (removed) Query_Operation.Status.FINISHED
+ else
+ get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
+ get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
+ Query_Operation.Status.WAITING
+
+ 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 */
+
+ if (current_output != new_output || current_status != new_status) {
+ if (snapshot.is_outdated)
+ current_update_pending = true
+ else {
+ current_update_pending = false
+ if (current_output != new_output && !removed) {
+ current_output = new_output
+ consume_output(snapshot, state.results, new_output)
+ }
+ if (current_status != new_status) {
+ current_status = new_status
+ consume_status(new_status)
+ if (new_status == Query_Operation.Status.FINISHED) {
+ remove_overlay()
+ editor.flush()
+ }
+ }
+ }
+ }
+ }
+
+
+ /* query operations */
+
+ def cancel_query(): Unit =
+ Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
+
+ def apply_query(query: List[String])
+ {
+ Swing_Thread.require()
+
+ editor.current_node_snapshot(editor_context) match {
+ case Some(snapshot) =>
+ remove_overlay()
+ reset_state()
+ consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+ 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, operation_name, instance :: query)
+ case None =>
+ }
+ consume_status(current_status)
+ editor.flush()
+ case None =>
+ }
+ }
+
+ def locate_query()
+ {
+ Swing_Thread.require()
+
+ for {
+ command <- current_location
+ snapshot = editor.node_snapshot(command.node_name)
+ link <- editor.hyperlink_command(snapshot, command)
+ } link.follow(editor_context)
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case changed: Session.Commands_Changed =>
+ current_location match {
+ case Some(command)
+ if current_update_pending ||
+ (current_status != Query_Operation.Status.FINISHED &&
+ changed.commands.contains(command)) =>
+ Swing_Thread.later { content_update() }
+ case _ =>
+ }
+ case bad =>
+ java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def activate() { editor.session.commands_changed += main_actor }
+ def deactivate() { editor.session.commands_changed -= main_actor }
+}
--- a/src/Pure/build-jars Mon Aug 12 17:11:27 2013 +0200
+++ b/src/Pure/build-jars Mon Aug 12 17:17:49 2013 +0200
@@ -40,6 +40,7 @@
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
+ PIDE/query_operation.scala
PIDE/text.scala
PIDE/xml.scala
PIDE/yxml.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Aug 12 17:11:27 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Aug 12 17:17:49 2013 +0200
@@ -36,7 +36,6 @@
"src/pretty_tooltip.scala"
"src/process_indicator.scala"
"src/protocol_dockable.scala"
- "src/query_operation.scala"
"src/raw_output_dockable.scala"
"src/readme_dockable.scala"
"src/rendering.scala"
--- a/src/Tools/jEdit/src/query_operation.scala Mon Aug 12 17:11:27 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,205 +0,0 @@
-/* Title: Tools/jEdit/src/query_operation.scala
- Author: Makarius
-
-One-shot query operations via asynchronous print functions and temporary
-document overlays.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import scala.actors.Actor._
-
-
-object Query_Operation
-{
- object Status extends Enumeration
- {
- val WAITING = Value("waiting")
- val RUNNING = Value("running")
- val FINISHED = Value("finished")
- }
-}
-
-class Query_Operation[Editor_Context](
- editor: Editor[Editor_Context],
- editor_context: Editor_Context,
- operation_name: String,
- consume_status: Query_Operation.Status.Value => Unit,
- consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
-{
- private val instance = Document_ID.make().toString
-
-
- /* implicit state -- owned by Swing thread */
-
- private var current_location: Option[Command] = None
- private var current_query: List[String] = Nil
- private var current_update_pending = false
- private var current_output: List[XML.Tree] = Nil
- private var current_status = Query_Operation.Status.FINISHED
- private var current_exec_id = Document_ID.none
-
- 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
- }
-
- private def remove_overlay()
- {
- current_location.foreach(command =>
- editor.remove_overlay(command, operation_name, instance :: current_query))
- }
-
-
- /* content update */
-
- private def content_update()
- {
- Swing_Thread.require()
-
-
- /* snapshot */
-
- val (snapshot, state, removed) =
- current_location match {
- case Some(cmd) =>
- val snapshot = editor.node_snapshot(cmd.node_name)
- val state = snapshot.state.command_state(snapshot.version, cmd)
- val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
- (snapshot, state, removed)
- case None =>
- (Document.Snapshot.init, Command.empty.init_state, true)
- }
-
- val results =
- (for {
- (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
- if props.contains((Markup.INSTANCE, instance))
- } yield elem).toList
-
-
- /* output */
-
- val new_output =
- for {
- XML.Elem(_, List(XML.Elem(markup, body))) <- results
- if Markup.messages.contains(markup.name)
- } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
-
-
- /* status */
-
- def get_status(name: String, status: Query_Operation.Status.Value)
- : Option[Query_Operation.Status.Value] =
- results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
-
- val new_status =
- if (removed) Query_Operation.Status.FINISHED
- else
- get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
- get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
- Query_Operation.Status.WAITING
-
- 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 */
-
- if (current_output != new_output || current_status != new_status) {
- if (snapshot.is_outdated)
- current_update_pending = true
- else {
- current_update_pending = false
- if (current_output != new_output && !removed) {
- current_output = new_output
- consume_output(snapshot, state.results, new_output)
- }
- if (current_status != new_status) {
- current_status = new_status
- consume_status(new_status)
- if (new_status == Query_Operation.Status.FINISHED) {
- remove_overlay()
- editor.flush()
- }
- }
- }
- }
- }
-
-
- /* query operations */
-
- def cancel_query(): Unit =
- Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
-
- def apply_query(query: List[String])
- {
- Swing_Thread.require()
-
- editor.current_node_snapshot(editor_context) match {
- case Some(snapshot) =>
- remove_overlay()
- reset_state()
- consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
- 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, operation_name, instance :: query)
- case None =>
- }
- consume_status(current_status)
- editor.flush()
- case None =>
- }
- }
-
- def locate_query()
- {
- Swing_Thread.require()
-
- for {
- command <- current_location
- snapshot = editor.node_snapshot(command.node_name)
- link <- editor.hyperlink_command(snapshot, command)
- } link.follow(editor_context)
- }
-
-
- /* main actor */
-
- private val main_actor = actor {
- loop {
- react {
- case changed: Session.Commands_Changed =>
- current_location match {
- case Some(command)
- if current_update_pending ||
- (current_status != Query_Operation.Status.FINISHED &&
- changed.commands.contains(command)) =>
- Swing_Thread.later { content_update() }
- case _ =>
- }
- case bad =>
- java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
- }
- }
- }
-
- def activate() { editor.session.commands_changed += main_actor }
- def deactivate() { editor.session.commands_changed -= main_actor }
-}