# HG changeset patch
# User wenzelm
# Date 1497291880 -7200
# Node ID 408a5325379c82b277cb2af82970452b4fd3b0fb
# Parent  4329cc78c2a1322ab37bb89eae4ebe3f84f9ec04
tuned rendering;

diff -r 4329cc78c2a1 -r 408a5325379c etc/isabelle.css
--- a/etc/isabelle.css	Mon Jun 12 20:06:55 2017 +0200
+++ b/etc/isabelle.css	Mon Jun 12 20:24:40 2017 +0200
@@ -66,6 +66,8 @@
 .comment        { color: #CC0000; }
 .improper       { color: #FF5050; }
 .bad            { background-color: #FF6A6A; }
+.quoted         { background-color: rgba(139,139,139,0.05); }
+.antiquoted     { background-color: rgba(255,200,50,0.1); }
 
 
 /* message background */
diff -r 4329cc78c2a1 -r 408a5325379c src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Mon Jun 12 20:06:55 2017 +0200
+++ b/src/Pure/Thy/present.scala	Mon Jun 12 20:24:40 2017 +0200
@@ -104,9 +104,9 @@
   /* theory document */
 
   private val document_span_elements =
-    Markup.Elements(Rendering.text_color.keySet + Markup.NUMERAL + Markup.COMMENT)
+    Rendering.foreground_elements ++ Rendering.text_color_elements + Markup.NUMERAL + Markup.COMMENT
 
-  def make_html(xml: XML.Body): XML.Body =
+  private 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))
@@ -119,12 +119,9 @@
             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)
+        Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
+          case Some(c) => HTML.span(c.toString, html)
+          case None => HTML.span(name, html)
         }
       case XML.Text(text) =>
         XML.Text(Symbol.decode(text))