more realistic sendback: pick exec_id from message position and text from buffer;
--- 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
--- 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 ||
--- 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 =>
}
}
--- 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 _ =>
}
}