1.1 --- a/src/Pure/General/markup.ML	Wed Aug 15 15:06:58 2007 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Wed Aug 15 19:24:23 2007 +0200
     1.3 @@ -54,6 +54,7 @@
     1.4    val promptN: string val prompt: T
     1.5    val stateN: string val state: T
     1.6    val subgoalN: string val subgoal: T
     1.7 +  val sendbackN: string val sendback: T
     1.8    val default_output: T -> output * output
     1.9    val add_mode: string -> (T -> output * output) -> unit
    1.10    val output: T -> output * output
    1.11 @@ -153,6 +154,7 @@
    1.12  val (promptN, prompt) = markup "prompt";
    1.13  val (stateN, state) = markup "state";
    1.14  val (subgoalN, subgoal) = markup "subgoal";
    1.15 +val (sendbackN, sendback) = markup "sendback";
    1.16  
    1.17  
    1.18  (* print mode operations *)

     2.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 15 15:06:58 2007 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 15 19:24:23 2007 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  signature PROOF_GENERAL =
     2.5  sig
     2.6    val init: bool -> unit
     2.7 +  val sendback: string -> Pretty.T list -> unit
     2.8    val write_keywords: string -> unit
     2.9  end;
    2.10  
    2.11 @@ -101,6 +102,7 @@
    2.12  fun proof_general_markup (name, props) =
    2.13    (if name = Markup.promptN then ("", special "372")
    2.14      else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
    2.15 +    else if name = Markup.sendbackN then (special "375", special "376")
    2.16      else ("", ""))
    2.17    |> (name <> Markup.promptN andalso print_mode_active "test_markup") ?
    2.18      (fn (bg, en) =>
    2.19 @@ -140,6 +142,9 @@
    2.20  fun tell_file_retracted path =
    2.21    emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
    2.22  
    2.23 +fun sendback heading prts =
    2.24 +  Pretty.writeln (Pretty.big_list heading [Pretty.markup Markup.sendback prts]);
    2.25 +
    2.26  
    2.27  (* theory loader actions *)
    2.28