report Markdown document structure;
authorwenzelm
Thu Oct 15 15:06:03 2015 +0200 (2015-10-15 ago)
changeset 614494f31f79cf2d1
parent 61448 25e40e78f6d4
child 61450 239a04ec2d4c
report Markdown document structure;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/markdown.ML
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Thu Oct 15 13:48:47 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Thu Oct 15 15:06:03 2015 +0200
     1.3 @@ -117,6 +117,9 @@
     1.4    val document_antiquotation_optionN: string
     1.5    val paragraphN: string val paragraph: T
     1.6    val text_foldN: string val text_fold: T
     1.7 +  val markdown_paragraphN: string val markdown_paragraph: T
     1.8 +  val markdown_listN: string val markdown_list: string -> T
     1.9 +  val markdown_itemN: string val markdown_item: int -> T
    1.10    val inputN: string val input: bool -> Properties.T -> T
    1.11    val command_keywordN: string val command_keyword: T
    1.12    val commandN: string val command: T
    1.13 @@ -465,6 +468,13 @@
    1.14  val (text_foldN, text_fold) = markup_elem "text_fold";
    1.15  
    1.16  
    1.17 +(* Markdown document structure *)
    1.18 +
    1.19 +val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
    1.20 +val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
    1.21 +val (markdown_itemN, markdown_item) = markup_int "markdown_item" "depth";
    1.22 +
    1.23 +
    1.24  (* formal input *)
    1.25  
    1.26  val inputN = "input";
     2.1 --- a/src/Pure/PIDE/markup.scala	Thu Oct 15 13:48:47 2015 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Thu Oct 15 15:06:03 2015 +0200
     2.3 @@ -243,6 +243,13 @@
     2.4    val TEXT_FOLD = "text_fold"
     2.5  
     2.6  
     2.7 +  /* Markdown document structure */
     2.8 +
     2.9 +  val MARKDOWN_PARAGRAPH = "markdown_paragraph"
    2.10 +  val Markdown_List = new Markup_String("markdown_list", "kind")
    2.11 +  val Markdown_Item = new Markup_Int("markdown_item", "depth")
    2.12 +
    2.13 +
    2.14    /* ML */
    2.15  
    2.16    val ML_KEYWORD1 = "ML_keyword1"
     3.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 13:48:47 2015 +0200
     3.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 15:06:03 2015 +0200
     3.3 @@ -20,6 +20,7 @@
     3.4  signature MARKDOWN =
     3.5  sig
     3.6    datatype kind = Itemize | Enumerate | Description
     3.7 +  val print_kind: kind -> string
     3.8    type marker = {indent: int, kind: kind}
     3.9    type line
    3.10    val line_content: line -> Antiquote.text_antiquote list
    3.11 @@ -28,6 +29,7 @@
    3.12    datatype block = Paragraph of line list | List of marker * block list
    3.13    val read_lines: line list -> block list
    3.14    val read: Input.source -> block list
    3.15 +  val reports: block list -> Position.report list
    3.16  end;
    3.17  
    3.18  structure Markdown: MARKDOWN =
    3.19 @@ -36,6 +38,11 @@
    3.20  (* document lines *)
    3.21  
    3.22  datatype kind = Itemize | Enumerate | Description;
    3.23 +
    3.24 +fun print_kind Itemize = "itemize"
    3.25 +  | print_kind Enumerate = "enumerate"
    3.26 +  | print_kind Description = "description";
    3.27 +
    3.28  type marker = {indent: int, kind: kind};
    3.29  
    3.30  datatype line =
    3.31 @@ -70,13 +77,14 @@
    3.32  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    3.33  
    3.34  val scan_marker =
    3.35 -  Scan.many is_space --
    3.36 +  Scan.many is_space -- Symbol_Pos.scan_pos --
    3.37    (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    3.38     Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    3.39 -   Symbol_Pos.$$ "\<^descr>" >> K Description) >> (fn (a, b) => {indent = length a, kind = b});
    3.40 +   Symbol_Pos.$$ "\<^descr>" >> K Description)
    3.41 +  >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
    3.42  
    3.43  fun read_marker (Antiquote.Text ss :: _) =
    3.44 -      #1 (Scan.finite Symbol_Pos.stopper (Scan.option (scan_marker -- Symbol_Pos.scan_pos)) ss)
    3.45 +      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
    3.46    | read_marker _ = NONE;
    3.47  
    3.48  in
    3.49 @@ -140,4 +148,22 @@
    3.50  
    3.51  val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
    3.52  
    3.53 +
    3.54 +(* PIDE reports *)
    3.55 +
    3.56 +local
    3.57 +
    3.58 +fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
    3.59 +      Position.is_reported pos ? cons (pos, Markup.markdown_item depth)
    3.60 +  | line_reports _ _ = I;
    3.61 +
    3.62 +fun block_reports depth (Paragraph lines) = fold (line_reports depth) lines
    3.63 +  | block_reports depth (List (_, body)) = fold (block_reports (depth + 1)) body;
    3.64 +
    3.65 +in
    3.66 +
    3.67 +fun reports blocks = fold (block_reports 0) blocks [];
    3.68 +
    3.69  end;
    3.70 +
    3.71 +end;
     4.1 --- a/src/Tools/jEdit/etc/options	Thu Oct 15 13:48:47 2015 +0200
     4.2 +++ b/src/Tools/jEdit/etc/options	Thu Oct 15 15:06:03 2015 +0200
     4.3 @@ -133,6 +133,11 @@
     4.4  option inner_comment_color : string = "CC0000FF"
     4.5  option dynamic_color : string = "7BA428FF"
     4.6  
     4.7 +option markdown_item_color1 : string = "DAFEDAFF"
     4.8 +option markdown_item_color2 : string = "FFF0CCFF"
     4.9 +option markdown_item_color3 : string = "E7E7FFFF"
    4.10 +option markdown_item_color4 : string = "FFE0F0FF"
    4.11 +
    4.12  
    4.13  section "Icons"
    4.14  
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 13:48:47 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 15:06:03 2015 +0200
     5.3 @@ -204,7 +204,7 @@
     5.4        Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
     5.5        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
     5.6        Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
     5.7 -      Markup.BAD + Markup.INTENSIFY ++ active_elements
     5.8 +      Markup.BAD + Markup.INTENSIFY + Markup.Markdown_Item.name ++ active_elements
     5.9  
    5.10    private val foreground_elements =
    5.11      Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    5.12 @@ -282,6 +282,11 @@
    5.13    val inner_comment_color = color_value("inner_comment_color")
    5.14    val dynamic_color = color_value("dynamic_color")
    5.15  
    5.16 +  val markdown_item_color1 = color_value("markdown_item_color1")
    5.17 +  val markdown_item_color2 = color_value("markdown_item_color2")
    5.18 +  val markdown_item_color3 = color_value("markdown_item_color3")
    5.19 +  val markdown_item_color4 = color_value("markdown_item_color4")
    5.20 +
    5.21  
    5.22    /* completion */
    5.23  
    5.24 @@ -679,6 +684,15 @@
    5.25                    Some((Nil, Some(bad_color)))
    5.26                  case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    5.27                    Some((Nil, Some(intensify_color)))
    5.28 +                case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
    5.29 +                  val color =
    5.30 +                    depth match {
    5.31 +                      case 1 => markdown_item_color1
    5.32 +                      case 2 => markdown_item_color2
    5.33 +                      case 3 => markdown_item_color3
    5.34 +                      case _ => markdown_item_color4
    5.35 +                    }
    5.36 +                  Some((Nil, Some(color)))
    5.37                  case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    5.38                    command_states.collectFirst(
    5.39                      { case st if st.results.defined(serial) => st.results.get(serial).get }) match