src/Pure/Thy/markdown.ML
author wenzelm
Thu Oct 15 12:43:02 2015 +0200 (2015-10-15)
changeset 61445 31aadb15eda5
parent 61444 1fcdfc1a7e50
child 61446 9b09acfb7e06
permissions -rw-r--r--
more document structure;
tuned signature;
     1 (*  Title:      Pure/Thy/markdown.ML
     2     Author:     Makarius
     3 
     4 Minimal support for Markdown documents (see also http://commonmark.org).
     5 *)
     6 
     7 signature MARKDOWN =
     8 sig
     9   datatype kind = Itemize | Enumerate | Description
    10   type marker = {indent: int, kind: kind}
    11   type line
    12   val line_content: line -> Antiquote.text_antiquote list
    13   val make_line: Antiquote.text_antiquote list -> line
    14   val empty_line: line
    15   datatype block = Paragraph of line list | List of marker * block list
    16   val read_lines: line list -> block list
    17   val read: Input.source -> block list
    18 end;
    19 
    20 structure Markdown: MARKDOWN =
    21 struct
    22 
    23 (* document lines *)
    24 
    25 datatype kind = Itemize | Enumerate | Description;
    26 type marker = {indent: int, kind: kind};
    27 
    28 datatype line =
    29   Line of
    30    {content: Antiquote.text_antiquote list,
    31     is_empty: bool,
    32     marker: (marker * Position.T) option};
    33 
    34 val eof_line =
    35   Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
    36     is_empty = false, marker = NONE};
    37 
    38 fun line_content (Line {content, ...}) = content;
    39 fun line_is_empty (Line {is_empty, ...}) = is_empty;
    40 fun line_marker (Line {marker, ...}) = marker;
    41 
    42 
    43 (* make line *)
    44 
    45 local
    46 
    47 fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
    48 val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []);
    49 
    50 fun check_blanks content =
    51   (case bad_blanks content of
    52     [] => ()
    53   | (c, pos) :: _ =>
    54       error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
    55 
    56 fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
    57 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    58 
    59 val scan_marker =
    60   Scan.many is_space --
    61   (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    62    Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    63    Symbol_Pos.$$ "\<^descr>" >> K Description) >> (fn (a, b) => {indent = length a, kind = b});
    64 
    65 fun read_marker (Antiquote.Text ss :: _) =
    66       #1 (Scan.finite Symbol_Pos.stopper (Scan.option (scan_marker -- Symbol_Pos.scan_pos)) ss)
    67   | read_marker _ = NONE;
    68 
    69 in
    70 
    71 fun make_line content =
    72   let
    73     val _ = check_blanks content;
    74     val marker = read_marker content;
    75   in Line {content = content, is_empty = is_empty content, marker = marker} end;
    76 
    77 val empty_line = make_line [];
    78 
    79 end;
    80 
    81 
    82 (* document blocks *)
    83 
    84 datatype block = Paragraph of line list | List of marker * block list;
    85 
    86 fun add_span (opt_marker, body) document =
    87   (case (opt_marker, document) of
    88     (SOME marker, List (list_marker, list_body) :: rest) =>
    89       if marker = list_marker then List (list_marker, body @ list_body) :: rest
    90       else List (marker, body) :: document
    91   | (SOME marker, _) => List (marker, body) :: document
    92   | (NONE, _) => body @ document);
    93 
    94 
    95 (* read document *)
    96 
    97 local
    98 
    99 fun plain_line line =
   100   not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
   101 
   102 val parse_paragraph = Scan.many1 plain_line >> Paragraph;
   103 
   104 val parse_span =
   105   parse_paragraph >> (fn par => (NONE, [par])) ||
   106   Scan.one (is_some o line_marker) -- Scan.many plain_line --
   107     Scan.repeat (Scan.one line_is_empty |-- parse_paragraph) >>
   108       (fn ((line, lines), pars) =>
   109         (Option.map #1 (line_marker line), Paragraph (line :: lines) :: pars));
   110 
   111 val parse_document =
   112   parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span)
   113     >> (fn spans => fold_rev add_span spans []);
   114 
   115 in
   116 
   117 val read_lines =
   118   Scan.read (Scan.stopper (K eof_line) (fn line => line = eof_line))
   119     (Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #>
   120   the_default [] #> flat;
   121 
   122 end;
   123 
   124 val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
   125 
   126 end;