# HG changeset patch # User wenzelm # Date 1514919156 -3600 # Node ID 4c94ec0488c7335e683396a0e579e3cff3ede11f # Parent 706b1cf7b76d6edc1fba6e6e04bcb5c8721a665a# Parent d02208cefbdbda6f05b6022a788b091e19485e63 merged diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Pure/PIDE/markup.ML --- 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 *) diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Pure/PIDE/markup.scala --- 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 */ diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Pure/PIDE/rendering.scala --- 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))) diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Pure/Thy/markdown.ML --- 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 diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Tools/VSCode/extension/package.json --- 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)" }, diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Tools/VSCode/extension/src/decorations.ts --- 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 = [ diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Tools/jEdit/etc/options --- 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" diff -r 706b1cf7b76d -r 4c94ec0488c7 src/Tools/jEdit/src/jedit_rendering.scala --- 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,