# HG changeset patch
# User wenzelm
# Date 1393360346 -3600
# Node ID baa7a1e57f4a4a5eee1097a1a5d954c15da4355c
# Parent  75a48dc4383e1e0c5a61a42f96fc9c96c44d13d6
back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors;

diff -r 75a48dc4383e -r baa7a1e57f4a src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Feb 25 20:57:57 2014 +0100
+++ b/src/Pure/Isar/token.ML	Tue Feb 25 21:32:26 2014 +0100
@@ -220,7 +220,7 @@
 local
 
 val token_kind_markup =
- fn Command       => (Markup.keyword1, "")
+ fn Command       => (Markup.command, "")
   | Keyword       => (Markup.keyword2, "")
   | Ident         => (Markup.empty, "")
   | LongIdent     => (Markup.empty, "")
diff -r 75a48dc4383e -r baa7a1e57f4a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Feb 25 20:57:57 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Feb 25 21:32:26 2014 +0100
@@ -97,7 +97,7 @@
   val document_antiquotation_optionN: string
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
-  val commandN: string
+  val commandN: string val command: T
   val operatorN: string val operator: T
   val stringN: string val string: T
   val altstringN: string val altstring: T
@@ -395,8 +395,7 @@
 
 (* outer syntax *)
 
-val commandN = "command";
-
+val (commandN, command) = markup_elem "command";
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (operatorN, operator) = markup_elem "operator";
diff -r 75a48dc4383e -r baa7a1e57f4a src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Feb 25 20:57:57 2014 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Feb 25 21:32:26 2014 +0100
@@ -178,7 +178,7 @@
   in (output_symbols syms, Symbol.length syms) end;
 
 fun latex_markup (s, _) =
-  if s = Markup.keyword1N then ("\\isacommand{", "}")
+  if s = Markup.commandN orelse s = Markup.keyword1N then ("\\isacommand{", "}")
   else if s = Markup.keyword2N then ("\\isakeyword{", "}")
   else Markup.no_output;