--- a/src/Pure/PIDE/markup.ML Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Nov 21 14:33:30 2018 +0100
@@ -96,7 +96,6 @@
val delimiterN: string val delimiter: T
val inner_stringN: string val inner_string: T
val inner_cartoucheN: string val inner_cartouche: T
- val inner_commentN: string val inner_comment: T
val token_rangeN: string val token_range: T
val sortingN: string val sorting: T
val typingN: string val typing: T
@@ -145,6 +144,9 @@
val quasi_keywordN: string val quasi_keyword: T
val improperN: string val improper: T
val operatorN: string val operator: T
+ val comment1N: string val comment1: T
+ val comment2N: string val comment2: T
+ val comment3N: string val comment3: T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -440,7 +442,6 @@
val (delimiterN, delimiter) = markup_elem "delimiter";
val (inner_stringN, inner_string) = markup_elem "inner_string";
val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
-val (inner_commentN, inner_comment) = markup_elem "inner_comment";
val (token_rangeN, token_range) = markup_elem "token_range";
@@ -524,6 +525,13 @@
val (commentN, comment) = markup_elem "comment";
+(* comments *)
+
+val (comment1N, comment1) = markup_elem "comment1";
+val (comment2N, comment2) = markup_elem "comment2";
+val (comment3N, comment3) = markup_elem "comment3";
+
+
(* timing *)
val elapsedN = "elapsed";
--- a/src/Pure/PIDE/markup.scala Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Pure/PIDE/markup.scala Wed Nov 21 14:33:30 2018 +0100
@@ -271,7 +271,6 @@
val DELIMITER = "delimiter"
val INNER_STRING = "inner_string"
val INNER_CARTOUCHE = "inner_cartouche"
- val INNER_COMMENT = "inner_comment"
val TOKEN_RANGE = "token_range"
@@ -348,6 +347,13 @@
val COMMENT = "comment"
+ /* comments */
+
+ val COMMENT1 = "comment1"
+ val COMMENT2 = "comment2"
+ val COMMENT3 = "comment3"
+
+
/* timing */
val Elapsed = new Properties.Double("elapsed")
--- a/src/Pure/PIDE/rendering.scala Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala Wed Nov 21 14:33:30 2018 +0100
@@ -40,7 +40,7 @@
// text
val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator,
tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
- inner_cartouche, inner_comment, dynamic, class_parameter, antiquote = Value
+ inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter, antiquote = Value
val text_colors =
values -- background_colors -- foreground_colors -- message_underline_colors --
message_background_colors
@@ -125,7 +125,6 @@
Markup.VAR -> Color.`var`,
Markup.INNER_STRING -> Color.inner_quoted,
Markup.INNER_CARTOUCHE -> Color.inner_cartouche,
- Markup.INNER_COMMENT -> Color.inner_comment,
Markup.DYNAMIC_FACT -> Color.dynamic,
Markup.CLASS_PARAMETER -> Color.class_parameter,
Markup.ANTIQUOTE -> Color.antiquote,
@@ -136,7 +135,10 @@
Markup.ML_NUMERAL -> Color.inner_numeral,
Markup.ML_CHAR -> Color.inner_quoted,
Markup.ML_STRING -> Color.inner_quoted,
- Markup.ML_COMMENT -> Color.inner_comment)
+ Markup.ML_COMMENT -> Color.comment1,
+ Markup.COMMENT1 -> Color.comment1,
+ Markup.COMMENT2 -> Color.comment2,
+ Markup.COMMENT3 -> Color.comment3)
val foreground =
Map(
--- a/src/Pure/Syntax/lexicon.ML Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML Wed Nov 21 14:33:30 2018 +0100
@@ -210,7 +210,7 @@
| Str => Markup.inner_string
| String => Markup.inner_string
| Cartouche => Markup.inner_cartouche
- | Comment _ => Markup.inner_comment
+ | Comment _ => Markup.comment1
| _ => Markup.empty;
fun report_of_token tok =
--- a/src/Tools/Haskell/Haskell.thy Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy Wed Nov 21 14:33:30 2018 +0100
@@ -268,7 +268,7 @@
tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
- inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
+ inner_cartoucheN, inner_cartouche,
token_rangeN, token_range,
sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
@@ -278,7 +278,8 @@
keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
- verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
+ verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
+ comment2N, comment2, comment3N, comment3,
writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
@@ -481,9 +482,6 @@
inner_cartoucheN :: String; inner_cartouche :: T
(inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
-inner_commentN :: String; inner_comment :: T
-(inner_commentN, inner_comment) = markup_elem \<open>Markup.inner_commentN\<close>
-
token_rangeN :: String; token_range :: T
(token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
@@ -553,6 +551,18 @@
(commentN, comment) = markup_elem \<open>Markup.commentN\<close>
+{- comments -}
+
+comment1N :: String; comment1 :: T
+(comment1N, comment1) = markup_elem \<open>Markup.comment1N\<close>
+
+comment2N :: String; comment2 :: T
+(comment2N, comment2) = markup_elem \<open>Markup.comment2N\<close>
+
+comment3N :: String; comment3 :: T
+(comment3N, comment3) = markup_elem \<open>Markup.comment3N\<close>
+
+
{- messages -}
writelnN :: String; writeln :: T
--- a/src/Tools/Haskell/Markup.hs Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Tools/Haskell/Markup.hs Wed Nov 21 14:33:30 2018 +0100
@@ -33,7 +33,7 @@
tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
- inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
+ inner_cartoucheN, inner_cartouche,
token_rangeN, token_range,
sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
@@ -43,7 +43,8 @@
keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
- verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
+ verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
+ comment2N, comment2, comment3N, comment3,
writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
@@ -246,9 +247,6 @@
inner_cartoucheN :: String; inner_cartouche :: T
(inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"
-inner_commentN :: String; inner_comment :: T
-(inner_commentN, inner_comment) = markup_elem "inner_comment"
-
token_rangeN :: String; token_range :: T
(token_rangeN, token_range) = markup_elem "token_range"
@@ -318,6 +316,18 @@
(commentN, comment) = markup_elem "comment"
+{- comments -}
+
+comment1N :: String; comment1 :: T
+(comment1N, comment1) = markup_elem "comment1"
+
+comment2N :: String; comment2 :: T
+(comment2N, comment2) = markup_elem "comment2"
+
+comment3N :: String; comment3 :: T
+(comment3N, comment3) = markup_elem "comment3"
+
+
{- messages -}
writelnN :: String; writeln :: T
--- a/src/Tools/VSCode/extension/package.json Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Tools/VSCode/extension/package.json Wed Nov 21 14:33:30 2018 +0100
@@ -498,6 +498,30 @@
"type": "string",
"default": "rgba(96, 139, 78, 1.00)"
},
+ "isabelle.comment1_light_color": {
+ "type": "string",
+ "default": "rgba(129, 31, 63, 1.00)"
+ },
+ "isabelle.comment1_dark_color": {
+ "type": "string",
+ "default": "rgba(100, 102, 149, 1.00)"
+ },
+ "isabelle.comment2_light_color": {
+ "type": "string",
+ "default": "rgba(209, 105, 105, 1.00)"
+ },
+ "isabelle.comment2_dark_color": {
+ "type": "string",
+ "default": "rgba(206, 155, 120, 1.00)"
+ },
+ "isabelle.comment3_light_color": {
+ "type": "string",
+ "default": "rgba(0, 128, 0, 1.00)"
+ },
+ "isabelle.comment3_dark_color": {
+ "type": "string",
+ "default": "rgba(96, 139, 78, 1.00)"
+ },
"isabelle.dynamic_light_color": {
"type": "string",
"default": "rgba(121, 94, 38, 1.00)"
--- a/src/Tools/VSCode/extension/src/decorations.ts Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Wed Nov 21 14:33:30 2018 +0100
@@ -53,6 +53,9 @@
"inner_quoted",
"inner_cartouche",
"inner_comment",
+ "comment1",
+ "comment2",
+ "comment3",
"dynamic",
"class_parameter",
"antiquote"
--- a/src/Tools/jEdit/etc/options Tue Nov 20 13:46:13 2018 +0100
+++ b/src/Tools/jEdit/etc/options Wed Nov 21 14:33:30 2018 +0100
@@ -115,6 +115,9 @@
option quasi_keyword_color : string = "9966FFFF"
option improper_color : string = "FF5050FF"
option operator_color : string = "323232FF"
+option comment1_color : string = "CC0000FF"
+option comment2_color : string = "FF8400FF"
+option comment3_color : string = "6600CCFF"
option caret_debugger_color : string = "FF9966FF"
option caret_invisible_color : string = "50000080"
option completion_color : string = "0000FFFF"
@@ -129,7 +132,6 @@
option inner_numeral_color : string = "FF0000FF"
option inner_quoted_color : string = "FF00CCFF"
option inner_cartouche_color : string = "CC6600FF"
-option inner_comment_color : string = "CC0000FF"
option dynamic_color : string = "7BA428FF"
option class_parameter_color : string = "D2691EFF"