# HG changeset patch # User wenzelm # Date 1542807210 -3600 # Node ID fc221fa797416f1446c265cbcc4894bfe96f0db4 # Parent baccaf89ca0d5a73c8d7b2192cdeaba1885592a5 more comment markup; diff -r baccaf89ca0d -r fc221fa79741 src/Pure/PIDE/markup.ML --- 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"; diff -r baccaf89ca0d -r fc221fa79741 src/Pure/PIDE/markup.scala --- 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") diff -r baccaf89ca0d -r fc221fa79741 src/Pure/PIDE/rendering.scala --- 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( diff -r baccaf89ca0d -r fc221fa79741 src/Pure/Syntax/lexicon.ML --- 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 = diff -r baccaf89ca0d -r fc221fa79741 src/Tools/Haskell/Haskell.thy --- 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 \Markup.inner_cartoucheN\ -inner_commentN :: String; inner_comment :: T -(inner_commentN, inner_comment) = markup_elem \Markup.inner_commentN\ - token_rangeN :: String; token_range :: T (token_rangeN, token_range) = markup_elem \Markup.token_rangeN\ @@ -553,6 +551,18 @@ (commentN, comment) = markup_elem \Markup.commentN\ +{- comments -} + +comment1N :: String; comment1 :: T +(comment1N, comment1) = markup_elem \Markup.comment1N\ + +comment2N :: String; comment2 :: T +(comment2N, comment2) = markup_elem \Markup.comment2N\ + +comment3N :: String; comment3 :: T +(comment3N, comment3) = markup_elem \Markup.comment3N\ + + {- messages -} writelnN :: String; writeln :: T diff -r baccaf89ca0d -r fc221fa79741 src/Tools/Haskell/Markup.hs --- 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 diff -r baccaf89ca0d -r fc221fa79741 src/Tools/VSCode/extension/package.json --- 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)" diff -r baccaf89ca0d -r fc221fa79741 src/Tools/VSCode/extension/src/decorations.ts --- 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" diff -r baccaf89ca0d -r fc221fa79741 src/Tools/jEdit/etc/options --- 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"