src/Pure/Thy/markdown.ML
changeset 61451 7f530057bc3c
parent 61450 239a04ec2d4c
child 61452 fa665e3df0ca
     1.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 16:12:38 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:30:54 2015 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    val print_kind: kind -> string
     1.5    type marker = {indent: int, kind: kind}
     1.6    type line
     1.7 +  val line_source: line -> Antiquote.text_antiquote list
     1.8    val line_content: line -> Antiquote.text_antiquote list
     1.9    val make_line: Antiquote.text_antiquote list -> line
    1.10    val empty_line: line
    1.11 @@ -47,14 +48,16 @@
    1.12  
    1.13  datatype line =
    1.14    Line of
    1.15 -   {content: Antiquote.text_antiquote list,
    1.16 +   {source: Antiquote.text_antiquote list,
    1.17 +    content: Antiquote.text_antiquote list,
    1.18      is_empty: bool,
    1.19      marker: (marker * Position.T) option};
    1.20  
    1.21  val eof_line =
    1.22 -  Line {content = [Antiquote.Text [(Symbol.eof, Position.none)]],
    1.23 -    is_empty = false, marker = NONE};
    1.24 +  Line {source = [Antiquote.Text [(Symbol.eof, Position.none)]],
    1.25 +    content = [], is_empty = false, marker = NONE};
    1.26  
    1.27 +fun line_source (Line {source, ...}) = source;
    1.28  fun line_content (Line {content, ...}) = content;
    1.29  fun line_is_empty (Line {is_empty, ...}) = is_empty;
    1.30  fun line_marker (Line {marker, ...}) = marker;
    1.31 @@ -67,8 +70,8 @@
    1.32  fun bad_blank ((s, _): Symbol_Pos.T) = Symbol.is_ascii_blank s andalso s <> Symbol.space;
    1.33  val bad_blanks = maps (fn Antiquote.Text ss => filter bad_blank ss | _ => []);
    1.34  
    1.35 -fun check_blanks content =
    1.36 -  (case bad_blanks content of
    1.37 +fun check_blanks source =
    1.38 +  (case bad_blanks source of
    1.39      [] => ()
    1.40    | (c, pos) :: _ =>
    1.41        error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
    1.42 @@ -83,17 +86,19 @@
    1.43     Symbol_Pos.$$ "\<^descr>" >> K Description)
    1.44    >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
    1.45  
    1.46 -fun read_marker (Antiquote.Text ss :: _) =
    1.47 -      #1 (Scan.finite Symbol_Pos.stopper (Scan.option scan_marker) ss)
    1.48 -  | read_marker _ = NONE;
    1.49 +fun read_marker (Antiquote.Text ss :: rest) =
    1.50 +      (case Scan.finite Symbol_Pos.stopper (Scan.option scan_marker --| Scan.many is_space) ss of
    1.51 +        (marker, []) => (marker, rest)
    1.52 +      | (marker, ss') => (marker, Antiquote.Text ss' :: rest))
    1.53 +  | read_marker source = (NONE, source);
    1.54  
    1.55  in
    1.56  
    1.57 -fun make_line content =
    1.58 +fun make_line source =
    1.59    let
    1.60 -    val _ = check_blanks content;
    1.61 -    val marker = read_marker content;
    1.62 -  in Line {content = content, is_empty = is_empty content, marker = marker} end;
    1.63 +    val _ = check_blanks source;
    1.64 +    val (marker, content) = read_marker source;
    1.65 +  in Line {source = source, content = content, is_empty = is_empty source, marker = marker} end;
    1.66  
    1.67  val empty_line = make_line [];
    1.68  
    1.69 @@ -161,13 +166,12 @@
    1.70        cons (pos, Markup.markdown_item depth)
    1.71    | line_reports _ _ = I;
    1.72  
    1.73 -val lines_pos = #1 o Antiquote.range o maps line_content;
    1.74 -
    1.75  fun block_reports depth (Paragraph lines) =
    1.76 -      cons (lines_pos lines, Markup.markdown_paragraph) #>
    1.77 +      cons (#1 (Antiquote.range (maps line_content lines)), Markup.markdown_paragraph) #>
    1.78        fold (line_reports depth) lines
    1.79    | block_reports depth (List ({kind, ...}, body)) =
    1.80 -      cons (lines_pos (maps block_lines body), Markup.markdown_list (print_kind kind)) #>
    1.81 +      cons (#1 (Antiquote.range (maps line_source (maps block_lines body))),
    1.82 +        Markup.markdown_list (print_kind kind)) #>
    1.83        fold (block_reports (depth + 1)) body;
    1.84  
    1.85  in