src/Pure/PIDE/markup.ML
changeset 61862 e2a9e46ac0fb
parent 61660 78b371644654
child 61864 3a5992c3410c
     1.1 --- a/src/Pure/PIDE/markup.ML	Wed Dec 16 17:30:30 2015 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Thu Dec 17 17:32:01 2015 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4    val indentN: string
     1.5    val blockN: string val block: int -> T
     1.6    val widthN: string
     1.7 -  val breakN: string val break: int -> T
     1.8 +  val breakN: string val break: int -> int -> T
     1.9    val fbreakN: string val fbreak: T
    1.10    val itemN: string val item: T
    1.11    val wordsN: string val words: T
    1.12 @@ -381,7 +381,8 @@
    1.13  val (blockN, block) = markup_int "block" indentN;
    1.14  
    1.15  val widthN = "width";
    1.16 -val (breakN, break) = markup_int "break" widthN;
    1.17 +val breakN = "break";
    1.18 +fun break w i = (breakN, [(widthN, print_int w), (indentN, print_int i)]);
    1.19  
    1.20  val (fbreakN, fbreak) = markup_elem "fbreak";
    1.21