--- a/src/Pure/Thy/thy_syntax.ML Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Wed Dec 10 13:45:44 2014 +0100
@@ -32,7 +32,7 @@
if Symbol.is_malformed sym
then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
- val reports = Token.report keywords tok :: Token.completion_report tok @ malformed_symbols;
+ val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
in (is_malformed, reports) end;
in
@@ -44,7 +44,7 @@
end;
fun present_token keywords tok =
- Markup.enclose (Token.markup keywords tok) (Output.output (Token.unparse tok));
+ fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;