# HG changeset patch
# User wenzelm
# Date 1215703582 -7200
# Node ID 56eb04c7b6b28530782d3187f88dc159121e0e81
# Parent  b819d3b263a01c669d49241593725d40ac329ea7
added prompt markup;

diff -r b819d3b263a0 -r 56eb04c7b6b2 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Jul 10 13:37:35 2008 +0200
+++ b/src/Pure/General/markup.ML	Thu Jul 10 17:26:22 2008 +0200
@@ -62,6 +62,7 @@
   val whitespaceN: string val whitespace: T
   val junkN: string val junk: T
   val commandspanN: string val commandspan: string -> T
+  val promptN: string val prompt: T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
   val sendbackN: string val sendback: T
@@ -186,6 +187,7 @@
 
 (* toplevel *)
 
+val (promptN, prompt) = markup_elem "prompt";
 val (stateN, state) = markup_elem "state";
 val (subgoalN, subgoal) = markup_elem "subgoal";
 val (sendbackN, sendback) = markup_elem "sendback";