src/Pure/Syntax/lexicon.ML

--- a/src/Pure/Syntax/lexicon.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -181,9 +181,9 @@
   | FloatSy     => Markup.numeral
   | XNumSy      => Markup.numeral
   | StrSy       => Markup.inner_string
-  | Space       => Markup.none
+  | Space       => Markup.empty
   | Comment     => Markup.inner_comment
-  | EOF         => Markup.none;
+  | EOF         => Markup.empty;
 
 fun report_token ctxt (Token (kind, _, (pos, _))) =
   Context_Position.report ctxt (token_kind_markup kind) pos;