src/Pure/PIDE/markup.ML
changeset 50215 97959912840a
parent 50201 c26369c9eda6
child 50255 d0ec1f0d1d7d
--- a/src/Pure/PIDE/markup.ML	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Nov 26 16:16:47 2012 +0100
@@ -96,6 +96,8 @@
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
+  val paddingN: string
+  val padding_line: string * string
   val sendbackN: string val sendback: T
   val intensifyN: string val intensify: T
   val taskN: string
@@ -333,7 +335,11 @@
 
 val (stateN, state) = markup_elem "state";
 val (subgoalN, subgoal) = markup_elem "subgoal";
+
+val paddingN = "padding";
+val padding_line = (paddingN, lineN);
 val (sendbackN, sendback) = markup_elem "sendback";
+
 val (intensifyN, intensify) = markup_elem "intensify";