more comment markup;
authorwenzelm
Wed Nov 21 14:33:30 2018 +0100 (6 months ago)
changeset 69320fc221fa79741
parent 69319 baccaf89ca0d
child 69321 42b91ee343ee
more comment markup;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Pure/Syntax/lexicon.ML
src/Tools/Haskell/Haskell.thy
src/Tools/Haskell/Markup.hs
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/decorations.ts
src/Tools/jEdit/etc/options
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Nov 20 13:46:13 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Wed Nov 21 14:33:30 2018 +0100
     1.3 @@ -96,7 +96,6 @@
     1.4    val delimiterN: string val delimiter: T
     1.5    val inner_stringN: string val inner_string: T
     1.6    val inner_cartoucheN: string val inner_cartouche: T
     1.7 -  val inner_commentN: string val inner_comment: T
     1.8    val token_rangeN: string val token_range: T
     1.9    val sortingN: string val sorting: T
    1.10    val typingN: string val typing: T
    1.11 @@ -145,6 +144,9 @@
    1.12    val quasi_keywordN: string val quasi_keyword: T
    1.13    val improperN: string val improper: T
    1.14    val operatorN: string val operator: T
    1.15 +  val comment1N: string val comment1: T
    1.16 +  val comment2N: string val comment2: T
    1.17 +  val comment3N: string val comment3: T
    1.18    val elapsedN: string
    1.19    val cpuN: string
    1.20    val gcN: string
    1.21 @@ -440,7 +442,6 @@
    1.22  val (delimiterN, delimiter) = markup_elem "delimiter";
    1.23  val (inner_stringN, inner_string) = markup_elem "inner_string";
    1.24  val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
    1.25 -val (inner_commentN, inner_comment) = markup_elem "inner_comment";
    1.26  
    1.27  val (token_rangeN, token_range) = markup_elem "token_range";
    1.28  
    1.29 @@ -524,6 +525,13 @@
    1.30  val (commentN, comment) = markup_elem "comment";
    1.31  
    1.32  
    1.33 +(* comments *)
    1.34 +
    1.35 +val (comment1N, comment1) = markup_elem "comment1";
    1.36 +val (comment2N, comment2) = markup_elem "comment2";
    1.37 +val (comment3N, comment3) = markup_elem "comment3";
    1.38 +
    1.39 +
    1.40  (* timing *)
    1.41  
    1.42  val elapsedN = "elapsed";
     2.1 --- a/src/Pure/PIDE/markup.scala	Tue Nov 20 13:46:13 2018 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Wed Nov 21 14:33:30 2018 +0100
     2.3 @@ -271,7 +271,6 @@
     2.4    val DELIMITER = "delimiter"
     2.5    val INNER_STRING = "inner_string"
     2.6    val INNER_CARTOUCHE = "inner_cartouche"
     2.7 -  val INNER_COMMENT = "inner_comment"
     2.8  
     2.9    val TOKEN_RANGE = "token_range"
    2.10  
    2.11 @@ -348,6 +347,13 @@
    2.12    val COMMENT = "comment"
    2.13  
    2.14  
    2.15 +  /* comments */
    2.16 +
    2.17 +  val COMMENT1 = "comment1"
    2.18 +  val COMMENT2 = "comment2"
    2.19 +  val COMMENT3 = "comment3"
    2.20 +
    2.21 +
    2.22    /* timing */
    2.23  
    2.24    val Elapsed = new Properties.Double("elapsed")
     3.1 --- a/src/Pure/PIDE/rendering.scala	Tue Nov 20 13:46:13 2018 +0100
     3.2 +++ b/src/Pure/PIDE/rendering.scala	Wed Nov 21 14:33:30 2018 +0100
     3.3 @@ -40,7 +40,7 @@
     3.4      // text
     3.5      val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator,
     3.6        tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
     3.7 -      inner_cartouche, inner_comment, dynamic, class_parameter, antiquote = Value
     3.8 +      inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter, antiquote = Value
     3.9      val text_colors =
    3.10        values -- background_colors -- foreground_colors -- message_underline_colors --
    3.11        message_background_colors
    3.12 @@ -125,7 +125,6 @@
    3.13      Markup.VAR -> Color.`var`,
    3.14      Markup.INNER_STRING -> Color.inner_quoted,
    3.15      Markup.INNER_CARTOUCHE -> Color.inner_cartouche,
    3.16 -    Markup.INNER_COMMENT -> Color.inner_comment,
    3.17      Markup.DYNAMIC_FACT -> Color.dynamic,
    3.18      Markup.CLASS_PARAMETER -> Color.class_parameter,
    3.19      Markup.ANTIQUOTE -> Color.antiquote,
    3.20 @@ -136,7 +135,10 @@
    3.21      Markup.ML_NUMERAL -> Color.inner_numeral,
    3.22      Markup.ML_CHAR -> Color.inner_quoted,
    3.23      Markup.ML_STRING -> Color.inner_quoted,
    3.24 -    Markup.ML_COMMENT -> Color.inner_comment)
    3.25 +    Markup.ML_COMMENT -> Color.comment1,
    3.26 +    Markup.COMMENT1 -> Color.comment1,
    3.27 +    Markup.COMMENT2 -> Color.comment2,
    3.28 +    Markup.COMMENT3 -> Color.comment3)
    3.29  
    3.30    val foreground =
    3.31      Map(
     4.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Nov 20 13:46:13 2018 +0100
     4.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Nov 21 14:33:30 2018 +0100
     4.3 @@ -210,7 +210,7 @@
     4.4    | Str => Markup.inner_string
     4.5    | String => Markup.inner_string
     4.6    | Cartouche => Markup.inner_cartouche
     4.7 -  | Comment _ => Markup.inner_comment
     4.8 +  | Comment _ => Markup.comment1
     4.9    | _ => Markup.empty;
    4.10  
    4.11  fun report_of_token tok =
     5.1 --- a/src/Tools/Haskell/Haskell.thy	Tue Nov 20 13:46:13 2018 +0100
     5.2 +++ b/src/Tools/Haskell/Haskell.thy	Wed Nov 21 14:33:30 2018 +0100
     5.3 @@ -268,7 +268,7 @@
     5.4  
     5.5    tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
     5.6    numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
     5.7 -  inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
     5.8 +  inner_cartoucheN, inner_cartouche,
     5.9    token_rangeN, token_range,
    5.10    sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
    5.11  
    5.12 @@ -278,7 +278,8 @@
    5.13  
    5.14    keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
    5.15    improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
    5.16 -  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
    5.17 +  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
    5.18 +  comment2N, comment2, comment3N, comment3,
    5.19  
    5.20    writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
    5.21    warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
    5.22 @@ -481,9 +482,6 @@
    5.23  inner_cartoucheN :: String; inner_cartouche :: T
    5.24  (inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
    5.25  
    5.26 -inner_commentN :: String; inner_comment :: T
    5.27 -(inner_commentN, inner_comment) = markup_elem \<open>Markup.inner_commentN\<close>
    5.28 -
    5.29  
    5.30  token_rangeN :: String; token_range :: T
    5.31  (token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
    5.32 @@ -553,6 +551,18 @@
    5.33  (commentN, comment) = markup_elem \<open>Markup.commentN\<close>
    5.34  
    5.35  
    5.36 +{- comments -}
    5.37 +
    5.38 +comment1N :: String; comment1 :: T
    5.39 +(comment1N, comment1) = markup_elem \<open>Markup.comment1N\<close>
    5.40 +
    5.41 +comment2N :: String; comment2 :: T
    5.42 +(comment2N, comment2) = markup_elem \<open>Markup.comment2N\<close>
    5.43 +
    5.44 +comment3N :: String; comment3 :: T
    5.45 +(comment3N, comment3) = markup_elem \<open>Markup.comment3N\<close>
    5.46 +
    5.47 +
    5.48  {- messages -}
    5.49  
    5.50  writelnN :: String; writeln :: T
     6.1 --- a/src/Tools/Haskell/Markup.hs	Tue Nov 20 13:46:13 2018 +0100
     6.2 +++ b/src/Tools/Haskell/Markup.hs	Wed Nov 21 14:33:30 2018 +0100
     6.3 @@ -33,7 +33,7 @@
     6.4  
     6.5    tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
     6.6    numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
     6.7 -  inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
     6.8 +  inner_cartoucheN, inner_cartouche,
     6.9    token_rangeN, token_range,
    6.10    sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
    6.11  
    6.12 @@ -43,7 +43,8 @@
    6.13  
    6.14    keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
    6.15    improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
    6.16 -  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
    6.17 +  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1,
    6.18 +  comment2N, comment2, comment3N, comment3,
    6.19  
    6.20    writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
    6.21    warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
    6.22 @@ -246,9 +247,6 @@
    6.23  inner_cartoucheN :: String; inner_cartouche :: T
    6.24  (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"
    6.25  
    6.26 -inner_commentN :: String; inner_comment :: T
    6.27 -(inner_commentN, inner_comment) = markup_elem "inner_comment"
    6.28 -
    6.29  
    6.30  token_rangeN :: String; token_range :: T
    6.31  (token_rangeN, token_range) = markup_elem "token_range"
    6.32 @@ -318,6 +316,18 @@
    6.33  (commentN, comment) = markup_elem "comment"
    6.34  
    6.35  
    6.36 +{- comments -}
    6.37 +
    6.38 +comment1N :: String; comment1 :: T
    6.39 +(comment1N, comment1) = markup_elem "comment1"
    6.40 +
    6.41 +comment2N :: String; comment2 :: T
    6.42 +(comment2N, comment2) = markup_elem "comment2"
    6.43 +
    6.44 +comment3N :: String; comment3 :: T
    6.45 +(comment3N, comment3) = markup_elem "comment3"
    6.46 +
    6.47 +
    6.48  {- messages -}
    6.49  
    6.50  writelnN :: String; writeln :: T
     7.1 --- a/src/Tools/VSCode/extension/package.json	Tue Nov 20 13:46:13 2018 +0100
     7.2 +++ b/src/Tools/VSCode/extension/package.json	Wed Nov 21 14:33:30 2018 +0100
     7.3 @@ -498,6 +498,30 @@
     7.4                      "type": "string",
     7.5                      "default": "rgba(96, 139, 78, 1.00)"
     7.6                  },
     7.7 +                "isabelle.comment1_light_color": {
     7.8 +                    "type": "string",
     7.9 +                    "default": "rgba(129, 31, 63, 1.00)"
    7.10 +                },
    7.11 +                "isabelle.comment1_dark_color": {
    7.12 +                    "type": "string",
    7.13 +                    "default": "rgba(100, 102, 149, 1.00)"
    7.14 +                },
    7.15 +                "isabelle.comment2_light_color": {
    7.16 +                    "type": "string",
    7.17 +                    "default": "rgba(209, 105, 105, 1.00)"
    7.18 +                },
    7.19 +                "isabelle.comment2_dark_color": {
    7.20 +                    "type": "string",
    7.21 +                    "default": "rgba(206, 155, 120, 1.00)"
    7.22 +                },
    7.23 +                "isabelle.comment3_light_color": {
    7.24 +                    "type": "string",
    7.25 +                    "default": "rgba(0, 128, 0, 1.00)"
    7.26 +                },
    7.27 +                "isabelle.comment3_dark_color": {
    7.28 +                    "type": "string",
    7.29 +                    "default": "rgba(96, 139, 78, 1.00)"
    7.30 +                },
    7.31                  "isabelle.dynamic_light_color": {
    7.32                      "type": "string",
    7.33                      "default": "rgba(121, 94, 38, 1.00)"
     8.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Tue Nov 20 13:46:13 2018 +0100
     8.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Wed Nov 21 14:33:30 2018 +0100
     8.3 @@ -53,6 +53,9 @@
     8.4    "inner_quoted",
     8.5    "inner_cartouche",
     8.6    "inner_comment",
     8.7 +  "comment1",
     8.8 +  "comment2",
     8.9 +  "comment3",
    8.10    "dynamic",
    8.11    "class_parameter",
    8.12    "antiquote"
     9.1 --- a/src/Tools/jEdit/etc/options	Tue Nov 20 13:46:13 2018 +0100
     9.2 +++ b/src/Tools/jEdit/etc/options	Wed Nov 21 14:33:30 2018 +0100
     9.3 @@ -115,6 +115,9 @@
     9.4  option quasi_keyword_color : string = "9966FFFF"
     9.5  option improper_color : string = "FF5050FF"
     9.6  option operator_color : string = "323232FF"
     9.7 +option comment1_color : string = "CC0000FF"
     9.8 +option comment2_color : string = "FF8400FF"
     9.9 +option comment3_color : string = "6600CCFF"
    9.10  option caret_debugger_color : string = "FF9966FF"
    9.11  option caret_invisible_color : string = "50000080"
    9.12  option completion_color : string = "0000FFFF"
    9.13 @@ -129,7 +132,6 @@
    9.14  option inner_numeral_color : string = "FF0000FF"
    9.15  option inner_quoted_color : string = "FF00CCFF"
    9.16  option inner_cartouche_color : string = "CC6600FF"
    9.17 -option inner_comment_color : string = "CC0000FF"
    9.18  option dynamic_color : string = "7BA428FF"
    9.19  option class_parameter_color : string = "D2691EFF"
    9.20