src/Pure/Thy/markdown.ML

--- a/src/Pure/Thy/markdown.ML	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Fri Oct 16 10:11:20 2015 +0200
@@ -19,6 +19,7 @@
 
 signature MARKDOWN =
 sig
+  val is_control: Symbol.symbol -> bool
   datatype kind = Itemize | Enumerate | Description
   val print_kind: kind -> string
   type marker = {indent: int, kind: kind}
@@ -29,7 +30,9 @@
   val empty_line: line
   datatype block = Paragraph of line list | List of marker * block list
   val read_lines: line list -> block list
-  val read: Input.source -> block list
+  val read_antiquotes: Antiquote.text_antiquote list -> block list
+  val read_source: Input.source -> block list
+  val text_reports: Antiquote.text_antiquote list -> Position.report list
   val reports: block list -> Position.report list
 end;
 
@@ -38,6 +41,8 @@
 
 (* document lines *)
 
+val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
+
 datatype kind = Itemize | Enumerate | Description;
 
 fun print_kind Itemize = "itemize"
@@ -155,17 +160,22 @@
     (Scan.repeat (Scan.many line_is_empty |-- parse_document) --| Scan.many line_is_empty) #>
   the_default [] #> flat;
 
-end;
+val read_antiquotes = Antiquote.split_lines #> map make_line #> read_lines;
+val read_source = Antiquote.read #> read_antiquotes;
 
-val read = Antiquote.read #> Antiquote.split_lines #> map make_line #> read_lines;
+end;
 
 
 (* PIDE reports *)
 
+val text_reports =
+  maps (fn Antiquote.Text ss => [(#1 (Symbol_Pos.range ss), Markup.words)] | _ => []);
+
 local
 
-fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
-      cons (pos, Markup.markdown_item depth)
+fun line_reports depth (Line {marker = SOME (_, pos), content, ...}) =
+      cons (pos, Markup.markdown_item depth) #>
+      append (text_reports content)
   | line_reports _ _ = I;
 
 fun block_reports depth block =