--- 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]})];
--- 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";
--- 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"
--- 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,
--- 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));
--- 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) =
--- 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)" }
}
}
},
--- 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 = [
--- 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"