src/Pure/Thy/markdown.ML
changeset 61457 3e21699bb83b
parent 61454 c86286ae9fe5
child 61459 5f2ddeb15c06
     1.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 22:25:57 2015 +0200
     1.2 +++ b/src/Pure/Thy/markdown.ML	Fri Oct 16 10:11:20 2015 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  
     1.5  signature MARKDOWN =
     1.6  sig
     1.7 +  val is_control: Symbol.symbol -> bool
     1.8    datatype kind = Itemize | Enumerate | Description
     1.9    val print_kind: kind -> string
    1.10    type marker = {indent: int, kind: kind}
    1.11 @@ -29,7 +30,9 @@
    1.12    val empty_line: line
    1.13    datatype block = Paragraph of line list | List of marker * block list
    1.14    val read_lines: line list -> block list
    1.15 -  val read: Input.source -> block list
    1.16 +  val read_antiquotes: Antiquote.text_antiquote list -> block list
    1.17 +  val read_source: Input.source -> block list
    1.18 +  val text_reports: Antiquote.text_antiquote list -> Position.report list
    1.19    val reports: block list -> Position.report list
    1.20  end;
    1.21  
    1.22 @@ -38,6 +41,8 @@
    1.23  
    1.24  (* document lines *)
    1.25  
    1.26 +val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
    1.27 +
    1.28  datatype kind = Itemize | Enumerate | Description;
    1.29  
    1.30  fun print_kind Itemize = "itemize"
    1.31 @@ -155,17 +160,22 @@
    1.32      (Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #>
    1.33    the_default [] #> flat;
    1.34  
    1.35 -end;
    1.36 +val read_antiquotes = Antiquote.split_lines #> map make_line #> read_lines;
    1.37 +val read_source = Antiquote.read #> read_antiquotes;
    1.38  
    1.39 -val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
    1.40 +end;
    1.41  
    1.42  
    1.43  (* PIDE reports *)
    1.44  
    1.45 +val text_reports =
    1.46 +  maps (fn Antiquote.Text ss => [(#1 (Symbol_Pos.range ss), Markup.words)] | _ => []);
    1.47 +
    1.48  local
    1.49  
    1.50 -fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
    1.51 -      cons (pos, Markup.markdown_item depth)
    1.52 +fun line_reports depth (Line {marker = SOME (_, pos), content, ...}) =
    1.53 +      cons (pos, Markup.markdown_item depth) #>
    1.54 +      append (text_reports content)
    1.55    | line_reports _ _ = I;
    1.56  
    1.57  fun block_reports depth block =