# HG changeset patch # User wenzelm # Date 1348239044 -7200 # Node ID db58490a68acb7f97f186c15ed6e24bac7a35dee # Parent 2e3e7ea5ce8e4f8c1240fda6d4906bb9d8c119e1 more realistic sendback: pick exec_id from message position and text from buffer; diff -r 2e3e7ea5ce8e -r db58490a68ac src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Sep 21 15:39:51 2012 +0200 +++ b/src/Pure/PIDE/command.scala Fri Sep 21 16:50:44 2012 +0200 @@ -60,16 +60,15 @@ case XML.Elem(Markup(name, atts), body) => atts match { case Isabelle_Markup.Serial(i) => - val props = Position.purge(atts) - val result = XML.Elem(Markup(name, props), body) - val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body) + val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), atts), body) + val message2 = XML.Elem(Markup(name, Position.purge(atts)), body) - val st0 = copy(results = results + (i -> result_message)) + val st0 = copy(results = results + (i -> message1)) val st1 = - if (Protocol.is_tracing(result)) st0 + if (Protocol.is_tracing(message)) st0 else (st0 /: Protocol.message_positions(command, message))( - (st, range) => st.add_markup(Text.Info(range, result))) + (st, range) => st.add_markup(Text.Info(range, message2))) st1 case _ => System.err.println("Ignored message without serial number: " + message); this diff -r 2e3e7ea5ce8e -r db58490a68ac src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 15:39:51 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 16:50:44 2012 +0200 @@ -239,17 +239,21 @@ } - def sendback(range: Text.Range): Option[Text.Info[Sendback]] = + def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] = { - snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)), - { - case Text.Info(info_range, Protocol.Sendback(body)) => - Text.Info(snapshot.convert(info_range), body) - }) match - { - case Text.Info(_, Text.Info(range, body)) #:: _ => - snapshot.node.command_at(range.start) - .map(command_range => Text.Info(range, Sendback(command_range._1, body))) + val results = + snapshot.cumulate_markup[(Option[Document.Exec_ID], Option[Text.Range])](range, + (None, None), Some(messages_include + Isabelle_Markup.SENDBACK), + { + case ((_, info), Text.Info(_, XML.Elem(Markup(name, Position.Id(id)), _))) + if messages_include(name) => (Some(id), info) + + case ((id, _), Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) => + (id, Some(snapshot.convert(info_range))) + }) + + (for (Text.Info(_, (Some(id), Some(r))) <- results) yield Text.Info(r, id)) match { + case res #:: _ => Some(res) case _ => None } } @@ -375,6 +379,10 @@ } + private val messages_include = + Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE, + Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE) + private val message_colors = Map( Isabelle_Rendering.writeln_pri -> writeln_message_color, Isabelle_Rendering.tracing_pri -> tracing_message_color, @@ -383,11 +391,8 @@ def line_background(range: Text.Range): Option[(Color, Boolean)] = { - val messages = - Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE, - Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE) val results = - snapshot.cumulate_markup[Int](range, 0, Some(messages), + snapshot.cumulate_markup[Int](range, 0, Some(messages_include), { case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) if name == Isabelle_Markup.WRITELN_MESSAGE || diff -r 2e3e7ea5ce8e -r db58490a68ac src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 15:39:51 2012 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 16:50:44 2012 +0200 @@ -101,17 +101,25 @@ private class Active_Area[A]( rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]]) { - private var the_info: Option[Text.Info[A]] = None + private var the_text_info: Option[(String, Text.Info[A])] = None - def info: Option[Text.Info[A]] = the_info + def text_info: Option[(String, Text.Info[A])] = the_text_info + def info: Option[Text.Info[A]] = the_text_info.map(_._2) def update(new_info: Option[Text.Info[A]]) { - val old_info = the_info - if (new_info != old_info) { - for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt } - JEdit_Lib.invalidate_range(text_area, range) - the_info = new_info + val old_text_info = the_text_info + val new_text_info = + new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) + + if (new_text_info != old_text_info) { + for { + r0 <- JEdit_Lib.visible_range(text_area) + opt <- List(old_text_info, new_text_info) + (_, Text.Info(r1, _)) <- opt + r2 <- r1.try_restrict(r0) // FIXME more precise?! + } JEdit_Lib.invalidate_range(text_area, r2) + the_text_info = new_text_info } } @@ -127,7 +135,8 @@ private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _) private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _) - private val sendback_area = new Active_Area[Sendback]((r: Isabelle_Rendering) => r.sendback _) + private val sendback_area = + new Active_Area[Document.Exec_ID]((r: Isabelle_Rendering) => r.sendback _) private val active_areas = List((highlight_area, true), (hyperlink_area, true), (sendback_area, false)) @@ -149,8 +158,8 @@ case Some(Text.Info(_, link)) => link.follow(view) case None => } - sendback_area.info match { - case Some(Text.Info(_, sendback)) => sendback.activate(view) + sendback_area.text_info match { + case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id) case None => } } diff -r 2e3e7ea5ce8e -r db58490a68ac src/Tools/jEdit/src/sendback.scala --- a/src/Tools/jEdit/src/sendback.scala Fri Sep 21 15:39:51 2012 +0200 +++ b/src/Tools/jEdit/src/sendback.scala Fri Sep 21 16:50:44 2012 +0200 @@ -9,18 +9,12 @@ import isabelle._ -import org.gjt.sp.jedit.{View, jEdit} -import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.View object Sendback { - def apply(command: Command, body: XML.Body): Sendback = new Sendback(command, body) -} - -class Sendback private(command: Command, body: XML.Body) -{ - def activate(view: View) + def activate(view: View, text: String, exec_id: Document.Exec_ID) { Swing_Thread.require() @@ -30,15 +24,19 @@ val model = doc_view.model val buffer = model.buffer val snapshot = model.snapshot() - snapshot.node.command_start(command) match { - case Some(start) if !snapshot.is_outdated => - val text = Pretty.string_of(body) - try { - buffer.beginCompoundEdit() - buffer.remove(start, command.proper_range.length) - buffer.insert(start, text) + + snapshot.state.execs.get(exec_id).map(_.command) match { + case Some(command) if !snapshot.is_outdated => + snapshot.node.command_start(command) match { + case Some(start) => + try { + buffer.beginCompoundEdit() + buffer.remove(start, command.proper_range.length) + buffer.insert(start, text) + } + finally { buffer.endCompoundEdit() } + case None => } - finally { buffer.endCompoundEdit() } case _ => } }