--- a/src/Pure/PIDE/markup.ML Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Jan 02 19:52:36 2018 +0100
@@ -122,8 +122,9 @@
val paragraphN: string val paragraph: T
val text_foldN: string val text_fold: T
val markdown_paragraphN: string val markdown_paragraph: T
+ val markdown_itemN: string val markdown_item: T
val markdown_listN: string val markdown_list: string -> T
- val markdown_itemN: string val markdown_item: int -> T
+ val markdown_bulletN: string val markdown_bullet: int -> T
val inputN: string val input: bool -> Properties.T -> T
val command_keywordN: string val command_keyword: T
val commandN: string val command_properties: T -> T
@@ -473,8 +474,9 @@
(* Markdown document structure *)
val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
+val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
-val (markdown_itemN, markdown_item) = markup_int "markdown_item" "depth";
+val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
(* formal input *)
--- a/src/Pure/PIDE/markup.scala Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Jan 02 19:52:36 2018 +0100
@@ -296,8 +296,9 @@
/* Markdown document structure */
val MARKDOWN_PARAGRAPH = "markdown_paragraph"
+ val MARKDOWN_ITEM = "markdown_item"
val Markdown_List = new Markup_String("markdown_list", "kind")
- val Markdown_Item = new Markup_Int("markdown_item", "depth")
+ val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
/* ML */
--- a/src/Pure/PIDE/rendering.scala Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala Tue Jan 02 19:52:36 2018 +0100
@@ -20,7 +20,7 @@
{
// background
val unprocessed1, running1, bad, intensify, entity, active, active_result,
- markdown_item1, markdown_item2, markdown_item3, markdown_item4 = Value
+ markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
val background_colors = values
// foreground
@@ -187,7 +187,7 @@
Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
- Markup.Markdown_Item.name ++ active_elements
+ Markup.Markdown_Bullet.name ++ active_elements
val foreground_elements = Markup.Elements(foreground.keySet)
@@ -197,7 +197,8 @@
Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
- Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
+ Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
+ Markup.Elements(tooltip_descriptions.keySet)
val tooltip_message_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
@@ -387,13 +388,13 @@
case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
case _ => None
}
- case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
+ case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
val color =
depth % 4 match {
- case 1 => Rendering.Color.markdown_item1
- case 2 => Rendering.Color.markdown_item2
- case 3 => Rendering.Color.markdown_item3
- case _ => Rendering.Color.markdown_item4
+ case 1 => Rendering.Color.markdown_bullet1
+ case 2 => Rendering.Color.markdown_bullet2
+ case 3 => Rendering.Color.markdown_bullet3
+ case _ => Rendering.Color.markdown_bullet4
}
Some((Nil, Some(color)))
case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
@@ -591,6 +592,8 @@
case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
Some(info + (r0, true, XML.Text("Markdown: paragraph")))
+ case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) =>
+ Some(info + (r0, true, XML.Text("Markdown: item")))
case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
Some(info + (r0, true, XML.Text("Markdown: " + kind)))
--- a/src/Pure/Thy/markdown.ML Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Pure/Thy/markdown.ML Tue Jan 02 19:52:36 2018 +0100
@@ -60,12 +60,12 @@
is_empty: bool,
indent: int,
item: kind option,
- item_pos: Position.T,
+ bullet_pos: Position.T,
content: Antiquote.text_antiquote list};
val eof_line =
Line {source = [Antiquote.Text [(Symbol.eof, Position.none)]],
- is_empty = false, indent = 0, item = NONE, item_pos = Position.none, content = []};
+ is_empty = false, indent = 0, item = NONE, bullet_pos = Position.none, content = []};
fun line_source (Line {source, ...}) = source;
fun line_is_empty (Line {is_empty, ...}) = is_empty;
@@ -100,9 +100,9 @@
(control as Antiquote.Control {name = (name, pos), body = [], ...}) :: rest =>
let
val item = AList.lookup (op =) kinds name;
- val item_pos = if is_some item then pos else Position.none;
+ val bullet_pos = if is_some item then pos else Position.none;
val (_, rest') = strip_spaces (if is_some item then rest else control :: rest);
- in ((indent, item, item_pos), rest') end
+ in ((indent, item, bullet_pos), rest') end
| _ => ((indent, NONE, Position.none), source'))
end;
@@ -111,10 +111,10 @@
fun make_line source =
let
val _ = check_blanks source;
- val ((indent, item, item_pos), content) = read_marker source;
+ val ((indent, item, bullet_pos), content) = read_marker source;
in
Line {source = source, is_empty = is_empty source, indent = indent,
- item = item, item_pos = item_pos, content = content}
+ item = item, bullet_pos = bullet_pos, content = content}
end;
val empty_line = make_line [];
@@ -129,6 +129,9 @@
fun block_lines (Par lines) = lines
| block_lines (List {body, ...}) = maps block_lines body;
+fun block_source (Par lines) = maps line_source lines
+ | block_source (List {body, ...}) = maps line_source (maps block_lines body);
+
fun block_range (Par lines) = Antiquote.range (maps line_content lines)
| block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
@@ -142,6 +145,13 @@
val is_list = fn List _ => true | _ => false;
+val is_item = fn Par (line :: _) => line_is_item line | _ => false;
+
+fun list_items [] = []
+ | list_items (item :: rest) =
+ let val (item_rest, rest') = take_prefix (not o is_item) rest;
+ in (item :: item_rest) :: list_items rest' end;
+
(* read document *)
@@ -193,16 +203,23 @@
local
-fun line_reports depth (Line {item_pos, content, ...}) =
- cons (item_pos, Markup.markdown_item depth) #> append (text_reports content);
+val block_pos = #1 o block_range;
+val item_pos = #1 o Antiquote.range o maps block_source;
+
+fun line_reports depth (Line {bullet_pos, content, ...}) =
+ cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);
+
+fun item_reports blocks =
+ cons (item_pos blocks, Markup.markdown_item);
fun block_reports depth block =
(case block of
Par lines =>
- cons (#1 (block_range block), Markup.markdown_paragraph) #>
+ cons (block_pos block, Markup.markdown_paragraph) #>
fold (line_reports depth) lines
| List {kind, body, ...} =>
- cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #>
+ cons (block_pos block, Markup.markdown_list (print_kind kind)) #>
+ fold item_reports (list_items body) #>
fold (block_reports (depth + 1)) body);
in
--- a/src/Tools/VSCode/extension/package.json Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Tools/VSCode/extension/package.json Tue Jan 02 19:52:36 2018 +0100
@@ -266,35 +266,35 @@
"type": "string",
"default": "rgba(204, 136, 0, 0.20)"
},
- "isabelle.markdown_item1_light_color": {
+ "isabelle.markdown_bullet1_light_color": {
"type": "string",
"default": "rgba(218, 254, 218, 1.00)"
},
- "isabelle.markdown_item1_dark_color": {
+ "isabelle.markdown_bullet1_dark_color": {
"type": "string",
"default": "rgba(5, 199, 5, 0.20)"
},
- "isabelle.markdown_item2_light_color": {
+ "isabelle.markdown_bullet2_light_color": {
"type": "string",
"default": "rgba(255, 240, 204, 1.00)"
},
- "isabelle.markdown_item2_dark_color": {
+ "isabelle.markdown_bullet2_dark_color": {
"type": "string",
"default": "rgba(204, 143, 0, 0.20)"
},
- "isabelle.markdown_item3_light_color": {
+ "isabelle.markdown_bullet3_light_color": {
"type": "string",
"default": "rgba(231, 231, 255, 1.00)"
},
- "isabelle.markdown_item3_dark_color": {
+ "isabelle.markdown_bullet3_dark_color": {
"type": "string",
"default": "rgba(0, 0, 204, 0.20)"
},
- "isabelle.markdown_item4_light_color": {
+ "isabelle.markdown_bullet4_light_color": {
"type": "string",
"default": "rgba(255, 224, 240, 1.00)"
},
- "isabelle.markdown_item4_dark_color": {
+ "isabelle.markdown_bullet4_dark_color": {
"type": "string",
"default": "rgba(204, 0, 105, 0.20)"
},
--- a/src/Tools/VSCode/extension/src/decorations.ts Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Tue Jan 02 19:52:36 2018 +0100
@@ -17,10 +17,10 @@
"intensify",
"quoted",
"antiquoted",
- "markdown_item1",
- "markdown_item2",
- "markdown_item3",
- "markdown_item4"
+ "markdown_bullet1",
+ "markdown_bullet2",
+ "markdown_bullet3",
+ "markdown_bullet4"
]
const foreground_colors = [
--- a/src/Tools/jEdit/etc/options Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Tools/jEdit/etc/options Tue Jan 02 19:52:36 2018 +0100
@@ -132,10 +132,10 @@
option dynamic_color : string = "7BA428FF"
option class_parameter_color : string = "D2691EFF"
-option markdown_item1_color : string = "DAFEDAFF"
-option markdown_item2_color : string = "FFF0CCFF"
-option markdown_item3_color : string = "E7E7FFFF"
-option markdown_item4_color : string = "FFE0F0FF"
+option markdown_bullet1_color : string = "DAFEDAFF"
+option markdown_bullet2_color : string = "FFF0CCFF"
+option markdown_bullet3_color : string = "E7E7FFFF"
+option markdown_bullet4_color : string = "FFE0F0FF"
section "Icons"
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Jan 02 17:38:20 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Jan 02 19:52:36 2018 +0100
@@ -120,7 +120,7 @@
Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
- Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
+ Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
private val hyperlink_elements =
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,