# HG changeset patch # User wenzelm # Date 1444914363 -7200 # Node ID 4f31f79cf2d1ba80cc21544c81a02817596249d3 # Parent 25e40e78f6d47697160dbbdbb47f873deb15bd41 report Markdown document structure; diff -r 25e40e78f6d4 -r 4f31f79cf2d1 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Oct 15 13:48:47 2015 +0200 +++ b/src/Pure/PIDE/markup.ML Thu Oct 15 15:06:03 2015 +0200 @@ -117,6 +117,9 @@ val document_antiquotation_optionN: string val paragraphN: string val paragraph: T 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 inputN: string val input: bool -> Properties.T -> T val command_keywordN: string val command_keyword: T val commandN: string val command: T @@ -465,6 +468,13 @@ val (text_foldN, text_fold) = markup_elem "text_fold"; +(* Markdown document structure *) + +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"; + + (* formal input *) val inputN = "input"; diff -r 25e40e78f6d4 -r 4f31f79cf2d1 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Oct 15 13:48:47 2015 +0200 +++ b/src/Pure/PIDE/markup.scala Thu Oct 15 15:06:03 2015 +0200 @@ -243,6 +243,13 @@ val TEXT_FOLD = "text_fold" + /* Markdown document structure */ + + val MARKDOWN_PARAGRAPH = "markdown_paragraph" + val Markdown_List = new Markup_String("markdown_list", "kind") + val Markdown_Item = new Markup_Int("markdown_item", "depth") + + /* ML */ val ML_KEYWORD1 = "ML_keyword1" diff -r 25e40e78f6d4 -r 4f31f79cf2d1 src/Pure/Thy/markdown.ML --- a/src/Pure/Thy/markdown.ML Thu Oct 15 13:48:47 2015 +0200 +++ b/src/Pure/Thy/markdown.ML Thu Oct 15 15:06:03 2015 +0200 @@ -20,6 +20,7 @@ signature MARKDOWN = sig datatype kind = Itemize | Enumerate | Description + val print_kind: kind -> string type marker = {indent: int, kind: kind} type line val line_content: line -> Antiquote.text_antiquote list @@ -28,6 +29,7 @@ datatype block = Paragraph of line list | List of marker * block list val read_lines: line list -> block list val read: Input.source -> block list + val reports: block list -> Position.report list end; structure Markdown: MARKDOWN = @@ -36,6 +38,11 @@ (* document lines *) datatype kind = Itemize | Enumerate | Description; + +fun print_kind Itemize = "itemize" + | print_kind Enumerate = "enumerate" + | print_kind Description = "description"; + type marker = {indent: int, kind: kind}; datatype line = @@ -70,13 +77,14 @@ val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false); val scan_marker = - Scan.many is_space -- + Scan.many is_space -- Symbol_Pos.scan_pos -- (Symbol_Pos.$$ "\<^item>" >> K Itemize || Symbol_Pos.$$ "\<^enum>" >> K Enumerate || - Symbol_Pos.$$ "\<^descr>" >> K Description) >> (fn (a, b) => {indent = length a, kind = b}); + Symbol_Pos.$$ "\<^descr>" >> K Description) + >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos)); fun read_marker (Antiquote.Text ss :: _) = - #1 (Scan.finite Symbol_Pos.stopper (Scan.option (scan_marker -- Symbol_Pos.scan_pos)) ss) + #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss) | read_marker _ = NONE; in @@ -140,4 +148,22 @@ val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines; + +(* PIDE reports *) + +local + +fun line_reports depth (Line {marker = SOME (_, pos), ...}) = + Position.is_reported pos ? cons (pos, Markup.markdown_item depth) + | line_reports _ _ = I; + +fun block_reports depth (Paragraph lines) = fold (line_reports depth) lines + | block_reports depth (List (_, body)) = fold (block_reports (depth + 1)) body; + +in + +fun reports blocks = fold (block_reports 0) blocks []; + end; + +end; diff -r 25e40e78f6d4 -r 4f31f79cf2d1 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Thu Oct 15 13:48:47 2015 +0200 +++ b/src/Tools/jEdit/etc/options Thu Oct 15 15:06:03 2015 +0200 @@ -133,6 +133,11 @@ option inner_comment_color : string = "CC0000FF" option dynamic_color : string = "7BA428FF" +option markdown_item_color1 : string = "DAFEDAFF" +option markdown_item_color2 : string = "FFF0CCFF" +option markdown_item_color3 : string = "E7E7FFFF" +option markdown_item_color4 : string = "FFE0F0FF" + section "Icons" diff -r 25e40e78f6d4 -r 4f31f79cf2d1 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Oct 15 13:48:47 2015 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Thu Oct 15 15:06:03 2015 +0200 @@ -204,7 +204,7 @@ Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + - Markup.BAD + Markup.INTENSIFY ++ active_elements + Markup.BAD + Markup.INTENSIFY + Markup.Markdown_Item.name ++ active_elements private val foreground_elements = Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, @@ -282,6 +282,11 @@ val inner_comment_color = color_value("inner_comment_color") val dynamic_color = color_value("dynamic_color") + val markdown_item_color1 = color_value("markdown_item_color1") + val markdown_item_color2 = color_value("markdown_item_color2") + val markdown_item_color3 = color_value("markdown_item_color3") + val markdown_item_color4 = color_value("markdown_item_color4") + /* completion */ @@ -679,6 +684,15 @@ Some((Nil, Some(bad_color))) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((Nil, Some(intensify_color))) + case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) => + val color = + depth match { + case 1 => markdown_item_color1 + case 2 => markdown_item_color2 + case 3 => markdown_item_color3 + case _ => markdown_item_color4 + } + Some((Nil, Some(color))) case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) => command_states.collectFirst( { case st if st.results.defined(serial) => st.results.get(serial).get }) match