src/Pure/Thy/markdown.ML
changeset 61449 4f31f79cf2d1
parent 61448 25e40e78f6d4
child 61450 239a04ec2d4c
     1.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 13:48:47 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 15:06:03 2015 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4  signature MARKDOWN =
     1.5  sig
     1.6    datatype kind = Itemize | Enumerate | Description
     1.7 +  val print_kind: kind -> string
     1.8    type marker = {indent: int, kind: kind}
     1.9    type line
    1.10    val line_content: line -> Antiquote.text_antiquote list
    1.11 @@ -28,6 +29,7 @@
    1.12    datatype block = Paragraph of line list | List of marker * block list
    1.13    val read_lines: line list -> block list
    1.14    val read: Input.source -> block list
    1.15 +  val reports: block list -> Position.report list
    1.16  end;
    1.17  
    1.18  structure Markdown: MARKDOWN =
    1.19 @@ -36,6 +38,11 @@
    1.20  (* document lines *)
    1.21  
    1.22  datatype kind = Itemize | Enumerate | Description;
    1.23 +
    1.24 +fun print_kind Itemize = "itemize"
    1.25 +  | print_kind Enumerate = "enumerate"
    1.26 +  | print_kind Description = "description";
    1.27 +
    1.28  type marker = {indent: int, kind: kind};
    1.29  
    1.30  datatype line =
    1.31 @@ -70,13 +77,14 @@
    1.32  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    1.33  
    1.34  val scan_marker =
    1.35 -  Scan.many is_space --
    1.36 +  Scan.many is_space -- Symbol_Pos.scan_pos --
    1.37    (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    1.38     Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    1.39 -   Symbol_Pos.$$ "\<^descr>" >> K Description) >> (fn (a, b) => {indent = length a, kind = b});
    1.40 +   Symbol_Pos.$$ "\<^descr>" >> K Description)
    1.41 +  >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
    1.42  
    1.43  fun read_marker (Antiquote.Text ss :: _) =
    1.44 -      #1 (Scan.finite Symbol_Pos.stopper (Scan.option (scan_marker -- Symbol_Pos.scan_pos)) ss)
    1.45 +      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
    1.46    | read_marker _ = NONE;
    1.47  
    1.48  in
    1.49 @@ -140,4 +148,22 @@
    1.50  
    1.51  val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
    1.52  
    1.53 +
    1.54 +(* PIDE reports *)
    1.55 +
    1.56 +local
    1.57 +
    1.58 +fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
    1.59 +      Position.is_reported pos ? cons (pos, Markup.markdown_item depth)
    1.60 +  | line_reports _ _ = I;
    1.61 +
    1.62 +fun block_reports depth (Paragraph lines) = fold (line_reports depth) lines
    1.63 +  | block_reports depth (List (_, body)) = fold (block_reports (depth + 1)) body;
    1.64 +
    1.65 +in
    1.66 +
    1.67 +fun reports blocks = fold (block_reports 0) blocks [];
    1.68 +
    1.69  end;
    1.70 +
    1.71 +end;