PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
authorwenzelm
Tue Jan 02 19:52:17 2018 +0100 (17 months ago)
changeset 67323d02208cefbdb
parent 67322 734a4e44b159
child 67324 4c94ec0488c7
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Pure/Thy/markdown.ML
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue Jan 02 15:38:22 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Tue Jan 02 19:52:17 2018 +0100
     1.3 @@ -122,6 +122,7 @@
     1.4    val paragraphN: string val paragraph: T
     1.5    val text_foldN: string val text_fold: T
     1.6    val markdown_paragraphN: string val markdown_paragraph: T
     1.7 +  val markdown_itemN: string val markdown_item: T
     1.8    val markdown_listN: string val markdown_list: string -> T
     1.9    val markdown_bulletN: string val markdown_bullet: int -> T
    1.10    val inputN: string val input: bool -> Properties.T -> T
    1.11 @@ -473,6 +474,7 @@
    1.12  (* Markdown document structure *)
    1.13  
    1.14  val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
    1.15 +val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
    1.16  val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
    1.17  val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
    1.18  
     2.1 --- a/src/Pure/PIDE/markup.scala	Tue Jan 02 15:38:22 2018 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jan 02 19:52:17 2018 +0100
     2.3 @@ -296,6 +296,7 @@
     2.4    /* Markdown document structure */
     2.5  
     2.6    val MARKDOWN_PARAGRAPH = "markdown_paragraph"
     2.7 +  val MARKDOWN_ITEM = "markdown_item"
     2.8    val Markdown_List = new Markup_String("markdown_list", "kind")
     2.9    val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
    2.10  
     3.1 --- a/src/Pure/PIDE/rendering.scala	Tue Jan 02 15:38:22 2018 +0100
     3.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Jan 02 19:52:17 2018 +0100
     3.3 @@ -197,7 +197,8 @@
     3.4      Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
     3.5        Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
     3.6        Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
     3.7 -      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
     3.8 +      Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
     3.9 +      Markup.Elements(tooltip_descriptions.keySet)
    3.10  
    3.11    val tooltip_message_elements =
    3.12      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    3.13 @@ -591,6 +592,8 @@
    3.14  
    3.15            case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
    3.16              Some(info + (r0, true, XML.Text("Markdown: paragraph")))
    3.17 +          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) =>
    3.18 +            Some(info + (r0, true, XML.Text("Markdown: item")))
    3.19            case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
    3.20              Some(info + (r0, true, XML.Text("Markdown: " + kind)))
    3.21  
     4.1 --- a/src/Pure/Thy/markdown.ML	Tue Jan 02 15:38:22 2018 +0100
     4.2 +++ b/src/Pure/Thy/markdown.ML	Tue Jan 02 19:52:17 2018 +0100
     4.3 @@ -129,6 +129,9 @@
     4.4  fun block_lines (Par lines) = lines
     4.5    | block_lines (List {body, ...}) = maps block_lines body;
     4.6  
     4.7 +fun block_source (Par lines) = maps line_source lines
     4.8 +  | block_source (List {body, ...}) = maps line_source (maps block_lines body);
     4.9 +
    4.10  fun block_range (Par lines) = Antiquote.range (maps line_content lines)
    4.11    | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
    4.12  
    4.13 @@ -142,6 +145,13 @@
    4.14  
    4.15  val is_list = fn List _ => true | _ => false;
    4.16  
    4.17 +val is_item = fn Par (line :: _) => line_is_item line | _ => false;
    4.18 +
    4.19 +fun list_items [] = []
    4.20 +  | list_items (item :: rest) =
    4.21 +      let val (item_rest, rest') = take_prefix (not o is_item) rest;
    4.22 +      in (item :: item_rest) :: list_items rest' end;
    4.23 +
    4.24  
    4.25  (* read document *)
    4.26  
    4.27 @@ -193,16 +203,23 @@
    4.28  
    4.29  local
    4.30  
    4.31 +val block_pos = #1 o block_range;
    4.32 +val item_pos = #1 o Antiquote.range o maps block_source;
    4.33 +
    4.34  fun line_reports depth (Line {bullet_pos, content, ...}) =
    4.35    cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);
    4.36  
    4.37 +fun item_reports blocks =
    4.38 +  cons (item_pos blocks, Markup.markdown_item);
    4.39 +
    4.40  fun block_reports depth block =
    4.41    (case block of
    4.42      Par lines =>
    4.43 -      cons (#1 (block_range block), Markup.markdown_paragraph) #>
    4.44 +      cons (block_pos block, Markup.markdown_paragraph) #>
    4.45        fold (line_reports depth) lines
    4.46    | List {kind, body, ...} =>
    4.47 -      cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #>
    4.48 +      cons (block_pos block, Markup.markdown_list (print_kind kind)) #>
    4.49 +      fold item_reports (list_items body) #>
    4.50        fold (block_reports (depth + 1)) body);
    4.51  
    4.52  in
     5.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 02 15:38:22 2018 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 02 19:52:17 2018 +0100
     5.3 @@ -120,7 +120,7 @@
     5.4        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
     5.5        Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
     5.6        Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
     5.7 -      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
     5.8 +      Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
     5.9  
    5.10    private val hyperlink_elements =
    5.11      Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,