# HG changeset patch
# User wenzelm
# Date 1553444664 -3600
# Node ID da5e7278286b0616f4679e7ebdedc00b96b2c1fc
# Parent  699ffc7cbab8852e7b48fb6d39eb211487fa4e60
more markup for various text kinds, notably for nested formal comments;

diff -r 699ffc7cbab8 -r da5e7278286b src/Pure/General/comment.ML
--- a/src/Pure/General/comment.ML	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Pure/General/comment.ML	Sun Mar 24 17:24:24 2019 +0100
@@ -28,13 +28,13 @@
 val kinds =
   [(Comment,
      {symbol = Symbol.comment, blanks = true,
-      markups = [Markup.language_document true]}),
+      markups = [Markup.language_document true, Markup.plain_text]}),
    (Cancel,
      {symbol = Symbol.cancel, blanks = false,
-      markups = [Markup.language_text true]}),
+      markups = [Markup.language_text true, Markup.raw_text]}),
    (Latex,
      {symbol = Symbol.latex, blanks = false,
-      markups = [Markup.language_latex true, Markup.no_words]}),
+      markups = [Markup.language_latex true, Markup.no_words, Markup.raw_text]}),
    (Marker,
      {symbol = Symbol.marker, blanks = false,
       markups = [Markup.language_document_marker]})];
diff -r 699ffc7cbab8 -r da5e7278286b src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Mar 24 17:24:24 2019 +0100
@@ -128,6 +128,8 @@
   val ML_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
+  val raw_textN: string val raw_text: T
+  val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
   val markdown_paragraphN: string val markdown_paragraph: T
@@ -510,6 +512,12 @@
 val document_antiquotation_optionN = "document_antiquotation_option";
 
 
+(* text kind *)
+
+val (raw_textN, raw_text) = markup_elem "raw_text";
+val (plain_textN, plain_text) = markup_elem "plain_text";
+
+
 (* text structure *)
 
 val (paragraphN, paragraph) = markup_elem "paragraph";
diff -r 699ffc7cbab8 -r da5e7278286b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Pure/PIDE/markup.scala	Sun Mar 24 17:24:24 2019 +0100
@@ -304,6 +304,12 @@
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
+  /* text kind */
+
+  val RAW_TEXT = "raw_text"
+  val PLAIN_TEXT = "plain_text"
+
+
   /* text structure */
 
   val PARAGRAPH = "paragraph"
diff -r 699ffc7cbab8 -r da5e7278286b src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Mar 24 17:24:24 2019 +0100
@@ -40,7 +40,8 @@
     // text
     val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator,
       tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
-      inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter, antiquote = Value
+      inner_cartouche, comment1, comment2, comment3, dynamic, class_parameter,
+      antiquote, raw_text, plain_text = Value
     val text_colors =
       values -- background_colors -- foreground_colors -- message_underline_colors --
       message_background_colors
@@ -128,6 +129,8 @@
     Markup.DYNAMIC_FACT -> Color.dynamic,
     Markup.CLASS_PARAMETER -> Color.class_parameter,
     Markup.ANTIQUOTE -> Color.antiquote,
+    Markup.RAW_TEXT -> Color.raw_text,
+    Markup.PLAIN_TEXT -> Color.plain_text,
     Markup.ML_KEYWORD1 -> Color.keyword1,
     Markup.ML_KEYWORD2 -> Color.keyword2,
     Markup.ML_KEYWORD3 -> Color.keyword3,
diff -r 699ffc7cbab8 -r da5e7278286b src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Sun Mar 24 17:24:24 2019 +0100
@@ -151,8 +151,11 @@
 local
 
 fun report_text ctxt text =
-  Context_Position.report ctxt (Input.pos_of text)
-    (Markup.language_text (Input.is_delimited text));
+  let val pos = Input.pos_of text in
+    Context_Position.reports ctxt
+      [(pos, Markup.language_text (Input.is_delimited text)),
+       (pos, Markup.raw_text)]
+  end;
 
 fun prepare_text ctxt =
   Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
@@ -246,9 +249,11 @@
   (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
+        val pos = Input.pos_of text;
         val _ =
-          Context_Position.report ctxt (Input.pos_of text)
-            (Markup.language_verbatim (Input.is_delimited text));
+          Context_Position.reports ctxt
+            [(pos, Markup.language_verbatim (Input.is_delimited text)),
+             (pos, Markup.raw_text)];
       in #1 (Input.source_content text) end));
 
 
diff -r 699ffc7cbab8 -r da5e7278286b src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Pure/pure_syn.ML	Sun Mar 24 17:24:24 2019 +0100
@@ -20,9 +20,11 @@
 fun output_document state markdown txt =
   let
     val ctxt = Toplevel.presentation_context state;
+    val pos = Input.pos_of txt;
     val _ =
-      Context_Position.report ctxt
-        (Input.pos_of txt) (Markup.language_document (Input.is_delimited txt));
+      Context_Position.reports ctxt
+        [(pos, Markup.language_document (Input.is_delimited txt)),
+         (pos, Markup.plain_text)];
   in Thy_Output.output_document ctxt markdown txt end;
 
 fun document_command markdown (loc, txt) =
diff -r 699ffc7cbab8 -r da5e7278286b src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Tools/VSCode/extension/package.json	Sun Mar 24 17:24:24 2019 +0100
@@ -299,7 +299,11 @@
                 "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
                 "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
                 "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
-                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }
+                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" },
+                "isabelle.raw_text_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
+                "isabelle.raw_text_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" },
+                "isabelle.plain_text_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
+                "isabelle.plain_text_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }
             }
         }
     },
diff -r 699ffc7cbab8 -r da5e7278286b src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sun Mar 24 17:24:24 2019 +0100
@@ -57,7 +57,9 @@
   "comment3",
   "dynamic",
   "class_parameter",
-  "antiquote"
+  "antiquote",
+  "raw_text",
+  "plain_text"
 ]
 
 const text_overview_colors = [
diff -r 699ffc7cbab8 -r da5e7278286b src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sun Mar 24 17:23:48 2019 +0100
+++ b/src/Tools/jEdit/etc/options	Sun Mar 24 17:24:24 2019 +0100
@@ -107,6 +107,8 @@
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
 option antiquote_color : string = "6600CCFF"
+option raw_text_color : string = "6600CCFF"
+option plain_text_color : string = "CC6600FF"
 option highlight_color : string = "50505032"
 option hyperlink_color : string = "000000FF"
 option active_color : string = "DCDCDCFF"