clarified terminology of "markdown_bullet";
authorwenzelm
Tue Jan 02 15:38:22 2018 +0100 (23 months ago ago)
changeset 67322734a4e44b159
parent 67313 a2d7c0987f19
child 67323 d02208cefbdb
clarified terminology of "markdown_bullet";
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Pure/Thy/markdown.ML
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/decorations.ts
src/Tools/jEdit/etc/options
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Jan 02 13:16:32 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Tue Jan 02 15:38:22 2018 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4    val text_foldN: string val text_fold: T
     1.5    val markdown_paragraphN: string val markdown_paragraph: T
     1.6    val markdown_listN: string val markdown_list: string -> T
     1.7 -  val markdown_itemN: string val markdown_item: int -> T
     1.8 +  val markdown_bulletN: string val markdown_bullet: int -> T
     1.9    val inputN: string val input: bool -> Properties.T -> T
    1.10    val command_keywordN: string val command_keyword: T
    1.11    val commandN: string val command_properties: T -> T
    1.12 @@ -474,7 +474,7 @@
    1.13  
    1.14  val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
    1.15  val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
    1.16 -val (markdown_itemN, markdown_item) = markup_int "markdown_item" "depth";
    1.17 +val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
    1.18  
    1.19  
    1.20  (* formal input *)
     2.1 --- a/src/Pure/PIDE/markup.scala	Tue Jan 02 13:16:32 2018 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jan 02 15:38:22 2018 +0100
     2.3 @@ -297,7 +297,7 @@
     2.4  
     2.5    val MARKDOWN_PARAGRAPH = "markdown_paragraph"
     2.6    val Markdown_List = new Markup_String("markdown_list", "kind")
     2.7 -  val Markdown_Item = new Markup_Int("markdown_item", "depth")
     2.8 +  val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
     2.9  
    2.10  
    2.11    /* ML */
     3.1 --- a/src/Pure/PIDE/rendering.scala	Tue Jan 02 13:16:32 2018 +0100
     3.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Jan 02 15:38:22 2018 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4    {
     3.5      // background
     3.6      val unprocessed1, running1, bad, intensify, entity, active, active_result,
     3.7 -      markdown_item1, markdown_item2, markdown_item3, markdown_item4 = Value
     3.8 +      markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
     3.9      val background_colors = values
    3.10  
    3.11      // foreground
    3.12 @@ -187,7 +187,7 @@
    3.13        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    3.14        Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    3.15        Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    3.16 -      Markup.Markdown_Item.name ++ active_elements
    3.17 +      Markup.Markdown_Bullet.name ++ active_elements
    3.18  
    3.19    val foreground_elements = Markup.Elements(foreground.keySet)
    3.20  
    3.21 @@ -387,13 +387,13 @@
    3.22                    case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
    3.23                    case _ => None
    3.24                  }
    3.25 -              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
    3.26 +              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
    3.27                  val color =
    3.28                    depth % 4 match {
    3.29 -                    case 1 => Rendering.Color.markdown_item1
    3.30 -                    case 2 => Rendering.Color.markdown_item2
    3.31 -                    case 3 => Rendering.Color.markdown_item3
    3.32 -                    case _ => Rendering.Color.markdown_item4
    3.33 +                    case 1 => Rendering.Color.markdown_bullet1
    3.34 +                    case 2 => Rendering.Color.markdown_bullet2
    3.35 +                    case 3 => Rendering.Color.markdown_bullet3
    3.36 +                    case _ => Rendering.Color.markdown_bullet4
    3.37                    }
    3.38                  Some((Nil, Some(color)))
    3.39                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
     4.1 --- a/src/Pure/Thy/markdown.ML	Tue Jan 02 13:16:32 2018 +0100
     4.2 +++ b/src/Pure/Thy/markdown.ML	Tue Jan 02 15:38:22 2018 +0100
     4.3 @@ -60,12 +60,12 @@
     4.4      is_empty: bool,
     4.5      indent: int,
     4.6      item: kind option,
     4.7 -    item_pos: Position.T,
     4.8 +    bullet_pos: Position.T,
     4.9      content: Antiquote.text_antiquote list};
    4.10  
    4.11  val eof_line =
    4.12    Line {source = [Antiquote.Text [(Symbol.eof, Position.none)]],
    4.13 -    is_empty = false, indent = 0, item = NONE, item_pos = Position.none, content = []};
    4.14 +    is_empty = false, indent = 0, item = NONE, bullet_pos = Position.none, content = []};
    4.15  
    4.16  fun line_source (Line {source, ...}) = source;
    4.17  fun line_is_empty (Line {is_empty, ...}) = is_empty;
    4.18 @@ -100,9 +100,9 @@
    4.19        (control as Antiquote.Control {name = (name, pos), body = [], ...}) :: rest =>
    4.20          let
    4.21            val item = AList.lookup (op =) kinds name;
    4.22 -          val item_pos = if is_some item then pos else Position.none;
    4.23 +          val bullet_pos = if is_some item then pos else Position.none;
    4.24            val (_, rest') = strip_spaces (if is_some item then rest else control :: rest);
    4.25 -        in ((indent, item, item_pos), rest') end
    4.26 +        in ((indent, item, bullet_pos), rest') end
    4.27      | _ => ((indent, NONE, Position.none), source'))
    4.28    end;
    4.29  
    4.30 @@ -111,10 +111,10 @@
    4.31  fun make_line source =
    4.32    let
    4.33      val _ = check_blanks source;
    4.34 -    val ((indent, item, item_pos), content) = read_marker source;
    4.35 +    val ((indent, item, bullet_pos), content) = read_marker source;
    4.36    in
    4.37      Line {source = source, is_empty = is_empty source, indent = indent,
    4.38 -      item = item, item_pos = item_pos, content = content}
    4.39 +      item = item, bullet_pos = bullet_pos, content = content}
    4.40    end;
    4.41  
    4.42  val empty_line = make_line [];
    4.43 @@ -193,8 +193,8 @@
    4.44  
    4.45  local
    4.46  
    4.47 -fun line_reports depth (Line {item_pos, content, ...}) =
    4.48 -  cons (item_pos, Markup.markdown_item depth) #> append (text_reports content);
    4.49 +fun line_reports depth (Line {bullet_pos, content, ...}) =
    4.50 +  cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);
    4.51  
    4.52  fun block_reports depth block =
    4.53    (case block of
     5.1 --- a/src/Tools/VSCode/extension/package.json	Tue Jan 02 13:16:32 2018 +0100
     5.2 +++ b/src/Tools/VSCode/extension/package.json	Tue Jan 02 15:38:22 2018 +0100
     5.3 @@ -266,35 +266,35 @@
     5.4                      "type": "string",
     5.5                      "default": "rgba(204, 136, 0, 0.20)"
     5.6                  },
     5.7 -                "isabelle.markdown_item1_light_color": {
     5.8 +                "isabelle.markdown_bullet1_light_color": {
     5.9                      "type": "string",
    5.10                      "default": "rgba(218, 254, 218, 1.00)"
    5.11                  },
    5.12 -                "isabelle.markdown_item1_dark_color": {
    5.13 +                "isabelle.markdown_bullet1_dark_color": {
    5.14                      "type": "string",
    5.15                      "default": "rgba(5, 199, 5, 0.20)"
    5.16                  },
    5.17 -                "isabelle.markdown_item2_light_color": {
    5.18 +                "isabelle.markdown_bullet2_light_color": {
    5.19                      "type": "string",
    5.20                      "default": "rgba(255, 240, 204, 1.00)"
    5.21                  },
    5.22 -                "isabelle.markdown_item2_dark_color": {
    5.23 +                "isabelle.markdown_bullet2_dark_color": {
    5.24                      "type": "string",
    5.25                      "default": "rgba(204, 143, 0, 0.20)"
    5.26                  },
    5.27 -                "isabelle.markdown_item3_light_color": {
    5.28 +                "isabelle.markdown_bullet3_light_color": {
    5.29                      "type": "string",
    5.30                      "default": "rgba(231, 231, 255, 1.00)"
    5.31                  },
    5.32 -                "isabelle.markdown_item3_dark_color": {
    5.33 +                "isabelle.markdown_bullet3_dark_color": {
    5.34                      "type": "string",
    5.35                      "default": "rgba(0, 0, 204, 0.20)"
    5.36                  },
    5.37 -                "isabelle.markdown_item4_light_color": {
    5.38 +                "isabelle.markdown_bullet4_light_color": {
    5.39                      "type": "string",
    5.40                      "default": "rgba(255, 224, 240, 1.00)"
    5.41                  },
    5.42 -                "isabelle.markdown_item4_dark_color": {
    5.43 +                "isabelle.markdown_bullet4_dark_color": {
    5.44                      "type": "string",
    5.45                      "default": "rgba(204, 0, 105, 0.20)"
    5.46                  },
     6.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Tue Jan 02 13:16:32 2018 +0100
     6.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue Jan 02 15:38:22 2018 +0100
     6.3 @@ -17,10 +17,10 @@
     6.4    "intensify",
     6.5    "quoted",
     6.6    "antiquoted",
     6.7 -  "markdown_item1",
     6.8 -  "markdown_item2",
     6.9 -  "markdown_item3",
    6.10 -  "markdown_item4"
    6.11 +  "markdown_bullet1",
    6.12 +  "markdown_bullet2",
    6.13 +  "markdown_bullet3",
    6.14 +  "markdown_bullet4"
    6.15  ]
    6.16  
    6.17  const foreground_colors = [
     7.1 --- a/src/Tools/jEdit/etc/options	Tue Jan 02 13:16:32 2018 +0100
     7.2 +++ b/src/Tools/jEdit/etc/options	Tue Jan 02 15:38:22 2018 +0100
     7.3 @@ -132,10 +132,10 @@
     7.4  option dynamic_color : string = "7BA428FF"
     7.5  option class_parameter_color : string = "D2691EFF"
     7.6  
     7.7 -option markdown_item1_color : string = "DAFEDAFF"
     7.8 -option markdown_item2_color : string = "FFF0CCFF"
     7.9 -option markdown_item3_color : string = "E7E7FFFF"
    7.10 -option markdown_item4_color : string = "FFE0F0FF"
    7.11 +option markdown_bullet1_color : string = "DAFEDAFF"
    7.12 +option markdown_bullet2_color : string = "FFF0CCFF"
    7.13 +option markdown_bullet3_color : string = "E7E7FFFF"
    7.14 +option markdown_bullet4_color : string = "FFE0F0FF"
    7.15  
    7.16  
    7.17  section "Icons"