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);
1.1 --- a/src/Pure/PIDE/query_operation.scala Wed Nov 20 23:00:18 2013 +0100
1.2 +++ b/src/Pure/PIDE/query_operation.scala Thu Nov 21 21:55:29 2013 +0100
1.3 @@ -18,7 +18,6 @@
1.4 val WAITING = Value("waiting")
1.5 val RUNNING = Value("running")
1.6 val FINISHED = Value("finished")
1.7 - val REMOVED = Value("removed")
1.8 }
1.9 }
1.10
1.11 @@ -38,7 +37,7 @@
1.12 private var current_query: List[String] = Nil
1.13 private var current_update_pending = false
1.14 private var current_output: List[XML.Tree] = Nil
1.15 - private var current_status = Query_Operation.Status.REMOVED
1.16 + private var current_status = Query_Operation.Status.FINISHED
1.17 private var current_exec_id = Document_ID.none
1.18
1.19 private def reset_state()
1.20 @@ -47,7 +46,7 @@
1.21 current_query = Nil
1.22 current_update_pending = false
1.23 current_output = Nil
1.24 - current_status = Query_Operation.Status.REMOVED
1.25 + current_status = Query_Operation.Status.FINISHED
1.26 current_exec_id = Document_ID.none
1.27 }
1.28
1.29 @@ -89,13 +88,40 @@
1.30 } yield elem).toList
1.31
1.32
1.33 + /* resolve sendback: static command id */
1.34 +
1.35 + def resolve_sendback(body: XML.Body): XML.Body =
1.36 + {
1.37 + current_location match {
1.38 + case None => body
1.39 + case Some(command) =>
1.40 + def resolve(body: XML.Body): XML.Body =
1.41 + body map {
1.42 + case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2))
1.43 + case XML.Elem(Markup(Markup.SENDBACK, props), b) =>
1.44 + val props1 =
1.45 + props.map({
1.46 + case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id =>
1.47 + (Markup.ID, Properties.Value.Long(command.id))
1.48 + case p => p
1.49 + })
1.50 + XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b))
1.51 + case XML.Elem(m, b) => XML.Elem(m, resolve(b))
1.52 + case t => t
1.53 + }
1.54 + resolve(body)
1.55 + }
1.56 + }
1.57 +
1.58 +
1.59 /* output */
1.60
1.61 val new_output =
1.62 for {
1.63 XML.Elem(_, List(XML.Elem(markup, body))) <- results
1.64 if Markup.messages.contains(markup.name)
1.65 - } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
1.66 + body1 = resolve_sendback(body)
1.67 + } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1)
1.68
1.69
1.70 /* status */
1.71 @@ -105,7 +131,7 @@
1.72 results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
1.73
1.74 val new_status =
1.75 - if (removed) Query_Operation.Status.REMOVED
1.76 + if (removed) Query_Operation.Status.FINISHED
1.77 else
1.78 get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
1.79 get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
1.80 @@ -133,7 +159,7 @@
1.81 if (current_status != new_status) {
1.82 current_status = new_status
1.83 consume_status(new_status)
1.84 - if (new_status == Query_Operation.Status.REMOVED)
1.85 + if (new_status == Query_Operation.Status.FINISHED)
1.86 remove_overlay()
1.87 }
1.88 }
1.89 @@ -192,7 +218,7 @@
1.90 current_location match {
1.91 case Some(command)
1.92 if current_update_pending ||
1.93 - (current_status != Query_Operation.Status.REMOVED &&
1.94 + (current_status != Query_Operation.Status.FINISHED &&
1.95 changed.commands.contains(command)) =>
1.96 Swing_Thread.later { content_update() }
1.97 case _ =>
2.1 --- a/src/Tools/jEdit/src/active.scala Wed Nov 20 23:00:18 2013 +0100
2.2 +++ b/src/Tools/jEdit/src/active.scala Thu Nov 21 21:55:29 2013 +0100
2.3 @@ -52,9 +52,9 @@
2.4
2.5 case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
2.6 props match {
2.7 - case Position.Id(exec_id) =>
2.8 + case Position.Id(id) =>
2.9 Isabelle.edit_command(snapshot, buffer,
2.10 - props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
2.11 + props.exists(_ == Markup.PADDING_COMMAND), id, text)
2.12 case _ =>
2.13 if (props.exists(_ == Markup.PADDING_LINE))
2.14 Isabelle.insert_line_padding(text_area, text)
3.1 --- a/src/Tools/jEdit/src/find_dockable.scala Wed Nov 20 23:00:18 2013 +0100
3.2 +++ b/src/Tools/jEdit/src/find_dockable.scala Thu Nov 21 21:55:29 2013 +0100
3.3 @@ -37,7 +37,7 @@
3.4 process_indicator.update("Waiting for evaluation of context ...", 5)
3.5 case Query_Operation.Status.RUNNING =>
3.6 process_indicator.update("Running find operation ...", 15)
3.7 - case _ =>
3.8 + case Query_Operation.Status.FINISHED =>
3.9 process_indicator.update(null, 0)
3.10 }
3.11 }
4.1 --- a/src/Tools/jEdit/src/isabelle.scala Wed Nov 20 23:00:18 2013 +0100
4.2 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Nov 21 21:55:29 2013 +0100
4.3 @@ -177,26 +177,28 @@
4.4 snapshot: Document.Snapshot,
4.5 buffer: Buffer,
4.6 padding: Boolean,
4.7 - exec_id: Document_ID.Exec,
4.8 + id: Document_ID.Generic,
4.9 s: String)
4.10 {
4.11 - snapshot.state.execs.get(exec_id).map(_.command) match {
4.12 - case Some(command) =>
4.13 - snapshot.node.command_start(command) match {
4.14 - case Some(start) =>
4.15 - JEdit_Lib.buffer_edit(buffer) {
4.16 - val range = command.proper_range + start
4.17 - if (padding) {
4.18 - buffer.insert(start + range.length, "\n" + s)
4.19 + if (!snapshot.is_outdated) {
4.20 + snapshot.state.find_command(snapshot.version, id) match {
4.21 + case Some((node, command)) =>
4.22 + node.command_start(command) match {
4.23 + case Some(start) =>
4.24 + JEdit_Lib.buffer_edit(buffer) {
4.25 + val range = command.proper_range + start
4.26 + if (padding) {
4.27 + buffer.insert(start + range.length, "\n" + s)
4.28 + }
4.29 + else {
4.30 + buffer.remove(start, range.length)
4.31 + buffer.insert(start, s)
4.32 + }
4.33 }
4.34 - else {
4.35 - buffer.remove(start, range.length)
4.36 - buffer.insert(start, s)
4.37 - }
4.38 - }
4.39 - case None =>
4.40 - }
4.41 - case None =>
4.42 + case None =>
4.43 + }
4.44 + case None =>
4.45 + }
4.46 }
4.47 }
4.48
5.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Nov 20 23:00:18 2013 +0100
5.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Nov 21 21:55:29 2013 +0100
5.3 @@ -38,7 +38,7 @@
5.4 process_indicator.update("Waiting for evaluation of context ...", 5)
5.5 case Query_Operation.Status.RUNNING =>
5.6 process_indicator.update("Sledgehammering ...", 15)
5.7 - case _ =>
5.8 + case Query_Operation.Status.FINISHED =>
5.9 process_indicator.update(null, 0)
5.10 }
5.11 }