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