--- a/src/Pure/General/markup.ML Sun May 30 14:14:30 2010 +0200
+++ b/src/Pure/General/markup.ML Sun May 30 14:21:35 2010 +0200
@@ -82,9 +82,9 @@
val doc_antiqN: string val doc_antiq: string -> T
val keyword_declN: string val keyword_decl: string -> T
val command_declN: string val command_decl: string -> string -> T
- val keywordN: string val keyword: string -> T
+ val keywordN: string val keyword: T
val operatorN: string val operator: T
- val commandN: string val command: string -> T
+ val commandN: string val command: T
val identN: string val ident: T
val stringN: string val string: T
val altstringN: string val altstring: T
@@ -271,9 +271,9 @@
val command_declN = "command_decl";
fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
-val (keywordN, keyword) = markup_string "keyword" nameN;
+val (keywordN, keyword) = markup_elem "keyword";
val (operatorN, operator) = markup_elem "operator";
-val (commandN, command) = markup_string "command" nameN;
+val (commandN, command) = markup_elem "command";
val (identN, ident) = markup_elem "ident";
val (stringN, string) = markup_elem "string";
val (altstringN, altstring) = markup_elem "altstring";
--- a/src/Pure/General/pretty.ML Sun May 30 14:14:30 2010 +0200
+++ b/src/Pure/General/pretty.ML Sun May 30 14:21:35 2010 +0200
@@ -137,8 +137,8 @@
fun markup m prts = markup_block m (0, prts);
fun mark m prt = markup m [prt];
-fun keyword name = mark (Markup.keyword name) (str name);
-fun command name = mark (Markup.command name) (str name);
+fun keyword name = mark Markup.keyword (str name);
+fun command name = mark Markup.command (str name);
fun markup_chunks m prts = markup m (fbreaks prts);
val chunks = markup_chunks Markup.none;
--- a/src/Pure/Thy/thy_syntax.ML Sun May 30 14:14:30 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Sun May 30 14:21:35 2010 +0200
@@ -47,8 +47,8 @@
local
val token_kind_markup =
- fn Token.Command => (Markup.commandN, [])
- | Token.Keyword => (Markup.keywordN, [])
+ fn Token.Command => Markup.command
+ | Token.Keyword => Markup.keyword
| Token.Ident => Markup.ident
| Token.LongIdent => Markup.ident
| Token.SymIdent => Markup.ident