diff -r c1dbcde94cd2 -r e68e44836d04 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Dec 09 22:13:48 2014 +0100
@@ -6,9 +6,9 @@
 
 signature THY_SYNTAX =
 sig
-  val reports_of_tokens: Token.T list -> bool * Position.report_text list
-  val present_token: Token.T -> Output.output
-  val present_span: Command_Span.span -> Output.output
+  val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list
+  val present_token: Keyword.keywords -> Token.T -> Output.output
+  val present_span: Keyword.keywords -> Command_Span.span -> Output.output
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
   val map_element: ('a -> 'b) -> 'a element -> 'b element
@@ -24,7 +24,7 @@
 
 local
 
-fun reports_of_token tok =
+fun reports_of_token keywords tok =
   let
     val malformed_symbols =
       Input.source_explode (Token.source_position_of tok)
@@ -32,21 +32,21 @@
           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 tok :: Token.completion_report tok @ malformed_symbols;
+    val reports = Token.report keywords tok :: Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
 
 in
 
-fun reports_of_tokens toks =
-  let val results = map reports_of_token toks
+fun reports_of_tokens keywords toks =
+  let val results = map (reports_of_token keywords) toks
   in (exists fst results, maps snd results) end;
 
 end;
 
-fun present_token tok =
-  Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
+fun present_token keywords tok =
+  Markup.enclose (Token.markup keywords tok) (Output.output (Token.unparse tok));
 
-val present_span = implode o map present_token o Command_Span.content;
+fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;