more markup for various text kinds, notably for nested formal comments;
authorwenzelm
Sun Mar 24 17:24:24 2019 +0100 (4 weeks ago)
changeset 69965da5e7278286b
parent 69964 699ffc7cbab8
child 69966 cba5b866c633
more markup for various text kinds, notably for nested formal comments;
src/Pure/General/comment.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Pure/Thy/document_antiquotations.ML
src/Pure/pure_syn.ML
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/decorations.ts
src/Tools/jEdit/etc/options
     1.1 --- a/src/Pure/General/comment.ML	Sun Mar 24 17:23:48 2019 +0100
     1.2 +++ b/src/Pure/General/comment.ML	Sun Mar 24 17:24:24 2019 +0100
     1.3 @@ -28,13 +28,13 @@
     1.4  val kinds =
     1.5    [(Comment,
     1.6       {symbol = Symbol.comment, blanks = true,
     1.7 -      markups = [Markup.language_document true]}),
     1.8 +      markups = [Markup.language_document true, Markup.plain_text]}),
     1.9     (Cancel,
    1.10       {symbol = Symbol.cancel, blanks = false,
    1.11 -      markups = [Markup.language_text true]}),
    1.12 +      markups = [Markup.language_text true, Markup.raw_text]}),
    1.13     (Latex,
    1.14       {symbol = Symbol.latex, blanks = false,
    1.15 -      markups = [Markup.language_latex true, Markup.no_words]}),
    1.16 +      markups = [Markup.language_latex true, Markup.no_words, Markup.raw_text]}),
    1.17     (Marker,
    1.18       {symbol = Symbol.marker, blanks = false,
    1.19        markups = [Markup.language_document_marker]})];
     2.1 --- a/src/Pure/PIDE/markup.ML	Sun Mar 24 17:23:48 2019 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 24 17:24:24 2019 +0100
     2.3 @@ -128,6 +128,8 @@
     2.4    val ML_antiquotationN: string
     2.5    val document_antiquotationN: string
     2.6    val document_antiquotation_optionN: string
     2.7 +  val raw_textN: string val raw_text: T
     2.8 +  val plain_textN: string val plain_text: T
     2.9    val paragraphN: string val paragraph: T
    2.10    val text_foldN: string val text_fold: T
    2.11    val markdown_paragraphN: string val markdown_paragraph: T
    2.12 @@ -510,6 +512,12 @@
    2.13  val document_antiquotation_optionN = "document_antiquotation_option";
    2.14  
    2.15  
    2.16 +(* text kind *)
    2.17 +
    2.18 +val (raw_textN, raw_text) = markup_elem "raw_text";
    2.19 +val (plain_textN, plain_text) = markup_elem "plain_text";
    2.20 +
    2.21 +
    2.22  (* text structure *)
    2.23  
    2.24  val (paragraphN, paragraph) = markup_elem "paragraph";
     3.1 --- a/src/Pure/PIDE/markup.scala	Sun Mar 24 17:23:48 2019 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 24 17:24:24 2019 +0100
     3.3 @@ -304,6 +304,12 @@
     3.4    val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
     3.5  
     3.6  
     3.7 +  /* text kind */
     3.8 +
     3.9 +  val RAW_TEXT = "raw_text"
    3.10 +  val PLAIN_TEXT = "plain_text"
    3.11 +
    3.12 +
    3.13    /* text structure */
    3.14  
    3.15    val PARAGRAPH = "paragraph"
     4.1 --- a/src/Pure/PIDE/rendering.scala	Sun Mar 24 17:23:48 2019 +0100
     4.2 +++ b/src/Pure/PIDE/rendering.scala	Sun Mar 24 17:24:24 2019 +0100
     4.3 @@ -40,7 +40,8 @@
     4.4      // text
     4.5      val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator,
     4.6        tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
     4.7 -      inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter, antiquote = Value
     4.8 +      inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter,
     4.9 +      antiquote, raw_text, plain_text = Value
    4.10      val text_colors =
    4.11        values -- background_colors -- foreground_colors -- message_underline_colors --
    4.12        message_background_colors
    4.13 @@ -128,6 +129,8 @@
    4.14      Markup.DYNAMIC_FACT -> Color.dynamic,
    4.15      Markup.CLASS_PARAMETER -> Color.class_parameter,
    4.16      Markup.ANTIQUOTE -> Color.antiquote,
    4.17 +    Markup.RAW_TEXT -> Color.raw_text,
    4.18 +    Markup.PLAIN_TEXT -> Color.plain_text,
    4.19      Markup.ML_KEYWORD1 -> Color.keyword1,
    4.20      Markup.ML_KEYWORD2 -> Color.keyword2,
    4.21      Markup.ML_KEYWORD3 -> Color.keyword3,
     5.1 --- a/src/Pure/Thy/document_antiquotations.ML	Sun Mar 24 17:23:48 2019 +0100
     5.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Sun Mar 24 17:24:24 2019 +0100
     5.3 @@ -151,8 +151,11 @@
     5.4  local
     5.5  
     5.6  fun report_text ctxt text =
     5.7 -  Context_Position.report ctxt (Input.pos_of text)
     5.8 -    (Markup.language_text (Input.is_delimited text));
     5.9 +  let val pos = Input.pos_of text in
    5.10 +    Context_Position.reports ctxt
    5.11 +      [(pos, Markup.language_text (Input.is_delimited text)),
    5.12 +       (pos, Markup.raw_text)]
    5.13 +  end;
    5.14  
    5.15  fun prepare_text ctxt =
    5.16    Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
    5.17 @@ -246,9 +249,11 @@
    5.18    (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
    5.19      (fn ctxt => fn text =>
    5.20        let
    5.21 +        val pos = Input.pos_of text;
    5.22          val _ =
    5.23 -          Context_Position.report ctxt (Input.pos_of text)
    5.24 -            (Markup.language_verbatim (Input.is_delimited text));
    5.25 +          Context_Position.reports ctxt
    5.26 +            [(pos, Markup.language_verbatim (Input.is_delimited text)),
    5.27 +             (pos, Markup.raw_text)];
    5.28        in #1 (Input.source_content text) end));
    5.29  
    5.30  
     6.1 --- a/src/Pure/pure_syn.ML	Sun Mar 24 17:23:48 2019 +0100
     6.2 +++ b/src/Pure/pure_syn.ML	Sun Mar 24 17:24:24 2019 +0100
     6.3 @@ -20,9 +20,11 @@
     6.4  fun output_document state markdown txt =
     6.5    let
     6.6      val ctxt = Toplevel.presentation_context state;
     6.7 +    val pos = Input.pos_of txt;
     6.8      val _ =
     6.9 -      Context_Position.report ctxt
    6.10 -        (Input.pos_of txt) (Markup.language_document (Input.is_delimited txt));
    6.11 +      Context_Position.reports ctxt
    6.12 +        [(pos, Markup.language_document (Input.is_delimited txt)),
    6.13 +         (pos, Markup.plain_text)];
    6.14    in Thy_Output.output_document ctxt markdown txt end;
    6.15  
    6.16  fun document_command markdown (loc, txt) =
     7.1 --- a/src/Tools/VSCode/extension/package.json	Sun Mar 24 17:23:48 2019 +0100
     7.2 +++ b/src/Tools/VSCode/extension/package.json	Sun Mar 24 17:24:24 2019 +0100
     7.3 @@ -299,7 +299,11 @@
     7.4                  "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
     7.5                  "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
     7.6                  "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
     7.7 -                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }
     7.8 +                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" },
     7.9 +                "isabelle.raw_text_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
    7.10 +                "isabelle.raw_text_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" },
    7.11 +                "isabelle.plain_text_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
    7.12 +                "isabelle.plain_text_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }
    7.13              }
    7.14          }
    7.15      },
     8.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 24 17:23:48 2019 +0100
     8.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 24 17:24:24 2019 +0100
     8.3 @@ -57,7 +57,9 @@
     8.4    "comment3",
     8.5    "dynamic",
     8.6    "class_parameter",
     8.7 -  "antiquote"
     8.8 +  "antiquote",
     8.9 +  "raw_text",
    8.10 +  "plain_text"
    8.11  ]
    8.12  
    8.13  const text_overview_colors = [
     9.1 --- a/src/Tools/jEdit/etc/options	Sun Mar 24 17:23:48 2019 +0100
     9.2 +++ b/src/Tools/jEdit/etc/options	Sun Mar 24 17:24:24 2019 +0100
     9.3 @@ -107,6 +107,8 @@
     9.4  option quoted_color : string = "8B8B8B19"
     9.5  option antiquoted_color : string = "FFC83219"
     9.6  option antiquote_color : string = "6600CCFF"
     9.7 +option raw_text_color : string = "6600CCFF"
     9.8 +option plain_text_color : string = "CC6600FF"
     9.9  option highlight_color : string = "50505032"
    9.10  option hyperlink_color : string = "000000FF"
    9.11  option active_color : string = "DCDCDCFF"