# HG changeset patch # User wenzelm # Date 1375816084 -7200 # Node ID 78989972d5b854f77d3c88c07f76f9b92c21112e # Parent e2d5c3ff5c3f3cd985a0df531b2be7292eb486ca 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; diff -r e2d5c3ff5c3f -r 78989972d5b8 src/Pure/PIDE/markup.scala --- 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") diff -r e2d5c3ff5c3f -r 78989972d5b8 src/Pure/PIDE/query_operation.ML --- 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; diff -r e2d5c3ff5c3f -r 78989972d5b8 src/Tools/jEdit/src/plugin.scala --- 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) diff -r e2d5c3ff5c3f -r 78989972d5b8 src/Tools/jEdit/src/query_operation.scala --- 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 =>