src/Pure/Thy/markdown.ML
author wenzelm
Wed Oct 14 18:29:41 2015 +0200 (2015-10-14)
changeset 61442 467ebb937294
parent 61441 20ff1d5c74e1
child 61443 78bbfadd1034
permissions -rw-r--r--
clarified;
     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   type line
    10   val read: Input.source -> line list list
    11 end;
    12 
    13 structure Markdown: MARKDOWN =
    14 struct
    15 
    16 (* line with optional item marker *)
    17 
    18 datatype kind = Itemize | Enumerate | Description;
    19 
    20 datatype line =
    21   Line of
    22    {content: Antiquote.text_antiquote list,
    23     is_empty: bool,
    24     indent: int,
    25     marker: (kind * Position.T) option};
    26 
    27 fun line_content (Line {content, ...}) = content;
    28 fun line_is_empty (Line {is_empty, ...}) = is_empty;
    29 fun line_indent (Line {indent, ...}) = indent;
    30 fun line_marker (Line {marker, ...}) = marker;
    31 
    32 local
    33 
    34 fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
    35 val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []);
    36 
    37 fun check_blanks content =
    38   (case bad_blanks content of
    39     [] => ()
    40   | (c, pos) :: _ =>
    41       error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
    42 
    43 fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
    44 val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    45 
    46 val scan_prefix =
    47   (Scan.many is_space >> length) --
    48   Scan.option
    49     ((Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    50       Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    51       Symbol_Pos.$$ "\<^descr>" >> K Description) -- Symbol_Pos.scan_pos);
    52 
    53 fun scan_line (Antiquote.Text ss :: _) =
    54       the_default (0, NONE) (Scan.read Symbol_Pos.stopper scan_prefix ss)
    55   | scan_line _ = (0, NONE);
    56 
    57 in
    58 
    59 fun make_line content =
    60   let
    61     val _ = check_blanks content;
    62     val (indent, marker) = scan_line content;
    63   in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
    64 
    65 end;
    66 
    67 
    68 (* spans of related lines *)
    69 
    70 local
    71 
    72 val eof =
    73   Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
    74     is_empty = false, indent = 0, marker = NONE};
    75 val stopper = Scan.stopper (K eof) (fn line => line = eof);
    76 
    77 fun plain_line line =
    78   not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof;
    79 
    80 val parse_span =
    81   Scan.many1 plain_line ||
    82   Scan.one (is_some o line_marker) -- Scan.many plain_line >> op :: ||
    83   Scan.many1 line_is_empty;
    84 
    85 in
    86 
    87 fun read_spans lines =
    88   the_default [] (Scan.read stopper (Scan.repeat parse_span) lines);
    89 
    90 end;
    91 
    92 
    93 (* document structure *)
    94 
    95 fun read input =
    96   Antiquote.read input
    97   |> Antiquote.split_lines
    98   |> map make_line
    99   |> read_spans;
   100 
   101 end;