changeset 23695 | 6c4662bb4862 |
parent 23671 | 9e8257472c27 |
child 23704 | 18d6ee425689 |
--- a/src/Pure/General/markup.ML Tue Jul 10 13:12:53 2007 +0200 +++ b/src/Pure/General/markup.ML Tue Jul 10 15:45:34 2007 +0200 @@ -17,6 +17,7 @@ val fileN: string val positionN: string val position: T val indentN: string + val widthN: string val blockN: string val block: int -> T val breakN: string val break: int -> T val fbreakN: string val fbreak: T