# HG changeset patch
# User wenzelm
# Date 1348500516 -7200
# Node ID 7b7bd2d7661d7d4baae07c933b7044f6bca1101a
# Parent  87b9481e4f62c4599dff212f4294ad4bdae6aa19
more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;

diff -r 87b9481e4f62 -r 7b7bd2d7661d etc/isabelle.css
--- a/etc/isabelle.css	Mon Sep 24 16:41:51 2012 +0200
+++ b/etc/isabelle.css	Mon Sep 24 17:28:36 2012 +0200
@@ -44,3 +44,6 @@
 .control        { background-color: #FF6A6A; }
 .bad            { background-color: #FF6A6A; }
 
+.keyword1       { font-weight: bold; }
+.keyword2       { font-weight: bold; }
+
diff -r 87b9481e4f62 -r 7b7bd2d7661d src/Pure/General/pretty.ML
--- 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;
diff -r 87b9481e4f62 -r 7b7bd2d7661d src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Mon Sep 24 16:41:51 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Mon Sep 24 17:28:36 2012 +0200
@@ -75,6 +75,8 @@
   val commentN: string val comment: Markup.T
   val controlN: string val control: Markup.T
   val tokenN: string val token: Properties.T -> Markup.T
+  val keyword1N: string val keyword1: Markup.T
+  val keyword2N: string val keyword2: Markup.T
   val elapsedN: string
   val cpuN: string
   val gcN: string
@@ -241,6 +243,9 @@
 val tokenN = "token";
 fun token props = (tokenN, props);
 
+val (keyword1N, keyword1) = markup_elem "keyword1";
+val (keyword2N, keyword2) = markup_elem "keyword2";
+
 
 (* timing *)
 
diff -r 87b9481e4f62 -r 7b7bd2d7661d src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Mon Sep 24 16:41:51 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Mon Sep 24 17:28:36 2012 +0200
@@ -152,6 +152,9 @@
   val COMMENT = "comment"
   val CONTROL = "control"
 
+  val KEYWORD1 = "keyword1"
+  val KEYWORD2 = "keyword2"
+
 
   /* timing */
 
diff -r 87b9481e4f62 -r 7b7bd2d7661d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Sep 24 16:41:51 2012 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Sep 24 17:28:36 2012 +0200
@@ -178,8 +178,10 @@
   in (output_symbols syms, Symbol.length syms) end;
 
 fun latex_markup (s, _) =
-  if s = Isabelle_Markup.keywordN then ("\\isakeyword{", "}")
-  else if s = Isabelle_Markup.commandN then ("\\isacommand{", "}")
+  if s = Isabelle_Markup.commandN orelse s = Isabelle_Markup.keyword1N
+    then ("\\isacommand{", "}")
+  else if s = Isabelle_Markup.keywordN orelse s = Isabelle_Markup.keyword2N
+    then ("\\isakeyword{", "}")
   else Markup.no_output;
 
 fun latex_indent "" _ = ""
diff -r 87b9481e4f62 -r 7b7bd2d7661d src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Sep 24 16:41:51 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Mon Sep 24 17:28:36 2012 +0200
@@ -468,6 +468,8 @@
 
 
   private val text_colors: Map[String, Color] = Map(
+      Isabelle_Markup.KEYWORD1 -> keyword1_color,
+      Isabelle_Markup.KEYWORD2 -> keyword2_color,
       Isabelle_Markup.STRING -> Color.BLACK,
       Isabelle_Markup.ALTSTRING -> Color.BLACK,
       Isabelle_Markup.VERBATIM -> Color.BLACK,