src/Pure/General/pretty.ML
changeset 49554 7b7bd2d7661d
parent 48704 85a3de10567d
child 49565 ea4308b7ef0f
--- a/src/Pure/General/pretty.ML	Mon Sep 24 16:41:51 2012 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 24 17:28:36 2012 +0200
@@ -37,8 +37,8 @@
   val mark: Markup.T -> T -> T
   val mark_str: Markup.T * string -> T
   val marks_str: Markup.T list * string -> T
+  val command: string -> T
   val keyword: string -> T
-  val command: string -> T
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
   val chunks2: T list -> T
@@ -150,8 +150,8 @@
 fun mark_str (m, s) = mark m (str s);
 fun marks_str (ms, s) = fold_rev mark ms (str s);
 
-fun keyword name = mark_str (Isabelle_Markup.keyword, name);
-fun command name = mark_str (Isabelle_Markup.command, name);
+fun command name = mark_str (Isabelle_Markup.keyword1, name);
+fun keyword name = mark_str (Isabelle_Markup.keyword2, name);
 
 fun markup_chunks m prts = markup m (fbreaks prts);
 val chunks = markup_chunks Markup.empty;