# HG changeset patch
# User wenzelm
# Date 1514903902 -3600
# Node ID 734a4e44b1598d186d401aca0ec484ba29114a36
# Parent  a2d7c0987f1987fdd042d51320df83abd7491d64
clarified terminology of "markdown_bullet";

diff -r a2d7c0987f19 -r 734a4e44b159 src/Pure/PIDE/markup.ML
--- 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 *)
diff -r a2d7c0987f19 -r 734a4e44b159 src/Pure/PIDE/markup.scala
--- 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 */
diff -r a2d7c0987f19 -r 734a4e44b159 src/Pure/PIDE/rendering.scala
--- 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))) =>
diff -r a2d7c0987f19 -r 734a4e44b159 src/Pure/Thy/markdown.ML
--- 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
diff -r a2d7c0987f19 -r 734a4e44b159 src/Tools/VSCode/extension/package.json
--- 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)"
                 },
diff -r a2d7c0987f19 -r 734a4e44b159 src/Tools/VSCode/extension/src/decorations.ts
--- 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 = [
diff -r a2d7c0987f19 -r 734a4e44b159 src/Tools/jEdit/etc/options
--- 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"