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