src/Pure/PIDE/markup.ML
changeset 50215 97959912840a
parent 50201 c26369c9eda6
child 50255 d0ec1f0d1d7d
     1.1 --- a/src/Pure/PIDE/markup.ML	Mon Nov 26 14:43:28 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Mon Nov 26 16:16:47 2012 +0100
     1.3 @@ -96,6 +96,8 @@
     1.4    val proof_stateN: string val proof_state: int -> T
     1.5    val stateN: string val state: T
     1.6    val subgoalN: string val subgoal: T
     1.7 +  val paddingN: string
     1.8 +  val padding_line: string * string
     1.9    val sendbackN: string val sendback: T
    1.10    val intensifyN: string val intensify: T
    1.11    val taskN: string
    1.12 @@ -333,7 +335,11 @@
    1.13  
    1.14  val (stateN, state) = markup_elem "state";
    1.15  val (subgoalN, subgoal) = markup_elem "subgoal";
    1.16 +
    1.17 +val paddingN = "padding";
    1.18 +val padding_line = (paddingN, lineN);
    1.19  val (sendbackN, sendback) = markup_elem "sendback";
    1.20 +
    1.21  val (intensifyN, intensify) = markup_elem "intensify";
    1.22  
    1.23