# HG changeset patch
# User wenzelm
# Date 1217957342 -7200
# Node ID 7420e78f1541e2f0e0aae87423e47d2d7299a0ad
# Parent  df552e6027cf365736a50fbd8c789caee5bae47b
added token;

diff -r df552e6027cf -r 7420e78f1541 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Aug 05 14:40:48 2008 +0200
+++ b/src/Pure/General/markup.ML	Tue Aug 05 19:29:02 2008 +0200
@@ -56,6 +56,7 @@
   val commandN: string val command: string -> T
   val keyword_declN: string val keyword_decl: string -> T
   val command_declN: string val command_decl: string -> string -> T
+  val tokenN: string val token: T
   val stringN: string val string: T
   val altstringN: string val altstring: T
   val verbatimN: string val verbatim: T
@@ -184,6 +185,7 @@
 val command_declN = "command_decl";
 fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
 
+val (tokenN, token) = markup_elem "token";
 val (stringN, string) = markup_elem "string";
 val (altstringN, altstring) = markup_elem "altstring";
 val (verbatimN, verbatim) = markup_elem "verbatim";