back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
resolve sendback wrt. static command id, to allow active area even after exec_id is removed (cf. prune_delay);
--- a/src/Pure/PIDE/query_operation.scala Wed Nov 20 23:00:18 2013 +0100
+++ b/src/Pure/PIDE/query_operation.scala Thu Nov 21 21:55:29 2013 +0100
@@ -18,7 +18,6 @@
val WAITING = Value("waiting")
val RUNNING = Value("running")
val FINISHED = Value("finished")
- val REMOVED = Value("removed")
}
}
@@ -38,7 +37,7 @@
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.REMOVED
+ private var current_status = Query_Operation.Status.FINISHED
private var current_exec_id = Document_ID.none
private def reset_state()
@@ -47,7 +46,7 @@
current_query = Nil
current_update_pending = false
current_output = Nil
- current_status = Query_Operation.Status.REMOVED
+ current_status = Query_Operation.Status.FINISHED
current_exec_id = Document_ID.none
}
@@ -89,13 +88,40 @@
} yield elem).toList
+ /* resolve sendback: static command id */
+
+ def resolve_sendback(body: XML.Body): XML.Body =
+ {
+ current_location match {
+ case None => body
+ case Some(command) =>
+ def resolve(body: XML.Body): XML.Body =
+ body map {
+ case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
+ case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
+ val props1 =
+ props.map({
+ case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
+ (Markup.ID, Properties.Value.Long(command.id))
+ case p => p
+ })
+ XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
+ case XML.Elem(m, b) => XML.Elem(m, resolve(b))
+ case t => t
+ }
+ resolve(body)
+ }
+ }
+
+
/* 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)
+ body1 = resolve_sendback(body)
+ } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
/* status */
@@ -105,7 +131,7 @@
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
val new_status =
- if (removed) Query_Operation.Status.REMOVED
+ 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
@@ -133,7 +159,7 @@
if (current_status != new_status) {
current_status = new_status
consume_status(new_status)
- if (new_status == Query_Operation.Status.REMOVED)
+ if (new_status == Query_Operation.Status.FINISHED)
remove_overlay()
}
}
@@ -192,7 +218,7 @@
current_location match {
case Some(command)
if current_update_pending ||
- (current_status != Query_Operation.Status.REMOVED &&
+ (current_status != Query_Operation.Status.FINISHED &&
changed.commands.contains(command)) =>
Swing_Thread.later { content_update() }
case _ =>
--- a/src/Tools/jEdit/src/active.scala Wed Nov 20 23:00:18 2013 +0100
+++ b/src/Tools/jEdit/src/active.scala Thu Nov 21 21:55:29 2013 +0100
@@ -52,9 +52,9 @@
case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
props match {
- case Position.Id(exec_id) =>
+ case Position.Id(id) =>
Isabelle.edit_command(snapshot, buffer,
- props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
+ props.exists(_ == Markup.PADDING_COMMAND), id, text)
case _ =>
if (props.exists(_ == Markup.PADDING_LINE))
Isabelle.insert_line_padding(text_area, text)
--- a/src/Tools/jEdit/src/find_dockable.scala Wed Nov 20 23:00:18 2013 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala Thu Nov 21 21:55:29 2013 +0100
@@ -37,7 +37,7 @@
process_indicator.update("Waiting for evaluation of context ...", 5)
case Query_Operation.Status.RUNNING =>
process_indicator.update("Running find operation ...", 15)
- case _ =>
+ case Query_Operation.Status.FINISHED =>
process_indicator.update(null, 0)
}
}
--- a/src/Tools/jEdit/src/isabelle.scala Wed Nov 20 23:00:18 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Thu Nov 21 21:55:29 2013 +0100
@@ -177,26 +177,28 @@
snapshot: Document.Snapshot,
buffer: Buffer,
padding: Boolean,
- exec_id: Document_ID.Exec,
+ id: Document_ID.Generic,
s: String)
{
- snapshot.state.execs.get(exec_id).map(_.command) match {
- case Some(command) =>
- snapshot.node.command_start(command) match {
- case Some(start) =>
- JEdit_Lib.buffer_edit(buffer) {
- val range = command.proper_range + start
- if (padding) {
- buffer.insert(start + range.length, "\n" + s)
+ if (!snapshot.is_outdated) {
+ snapshot.state.find_command(snapshot.version, id) match {
+ case Some((node, command)) =>
+ node.command_start(command) match {
+ case Some(start) =>
+ JEdit_Lib.buffer_edit(buffer) {
+ val range = command.proper_range + start
+ if (padding) {
+ buffer.insert(start + range.length, "\n" + s)
+ }
+ else {
+ buffer.remove(start, range.length)
+ buffer.insert(start, s)
+ }
}
- else {
- buffer.remove(start, range.length)
- buffer.insert(start, s)
- }
- }
- case None =>
- }
- case None =>
+ case None =>
+ }
+ case None =>
+ }
}
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Nov 20 23:00:18 2013 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Nov 21 21:55:29 2013 +0100
@@ -38,7 +38,7 @@
process_indicator.update("Waiting for evaluation of context ...", 5)
case Query_Operation.Status.RUNNING =>
process_indicator.update("Sledgehammering ...", 15)
- case _ =>
+ case Query_Operation.Status.FINISHED =>
process_indicator.update(null, 0)
}
}