src/Pure/Thy/markdown.ML
changeset 61441 20ff1d5c74e1
child 61442 467ebb937294
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/markdown.ML	Wed Oct 14 17:24:21 2015 +0200
     1.3 @@ -0,0 +1,105 @@
     1.4 +(*  Title:      Pure/Thy/markdown.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Minimal support for Markdown documents (see also http://commonmark.org).
     1.8 +*)
     1.9 +
    1.10 +signature MARKDOWN =
    1.11 +sig
    1.12 +  type line
    1.13 +  val read: Input.source -> line list list
    1.14 +end;
    1.15 +
    1.16 +structure Markdown: MARKDOWN =
    1.17 +struct
    1.18 +
    1.19 +(* line with optional item marker *)
    1.20 +
    1.21 +datatype kind = Itemize | Enumerate | Description;
    1.22 +
    1.23 +datatype line =
    1.24 +  Line of
    1.25 +   {content: Antiquote.text_antiquote list,
    1.26 +    is_empty: bool,
    1.27 +    indent: int,
    1.28 +    marker: (kind * Position.T) option};
    1.29 +
    1.30 +fun line_content (Line {content, ...}) = content;
    1.31 +fun line_is_empty (Line {is_empty, ...}) = is_empty;
    1.32 +fun line_indent (Line {indent, ...}) = indent;
    1.33 +fun line_marker (Line {marker, ...}) = marker;
    1.34 +
    1.35 +local
    1.36 +
    1.37 +fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
    1.38 +val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []);
    1.39 +
    1.40 +fun check_blanks content =
    1.41 +  (case bad_blanks content of
    1.42 +    [] => ()
    1.43 +  | (c, pos) :: _ =>
    1.44 +      error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
    1.45 +
    1.46 +fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
    1.47 +val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    1.48 +
    1.49 +fun line_kind (Antiquote.Text ss :: _) =
    1.50 +      let
    1.51 +        val (spaces, rest) = take_prefix is_space ss;
    1.52 +        fun make_marker kind =
    1.53 +          (case rest of
    1.54 +            [(_, pos)] => (kind, pos)
    1.55 +          | (_, pos) :: (" ", _) :: _ => (kind, pos)
    1.56 +          | (_, pos) :: _ => error ("Missing space after item marker" ^ Position.here pos));
    1.57 +        val marker =
    1.58 +          (case rest of
    1.59 +            ("\<^item>", _) :: _ => SOME (make_marker Itemize)
    1.60 +          | ("\<^enum>", _) :: _ => SOME (make_marker Enumerate)
    1.61 +          | ("\<^descr>", _) :: _ => SOME (make_marker Description)
    1.62 +          | _ => NONE);
    1.63 +      in (length spaces, marker) end
    1.64 +  | line_kind _ = (0, NONE);
    1.65 +
    1.66 +in
    1.67 +
    1.68 +fun make_line content =
    1.69 +  let
    1.70 +    val _ = check_blanks content;
    1.71 +    val (indent, marker) = line_kind content;
    1.72 +  in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
    1.73 +
    1.74 +end;
    1.75 +
    1.76 +
    1.77 +(* spans of related lines *)
    1.78 +
    1.79 +local
    1.80 +
    1.81 +val eof = make_line [Antiquote.Text [(Symbol.eof, Position.none)]];
    1.82 +val stopper = Scan.stopper (K eof) (fn line => line = eof);
    1.83 +
    1.84 +fun item_line line = is_some (line_marker line);
    1.85 +fun plain_line line = is_none (line_marker line) andalso line <> eof;
    1.86 +
    1.87 +val parse_span =
    1.88 +  Scan.one item_line -- Scan.many plain_line >> op :: ||
    1.89 +  Scan.many1 plain_line ||
    1.90 +  Scan.many1 line_is_empty;
    1.91 +
    1.92 +in
    1.93 +
    1.94 +fun read_spans lines =
    1.95 +  the_default [] (Scan.read stopper (Scan.repeat parse_span) lines);
    1.96 +
    1.97 +end;
    1.98 +
    1.99 +
   1.100 +(* document structure *)
   1.101 +
   1.102 +fun read input =
   1.103 +  Antiquote.read input
   1.104 +  |> Antiquote.split_lines
   1.105 +  |> map make_line
   1.106 +  |> read_spans;
   1.107 +
   1.108 +end;