more abstract Sendback operations, with explicit id/exec_id properties;
purge result messages (again), cf. db58490a68ac, 7b61a539721e;

--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -130,7 +130,7 @@
 
 fun output_line cert =
   "To repeat this proof with a certifiate use this command:\n" ^
-    Markup.markup Isabelle_Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
+    Sendback.markup ("by (sos_cert \"" ^ cert ^ "\")")
 
 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
 

--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Nov 22 13:21:02 2012 +0100
@@ -235,7 +235,7 @@
 
 ML {*
   fun make_benchmark n =
-    writeln (Markup.markup Isabelle_Markup.sendback
+    writeln (Sendback.markup
       ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
         (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
 *}

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -470,7 +470,7 @@
               pprint_nt (fn () => Pretty.blk (0,
                   pstrs "Hint: To check that the induction hypothesis is \
                         \general enough, try this command: " @
-                  [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
+                  [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0,
                        pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
             else
               ()

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -754,8 +754,7 @@
           (true, "")
         end)
 
-fun sendback sub =
-  Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
+fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub)
 
 val commit_timeout = seconds 30.0
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -233,15 +233,14 @@
   command_call (string_for_reconstructor reconstr) ss
 
 fun try_command_line banner time command =
-  banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^
-  show_time time ^ "."
+  banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "."
 
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of
       "" => ""
     | command =>
-      "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
+      "\nTo minimize: " ^ Sendback.markup command ^ "."
 
 fun split_used_facts facts =
   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
@@ -1055,7 +1054,7 @@
            else if preplay then
              " (" ^ string_from_ext_time ext_time ^ ")"
            else
-             "") ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
+             "") ^ ":\n" ^ Sendback.markup isar_text
       end
     val isar_proof =
       if debug then

--- a/src/HOL/Tools/try0.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/HOL/Tools/try0.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -138,7 +138,7 @@
              Auto_Try => "Auto Try Methods found a proof"
            | Try => "Try Methods found a proof"
            | Normal => "Try this") ^ ": " ^
-          Markup.markup Isabelle_Markup.sendback
+          Sendback.markup
               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
           "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"

--- a/src/Pure/PIDE/command.scala	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Nov 22 13:21:02 2012 +0100
@@ -66,14 +66,16 @@
         case XML.Elem(Markup(name, atts), body) =>
           atts match {
             case Isabelle_Markup.Serial(i) =>
-              val st0 =
-                copy(results =
-                  results + (i -> XML.Elem(Markup(Isabelle_Markup.message(name), atts), body)))
+              val props = Position.purge(atts)
+              val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+              val message2 = XML.Elem(Markup(name, props), body)
+
+              val st0 = copy(results = results + (i -> message1))
               val st1 =
                 if (Protocol.is_tracing(message)) st0
                 else
                   (st0 /: Protocol.message_positions(command, message))(
-                    (st, range) => st.add_markup(Text.Info(range, message)))
+                    (st, range) => st.add_markup(Text.Info(range, message2)))
 
               st1
             case _ => System.err.println("Ignored message without serial number: " + message); this

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/sendback.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -0,0 +1,28 @@
+(*  Title:      Pure/PIDE/sendback.ML
+    Author:     Makarius
+
+Clickable "sendback" areas within the source text (see also
+Tools/jEdit/src/sendback.scala).
+*)
+
+signature SENDBACK =
+sig
+  val make_markup: unit -> Markup.T
+  val markup: string -> string
+end;
+
+structure Sendback: SENDBACK =
+struct
+
+fun make_markup () =
+  let
+    val props =
+      (case Position.get_id (Position.thread_data ()) of
+        SOME id => [(Isabelle_Markup.idN, id)]
+      | NONE => []);
+  in Markup.properties props Isabelle_Markup.sendback end;
+
+fun markup s = Markup.markup (make_markup ()) s;
+
+end;
+

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -8,7 +8,6 @@
 signature PROOF_GENERAL =
 sig
   val test_markupN: string
-  val sendback: string -> Pretty.T list -> unit
   val init: bool -> unit
   structure ThyLoad: sig val add_path: string -> unit end
 end;
@@ -113,9 +112,6 @@
 fun tell_file_retracted path =
   emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
 
-fun sendback heading prts =
-  Pretty.writeln (Pretty.big_list heading [Pretty.markup Isabelle_Markup.sendback prts]);
-
 
 (* theory loader actions *)
 

--- a/src/Pure/ROOT	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/Pure/ROOT	Thu Nov 22 13:21:02 2012 +0100
@@ -147,6 +147,7 @@
     "PIDE/isabelle_markup.ML"
     "PIDE/markup.ML"
     "PIDE/protocol.ML"
+    "PIDE/sendback.ML"
     "PIDE/xml.ML"
     "PIDE/yxml.ML"
     "Proof/extraction.ML"

--- a/src/Pure/ROOT.ML	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/Pure/ROOT.ML	Thu Nov 22 13:21:02 2012 +0100
@@ -64,6 +64,7 @@
 
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
+use "PIDE/sendback.ML";
 
 use "General/graph.ML";
 

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Nov 22 12:22:03 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Nov 22 13:21:02 2012 +0100
@@ -246,23 +246,11 @@
 
 
   def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] =
-  {
-    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
-    }
-  }
+    snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
+        {
+          case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, Position.Id(id)), _)) =>
+            Text.Info(snapshot.convert(info_range), id)
+        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
 
 
   def tooltip_message(range: Text.Range): XML.Body =