more explicit status for query operation;
avoid output with outdated snapshot;
animation rate according to status;
added PIDE.document_snapshot convenience -- independent of availability of physical buffer;
--- a/src/Pure/PIDE/markup.scala Tue Aug 06 17:30:09 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Aug 06 21:08:04 2013 +0200
@@ -245,6 +245,8 @@
val FINISHED = "finished"
val FAILED = "failed"
+ val WAITING = "waiting"
+
/* interactive documents */
@@ -283,9 +285,10 @@
val WARNING_MESSAGE = "warning_message"
val ERROR_MESSAGE = "error_message"
- val message: String => String =
+ val messages =
Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
- WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
+ WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
+ val message: String => String = messages.withDefault((s: String) => s)
val Return_Code = new Properties.Int("return_code")
--- a/src/Pure/PIDE/query_operation.ML Tue Aug 06 17:30:09 2013 +0200
+++ b/src/Pure/PIDE/query_operation.ML Tue Aug 06 21:08:04 2013 +0200
@@ -19,11 +19,17 @@
SOME {delay = NONE, pri = 0, persistent = false,
print_fn = fn _ => fn state =>
let
+ fun result s = Output.result [(Markup.instanceN, instance)] s;
+ fun status m = result (Markup.markup_only m);
+
+ val _ = status Markup.running;
val msg = XML.Elem ((Markup.writelnN, []), [XML.Text (f state args)])
handle exn =>
if Exn.is_interrupt exn then reraise exn
else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
- in Output.result [(Markup.instanceN, instance)] (YXML.string_of msg) end}
+ val _ = result (YXML.string_of msg);
+ val _ = status Markup.finished;
+ in () end}
| _ => NONE);
end;
--- a/src/Tools/jEdit/src/plugin.scala Tue Aug 06 17:30:09 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Aug 06 21:08:04 2013 +0200
@@ -50,6 +50,20 @@
/* document model and view */
+ def document_snapshot(name: Document.Node.Name): Document.Snapshot =
+ {
+ Swing_Thread.require()
+
+ JEdit_Lib.jedit_buffer(name.node) match {
+ case Some(buffer) =>
+ document_model(buffer) match {
+ case Some(model) => model.snapshot
+ case None => session.snapshot(name)
+ }
+ case None => session.snapshot(name)
+ }
+ }
+
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
--- a/src/Tools/jEdit/src/query_operation.scala Tue Aug 06 17:30:09 2013 +0200
+++ b/src/Tools/jEdit/src/query_operation.scala Tue Aug 06 21:08:04 2013 +0200
@@ -44,7 +44,7 @@
val animation = new Label
private val animation_icon =
- new AnimatedIcon(passive_icon, active_icons.toArray, 10, animation.peer)
+ new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer)
animation.icon = animation_icon
private def animation_rate(rate: Int)
@@ -61,10 +61,18 @@
private var current_location: Option[Command] = None
private var current_query: List[String] = Nil
- private var current_result = false
- private var current_snapshot = Document.State.init.snapshot()
- private var current_state = Command.empty.init_state
+ private var current_update_pending = false
private var current_output: List[XML.Tree] = Nil
+ private var current_status = Markup.FINISHED
+
+ private def reset_state()
+ {
+ current_location = None
+ current_query = Nil
+ current_update_pending = false
+ current_output = Nil
+ current_status = Markup.FINISHED
+ }
private def remove_overlay()
{
@@ -77,43 +85,72 @@
} model.remove_overlay(command, operation_name, instance :: current_query)
}
- private def handle_result()
+ private def handle_update()
{
Swing_Thread.require()
- val (new_snapshot, new_state) =
- Document_View(view.getTextArea) match {
- case Some(doc_view) =>
- val snapshot = doc_view.model.snapshot()
- current_location match {
- case Some(cmd) =>
- (snapshot, snapshot.state.command_state(snapshot.version, cmd))
- case None =>
- (Document.State.init.snapshot(), Command.empty.init_state)
- }
- case None => (current_snapshot, current_state)
+
+ /* snapshot */
+
+ val (snapshot, state) =
+ current_location match {
+ case Some(cmd) =>
+ val snapshot = PIDE.document_snapshot(cmd.node_name)
+ val state = snapshot.state.command_state(snapshot.version, cmd)
+ (snapshot, state)
+ case None =>
+ (Document.State.init.snapshot(), Command.empty.init_state)
}
+ val results =
+ (for {
+ (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- state.results.entries
+ if props.contains((Markup.INSTANCE, instance))
+ } yield body).toList
+
+
+ /* output */
+
val new_output =
- (for {
- (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
- new_state.results.entries
- if props.contains((Markup.INSTANCE, instance))
- } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
+ for {
+ List(XML.Elem(markup, body)) <- results
+ if Markup.messages.contains(markup.name)
+ }
+ yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
+
+
+ /* status */
- if (new_output != current_output)
- consume_result(new_snapshot, new_state.results, new_output)
+ def status(name: String): Option[String] =
+ results.collectFirst({ case List(XML.Elem(m, _)) if m.name == name => name })
+
+ val new_status =
+ status(Markup.FINISHED) orElse status(Markup.RUNNING) getOrElse Markup.WAITING
+
+
+ /* state update */
- if (!new_output.isEmpty) {
- current_result = true
- animation_rate(0)
- remove_overlay()
- PIDE.flush_buffers()
+ if (current_output != new_output || current_status != new_status) {
+ if (snapshot.is_outdated)
+ current_update_pending = true
+ else {
+ if (current_output != new_output)
+ consume_result(snapshot, state.results, new_output)
+ if (current_status != new_status)
+ new_status match {
+ case Markup.WAITING => animation_rate(5)
+ case Markup.RUNNING => animation_rate(15)
+ case Markup.FINISHED =>
+ animation_rate(0)
+ remove_overlay()
+ PIDE.flush_buffers()
+ case _ =>
+ }
+ current_output = new_output
+ current_status = new_status
+ current_update_pending = false
+ }
}
-
- current_snapshot = new_snapshot
- current_state = new_state
- current_output = new_output
}
def apply_query(query: List[String])
@@ -124,14 +161,14 @@
case Some(doc_view) =>
val snapshot = doc_view.model.snapshot()
remove_overlay()
- current_location = None
- current_query = Nil
- current_result = false
- animation_rate(10)
+ reset_state()
+ animation_rate(0)
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
case Some(command) =>
current_location = Some(command)
current_query = query
+ current_status = Markup.WAITING
+ animation_rate(5)
doc_view.model.insert_overlay(command, operation_name, instance :: query)
case None =>
}
@@ -146,9 +183,10 @@
current_location match {
case Some(command) =>
- val snapshot = PIDE.session.snapshot(command.node_name)
+ val snapshot = PIDE.document_snapshot(command.node_name)
val commands = snapshot.node.commands
if (commands.contains(command)) {
+ // FIXME revert offset (!?)
val sources = commands.iterator.takeWhile(_ != command).map(_.source)
val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
Hyperlink(command.node_name.node, line, column).follow(view)
@@ -165,8 +203,10 @@
react {
case changed: Session.Commands_Changed =>
current_location match {
- case Some(command) if !current_result && changed.commands.contains(command) =>
- Swing_Thread.later { handle_result() }
+ case Some(command)
+ if current_update_pending ||
+ (current_status != Markup.FINISHED && changed.commands.contains(command)) =>
+ Swing_Thread.later { handle_update() }
case _ =>
}
case bad =>