src/Pure/Thy/markdown.ML
changeset 61442 467ebb937294
parent 61441 20ff1d5c74e1
child 61443 78bbfadd1034
     1.1 --- a/src/Pure/Thy/markdown.ML	Wed Oct 14 17:24:21 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Wed Oct 14 18:29:41 2015 +0200
     1.3 @@ -43,29 +43,23 @@
     1.4  fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
     1.5  val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
     1.6  
     1.7 -fun line_kind (Antiquote.Text ss :: _) =
     1.8 -      let
     1.9 -        val (spaces, rest) = take_prefix is_space ss;
    1.10 -        fun make_marker kind =
    1.11 -          (case rest of
    1.12 -            [(_, pos)] => (kind, pos)
    1.13 -          | (_, pos) :: (" ", _) :: _ => (kind, pos)
    1.14 -          | (_, pos) :: _ => error ("Missing space after item marker" ^ Position.here pos));
    1.15 -        val marker =
    1.16 -          (case rest of
    1.17 -            ("\<^item>", _) :: _ => SOME (make_marker Itemize)
    1.18 -          | ("\<^enum>", _) :: _ => SOME (make_marker Enumerate)
    1.19 -          | ("\<^descr>", _) :: _ => SOME (make_marker Description)
    1.20 -          | _ => NONE);
    1.21 -      in (length spaces, marker) end
    1.22 -  | line_kind _ = (0, NONE);
    1.23 +val scan_prefix =
    1.24 +  (Scan.many is_space >> length) --
    1.25 +  Scan.option
    1.26 +    ((Symbol_Pos.$$ "\<^item>" >> K Itemize ||
    1.27 +      Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
    1.28 +      Symbol_Pos.$$ "\<^descr>" >> K Description) -- Symbol_Pos.scan_pos);
    1.29 +
    1.30 +fun scan_line (Antiquote.Text ss :: _) =
    1.31 +      the_default (0, NONE) (Scan.read Symbol_Pos.stopper scan_prefix ss)
    1.32 +  | scan_line _ = (0, NONE);
    1.33  
    1.34  in
    1.35  
    1.36  fun make_line content =
    1.37    let
    1.38      val _ = check_blanks content;
    1.39 -    val (indent, marker) = line_kind content;
    1.40 +    val (indent, marker) = scan_line content;
    1.41    in Line {content = content, is_empty = is_empty content, indent = indent, marker = marker} end;
    1.42  
    1.43  end;
    1.44 @@ -75,15 +69,17 @@
    1.45  
    1.46  local
    1.47  
    1.48 -val eof = make_line [Antiquote.Text [(Symbol.eof, Position.none)]];
    1.49 +val eof =
    1.50 +  Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
    1.51 +    is_empty = false, indent = 0, marker = NONE};
    1.52  val stopper = Scan.stopper (K eof) (fn line => line = eof);
    1.53  
    1.54 -fun item_line line = is_some (line_marker line);
    1.55 -fun plain_line line = is_none (line_marker line) andalso line <> eof;
    1.56 +fun plain_line line =
    1.57 +  not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof;
    1.58  
    1.59  val parse_span =
    1.60 -  Scan.one item_line -- Scan.many plain_line >> op :: ||
    1.61    Scan.many1 plain_line ||
    1.62 +  Scan.one (is_some o line_marker) -- Scan.many plain_line >> op :: ||
    1.63    Scan.many1 line_is_empty;
    1.64  
    1.65  in