--- a/src/Pure/PIDE/markup.ML Tue Jan 02 13:16:32 2018 +0100
+++ b/src/Pure/PIDE/markup.ML Tue Jan 02 15:38:22 2018 +0100
@@ -123,7 +123,7 @@
val text_foldN: string val text_fold: T
val markdown_paragraphN: string val markdown_paragraph: 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
@@ -474,7 +474,7 @@
val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
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 13:16:32 2018 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Jan 02 15:38:22 2018 +0100
@@ -297,7 +297,7 @@
val MARKDOWN_PARAGRAPH = "markdown_paragraph"
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 13:16:32 2018 +0100
+++ b/src/Pure/PIDE/rendering.scala Tue Jan 02 15:38:22 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)
@@ -387,13 +387,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))) =>
--- a/src/Pure/Thy/markdown.ML Tue Jan 02 13:16:32 2018 +0100
+++ b/src/Pure/Thy/markdown.ML Tue Jan 02 15:38:22 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 [];
@@ -193,8 +193,8 @@
local
-fun line_reports depth (Line {item_pos, content, ...}) =
- cons (item_pos, Markup.markdown_item depth) #> append (text_reports content);
+fun line_reports depth (Line {bullet_pos, content, ...}) =
+ cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);
fun block_reports depth block =
(case block of
--- a/src/Tools/VSCode/extension/package.json Tue Jan 02 13:16:32 2018 +0100
+++ b/src/Tools/VSCode/extension/package.json Tue Jan 02 15:38:22 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 13:16:32 2018 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Tue Jan 02 15:38:22 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 13:16:32 2018 +0100
+++ b/src/Tools/jEdit/etc/options Tue Jan 02 15:38:22 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"