# HG changeset patch
# User wenzelm
# Date 1275222095 -7200
# Node ID a4b2bb0dab0867eb406780d77feb41eb5129ce08
# Parent  8cdddd689ea98de1989786737764abab2b296290
simplified command/keyword markup;

diff -r 8cdddd689ea9 -r a4b2bb0dab08 src/Pure/General/markup.ML
--- 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";
diff -r 8cdddd689ea9 -r a4b2bb0dab08 src/Pure/General/pretty.ML
--- 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;
diff -r 8cdddd689ea9 -r a4b2bb0dab08 src/Pure/Thy/thy_syntax.ML
--- 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