--- 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; }
--- 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;
--- 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";
--- 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"
--- 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;
--- 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))
}