src/Pure/General/markup.ML
changeset 24289 bfd59eb6e24e
parent 23922 707639e9497d
child 24555 ea220faa69e7
--- 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 *)