# HG changeset patch # User wenzelm # Date 1385067329 -3600 # Node ID bbd2fa3538097eb8564974f2a254920b31ecb983 # Parent 5adc68deb3229f5933ae149c90fd646cb9cb881c 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); diff -r 5adc68deb322 -r bbd2fa353809 src/Pure/PIDE/query_operation.scala --- 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 _ => diff -r 5adc68deb322 -r bbd2fa353809 src/Tools/jEdit/src/active.scala --- 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) diff -r 5adc68deb322 -r bbd2fa353809 src/Tools/jEdit/src/find_dockable.scala --- 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) } } diff -r 5adc68deb322 -r bbd2fa353809 src/Tools/jEdit/src/isabelle.scala --- 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 => + } } } diff -r 5adc68deb322 -r bbd2fa353809 src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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) } }