# HG changeset patch
# User wenzelm
# Date 1187198663 -7200
# Node ID bfd59eb6e24e3454ade70b2046a4915d651b6cd6
# Parent  4016baca4973a03b99f205212b53f48fdb349d82
added sendback;

diff -r 4016baca4973 -r bfd59eb6e24e src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Aug 15 15:06:58 2007 +0200
+++ b/src/Pure/General/markup.ML	Wed Aug 15 19:24:23 2007 +0200
@@ -54,6 +54,7 @@
   val promptN: string val prompt: T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
+  val sendbackN: string val sendback: T
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
   val output: T -> output * output
@@ -153,6 +154,7 @@
 val (promptN, prompt) = markup "prompt";
 val (stateN, state) = markup "state";
 val (subgoalN, subgoal) = markup "subgoal";
+val (sendbackN, sendback) = markup "sendback";
 
 
 (* print mode operations *)
diff -r 4016baca4973 -r bfd59eb6e24e src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 15 15:06:58 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 15 19:24:23 2007 +0200
@@ -9,6 +9,7 @@
 signature PROOF_GENERAL =
 sig
   val init: bool -> unit
+  val sendback: string -> Pretty.T list -> unit
   val write_keywords: string -> unit
 end;
 
@@ -101,6 +102,7 @@
 fun proof_general_markup (name, props) =
   (if name = Markup.promptN then ("", special "372")
     else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
+    else if name = Markup.sendbackN then (special "375", special "376")
     else ("", ""))
   |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
     (fn (bg, en) =>
@@ -140,6 +142,9 @@
 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 Markup.sendback prts]);
+
 
 (* theory loader actions *)