--- a/src/Pure/Thy/thy_syntax.ML Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Wed Aug 18 11:02:47 2010 +0200
@@ -59,9 +59,9 @@
| Token.String => Markup.string
| Token.AltString => Markup.altstring
| Token.Verbatim => Markup.verbatim
- | Token.Space => Markup.none
+ | Token.Space => Markup.empty
| Token.Comment => Markup.comment
- | Token.InternalValue => Markup.none
+ | Token.InternalValue => Markup.empty
| Token.Malformed => Markup.malformed
| Token.Error _ => Markup.malformed
| Token.Sync => Markup.control