# HG changeset patch
# User wenzelm
# Date 1496955847 -7200
# Node ID bd75167090514adbcc3e0d5488541b4637423f12
# Parent  f704c063e95d0f9efacb7a8ae220fa0aa05ba384
more HTML rendering as in Isabelle/jEdit;
tuned;

diff -r f704c063e95d -r bd7516709051 etc/isabelle.css
--- a/etc/isabelle.css	Thu Jun 08 21:17:13 2017 +0200
+++ b/etc/isabelle.css	Thu Jun 08 23:04:07 2017 +0200
@@ -35,23 +35,30 @@
 .binding        { color: #336655; }
 .tfree          { color: #A020F0; }
 .tvar           { color: #A020F0; }
-.free           { color: blue; }
+.free           { color: #0000FF; }
 .skolem         { color: #D2691E; }
-.bound          { color: green; }
+.bound          { color: #008000; }
 .var            { color: #00009B; }
 .numeral        { }
 .literal        { font-weight: bold; }
 .delimiter      { }
-.inner_string   { color: #FF00CC; }
+.inner_numeral  { color: #FF0000; }
+.inner_quoted   { color: #FF00CC; }
 .inner_cartouche { color: #CC6600; }
 .inner_comment  { color: #CC0000; }
+.dynamic        { color: #7BA428; }
+.class_parameter_color { color: #D2691E; }
 
 .bold           { font-weight: bold; }
 
-.keyword1       { color: #006699; font-weight: bold; }
-.keyword2       { color: #009966; font-weight: bold; }
-.keyword3       { color: #0099FF; font-weight: bold; }
-.operator       { }
+.main           { color: #000000; }
+.command        { font-weight: bold; }
+.keyword        { font-weight: bold; }
+.keyword1       { color: #006699; }
+.keyword2       { color: #009966; }
+.keyword3       { color: #0099FF; }
+.quasi_keyword  { color: #9966FF; }
+.operator       { color: #323232; }
 .string         { color: #FF00CC; }
 .alt_string     { color: #CC00CC; }
 .verbatim       { color: #6600CC; }
diff -r f704c063e95d -r bd7516709051 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Jun 08 21:17:13 2017 +0200
+++ b/src/Pure/Isar/token.ML	Thu Jun 08 23:04:07 2017 +0200
@@ -293,6 +293,8 @@
 fun keyword_markup (important, keyword) x =
   if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
 
+val keyword_properties = Markup.properties [(Markup.kindN, Markup.keywordN)];
+
 fun completion_report tok =
   if is_kind Keyword tok
   then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
@@ -302,7 +304,8 @@
   if is_command tok then
     keyword_reports tok (command_markups keywords (content_of tok))
   else if is_kind Keyword tok then
-    keyword_reports tok [keyword_markup (false, Markup.keyword2) (content_of tok)]
+    keyword_reports tok
+      [keyword_markup (false, keyword_properties Markup.keyword2) (content_of tok)]
   else
     let val (m, text) = token_kind_markup (kind_of tok)
     in [((pos_of tok, m), text)] end;
diff -r f704c063e95d -r bd7516709051 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jun 08 21:17:13 2017 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Jun 08 23:04:07 2017 +0200
@@ -125,7 +125,8 @@
   val markdown_itemN: string val markdown_item: int -> T
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
-  val commandN: string val command: T
+  val commandN: string
+  val keywordN: string
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
@@ -304,7 +305,7 @@
     (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
 
 fun get_entity_kind (name, props) =
-  if name = entityN then AList.lookup (op =) props kindN
+  if name = entityN then Properties.get props kindN
   else NONE;
 
 val defN = "def";
@@ -480,7 +481,9 @@
 (* outer syntax *)
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
-val (commandN, command) = markup_elem "command";
+
+val commandN = "command";
+val keywordN = "keyword";
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";
diff -r f704c063e95d -r bd7516709051 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Jun 08 21:17:13 2017 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Jun 08 23:04:07 2017 +0200
@@ -325,6 +325,7 @@
   /* outer syntax */
 
   val COMMAND = "command"
+  val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
diff -r f704c063e95d -r bd7516709051 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu Jun 08 21:17:13 2017 +0200
+++ b/src/Pure/Thy/html.ML	Thu Jun 08 23:04:07 2017 +0200
@@ -25,8 +25,9 @@
 (* common markup *)
 
 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
+val enclose_span = uncurry enclose o span;
 
-val hidden = span Markup.hiddenN |-> enclose;
+val hidden = enclose_span Markup.hiddenN;
 
 
 (* symbol output *)
@@ -85,9 +86,14 @@
 
 fun present_span symbols keywords =
   let
+    fun present_markup (name, props) =
+      (case Properties.get props Markup.kindN of
+        SOME kind =>
+          if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I
+      | NONE => I) #> enclose_span name;
     fun present_token tok =
-      fold_rev (uncurry enclose o span o #1)
-        (Token.markups keywords tok) (output symbols (Token.unparse tok));
+      fold_rev present_markup (Token.markups keywords tok)
+        (output symbols (Token.unparse tok));
   in implode o map present_token o Command_Span.content end;
 
 
diff -r f704c063e95d -r bd7516709051 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Jun 08 21:17:13 2017 +0200
+++ b/src/Pure/Thy/present.scala	Thu Jun 08 23:04:07 2017 +0200
@@ -104,19 +104,28 @@
   /* theory document */
 
   private val document_span_elements =
-    Markup.Elements(Markup.TFREE, Markup.TVAR, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
-      Markup.NUMERAL, Markup.LITERAL, Markup.DELIMITER, Markup.INNER_STRING, Markup.INNER_CARTOUCHE,
-      Markup.INNER_COMMENT, Markup.COMMAND, Markup.KEYWORD1, Markup.KEYWORD2, Markup.KEYWORD3,
-      Markup.QUASI_KEYWORD, Markup.IMPROPER, Markup.OPERATOR, Markup.STRING, Markup.ALT_STRING,
-      Markup.VERBATIM, Markup.CARTOUCHE, Markup.COMMENT)
+    Markup.Elements(Rendering.text_color.keySet + Markup.NUMERAL + Markup.COMMENT)
 
   def make_html(xml: XML.Body): XML.Body =
     xml map {
       case XML.Wrapped_Elem(markup, body1, body2) =>
         XML.Wrapped_Elem(markup, make_html(body1), make_html(body2))
       case XML.Elem(markup, body) =>
-        if (document_span_elements(markup.name)) HTML.span(markup.name, make_html(body))
-        else XML.Elem(markup, make_html(body))
+        val name = markup.name
+        val html =
+          markup.properties match {
+            case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
+              List(HTML.span(kind, make_html(body)))
+            case _ =>
+              make_html(body)
+          }
+        Rendering.text_color.get(name) match {
+          case Some(c) =>
+            HTML.span(c.toString, html)
+          case None =>
+            if (document_span_elements(name)) HTML.span(name, html)
+            else XML.Elem(markup, html)
+        }
       case XML.Text(text) =>
         XML.Text(Symbol.decode(text))
     }