minimal support for Markdown documents;
authorwenzelm
Wed Oct 14 17:24:21 2015 +0200 (2015-10-14)
changeset 6144120ff1d5c74e1
parent 61440 8626c2fed037
child 61442 467ebb937294
minimal support for Markdown documents;
src/Pure/ROOT
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/ROOT	Wed Oct 14 17:24:03 2015 +0200
     1.2 +++ b/src/Pure/ROOT	Wed Oct 14 17:24:21 2015 +0200
     1.3 @@ -229,6 +229,7 @@
     1.4      "System/system_channel.ML"
     1.5      "Thy/html.ML"
     1.6      "Thy/latex.ML"
     1.7 +    "Thy/markdown.ML"
     1.8      "Thy/present.ML"
     1.9      "Thy/term_style.ML"
    1.10      "Thy/thy_header.ML"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Thy/markdown.ML	Wed Oct 14 17:24:21 2015 +0200
     2.3 @@ -0,0 +1,105 @@
     2.4 +(*  Title:      Pure/Thy/markdown.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Minimal support for Markdown documents (see also http://commonmark.org).
     2.8 +*)
     2.9 +
    2.10 +signature MARKDOWN =
    2.11 +sig
    2.12 +  type line
    2.13 +  val read: Input.source -> line list list
    2.14 +end;
    2.15 +
    2.16 +structure Markdown: MARKDOWN =
    2.17 +struct
    2.18 +
    2.19 +(* line with optional item marker *)
    2.20 +
    2.21 +datatype kind = Itemize | Enumerate | Description;
    2.22 +
    2.23 +datatype line =
    2.24 +  Line of
    2.25 +   {content: Antiquote.text_antiquote list,
    2.26 +    is_empty: bool,
    2.27 +    indent: int,
    2.28 +    marker: (kind * Position.T) option};
    2.29 +
    2.30 +fun line_content (Line {content, ...}) = content;
    2.31 +fun line_is_empty (Line {is_empty, ...}) = is_empty;
    2.32 +fun line_indent (Line {indent, ...}) = indent;
    2.33 +fun line_marker (Line {marker, ...}) = marker;
    2.34 +
    2.35 +local
    2.36 +
    2.37 +fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
    2.38 +val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []);
    2.39 +
    2.40 +fun check_blanks content =
    2.41 +  (case bad_blanks content of
    2.42 +    [] => ()
    2.43 +  | (c, pos) :: _ =>
    2.44 +      error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
    2.45 +
    2.46 +fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
    2.47 +val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
    2.48 +
    2.49 +fun line_kind (Antiquote.Text ss :: _) =
    2.50 +      let
    2.51 +        val (spaces, rest) = take_prefix is_space ss;
    2.52 +        fun make_marker kind =
    2.53 +          (case rest of
    2.54 +            [(_, pos)] => (kind, pos)
    2.55 +          | (_, pos) :: (" ", _) :: _ => (kind, pos)
    2.56 +          | (_, pos) :: _ => error ("Missing space after item marker" ^ Position.here pos));
    2.57 +        val marker =
    2.58 +          (case rest of
    2.59 +            ("\<^item>", _) :: _ => SOME (make_marker Itemize)
    2.60 +          | ("\<^enum>", _) :: _ => SOME (make_marker Enumerate)
    2.61 +          | ("\<^descr>", _) :: _ => SOME (make_marker Description)
    2.62 +          | _ => NONE);
    2.63 +      in (length spaces, marker) end
    2.64 +  | line_kind _ = (0, NONE);
    2.65 +
    2.66 +in
    2.67 +
    2.68 +fun make_line content =
    2.69 +  let
    2.70 +    val _ = check_blanks content;
    2.71 +    val (indent, marker) = line_kind content;
    2.72 +  in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
    2.73 +
    2.74 +end;
    2.75 +
    2.76 +
    2.77 +(* spans of related lines *)
    2.78 +
    2.79 +local
    2.80 +
    2.81 +val eof = make_line [Antiquote.Text [(Symbol.eof, Position.none)]];
    2.82 +val stopper = Scan.stopper (K eof) (fn line => line = eof);
    2.83 +
    2.84 +fun item_line line = is_some (line_marker line);
    2.85 +fun plain_line line = is_none (line_marker line) andalso line <> eof;
    2.86 +
    2.87 +val parse_span =
    2.88 +  Scan.one item_line -- Scan.many plain_line >> op :: ||
    2.89 +  Scan.many1 plain_line ||
    2.90 +  Scan.many1 line_is_empty;
    2.91 +
    2.92 +in
    2.93 +
    2.94 +fun read_spans lines =
    2.95 +  the_default [] (Scan.read stopper (Scan.repeat parse_span) lines);
    2.96 +
    2.97 +end;
    2.98 +
    2.99 +
   2.100 +(* document structure *)
   2.101 +
   2.102 +fun read input =
   2.103 +  Antiquote.read input
   2.104 +  |> Antiquote.split_lines
   2.105 +  |> map make_line
   2.106 +  |> read_spans;
   2.107 +
   2.108 +end;