src/Tools/jEdit/src/isabelle_rendering.scala

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 21 12:07:59 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 21 15:39:51 2012 +0200
@@ -125,6 +125,8 @@
   val quoted_color = color_value("quoted_color")
   val highlight_color = color_value("highlight_color")
   val hyperlink_color = color_value("hyperlink_color")
+  val sendback_color = color_value("sendback_color")
+  val sendback_active_color = color_value("sendback_active_color")
   val keyword1_color = color_value("keyword1_color")
   val keyword2_color = color_value("keyword2_color")
 
@@ -237,6 +239,22 @@
   }
 
 
+  def sendback(range: Text.Range): Option[Text.Info[Sendback]] =
+  {
+    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)))
+      case _ => None
+    }
+  }
+
+
   private def tooltip_text(msg: XML.Tree): String =
     Pretty.string_of(List(msg), margin = options.int("jedit_tooltip_margin"))
 
@@ -388,6 +406,13 @@
     message_colors.get(pri).map((_, is_separator))
   }
 
+
+  private val background1_include =
+    Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
+      Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
+      Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY +
+      Isabelle_Markup.SENDBACK
+
   def background1(range: Text.Range): Stream[Text.Info[Color]] =
   {
     if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
@@ -395,10 +420,7 @@
       for {
         Text.Info(r, result) <-
           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
-            range, (Some(Protocol.Status.init), None),
-            Some(Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
-              Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
-              Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
+            range, (Some(Protocol.Status.init), None), Some(background1_include),
             {
               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
               if (Protocol.command_status_markup(markup.name)) =>
@@ -407,6 +429,8 @@
                 (None, Some(bad_color))
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
                 (None, Some(intensify_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) =>
+                (None, Some(sendback_color))
             })
         color <-
           (result match {