src/Pure/Thy/markdown.ML
author wenzelm
Wed Oct 14 17:24:21 2015 +0200 (2015-10-14)
changeset 61441 20ff1d5c74e1
child 61442 467ebb937294
permissions -rw-r--r--
minimal support for Markdown documents;
     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 fun line_kind (Antiquote.Text ss :: _) =
    47       let
    48         val (spaces, rest) = take_prefix is_space ss;
    49         fun make_marker kind =
    50           (case rest of
    51             [(_, pos)] => (kind, pos)
    52           | (_, pos) :: (" ", _) :: _ => (kind, pos)
    53           | (_, pos) :: _ => error ("Missing space after item marker" ^ Position.here pos));
    54         val marker =
    55           (case rest of
    56             ("\<^item>", _) :: _ => SOME (make_marker Itemize)
    57           | ("\<^enum>", _) :: _ => SOME (make_marker Enumerate)
    58           | ("\<^descr>", _) :: _ => SOME (make_marker Description)
    59           | _ => NONE);
    60       in (length spaces, marker) end
    61   | line_kind _ = (0, NONE);
    62 
    63 in
    64 
    65 fun make_line content =
    66   let
    67     val _ = check_blanks content;
    68     val (indent, marker) = line_kind content;
    69   in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
    70 
    71 end;
    72 
    73 
    74 (* spans of related lines *)
    75 
    76 local
    77 
    78 val eof = make_line [Antiquote.Text [(Symbol.eof, Position.none)]];
    79 val stopper = Scan.stopper (K eof) (fn line => line = eof);
    80 
    81 fun item_line line = is_some (line_marker line);
    82 fun plain_line line = is_none (line_marker line) andalso line <> eof;
    83 
    84 val parse_span =
    85   Scan.one item_line -- Scan.many plain_line >> op :: ||
    86   Scan.many1 plain_line ||
    87   Scan.many1 line_is_empty;
    88 
    89 in
    90 
    91 fun read_spans lines =
    92   the_default [] (Scan.read stopper (Scan.repeat parse_span) lines);
    93 
    94 end;
    95 
    96 
    97 (* document structure *)
    98 
    99 fun read input =
   100   Antiquote.read input
   101   |> Antiquote.split_lines
   102   |> map make_line
   103   |> read_spans;
   104 
   105 end;