clarified Antiquote.antiq_reports;
Thy_Output.output_text: support for markdown (inactive);
eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;

--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Fri Oct 16 10:11:20 2015 +0200
@@ -179,7 +179,8 @@
 ML \<open>
   Outer_Syntax.command
     @{command_keyword text_cartouche} ""
-    (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
+    (Parse.opt_target -- Parse.input Parse.cartouche
+      >> Thy_Output.document_command {markdown = true})
 \<close>
 
 text_cartouche

--- a/src/Pure/General/antiquote.ML	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Fri Oct 16 10:11:20 2015 +0200
@@ -11,9 +11,7 @@
   type text_antiquote = Symbol_Pos.T list antiquote
   val range: text_antiquote list -> Position.range
   val split_lines: text_antiquote list -> text_antiquote list list
-  val antiq_reports: antiq -> Position.report list
-  val antiquote_reports: ('a -> Position.report_text list) ->
-    'a antiquote list -> Position.report_text list
+  val antiq_reports: 'a antiquote list -> Position.report list
   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
   val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
   val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
@@ -56,12 +54,13 @@
 
 (* reports *)
 
-fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
-  [(start, Markup.antiquote), (stop, Markup.antiquote),
-   (pos, Markup.antiquoted), (pos, Markup.language_antiquotation)];
-
-fun antiquote_reports text =
-  maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
+fun antiq_reports ants = ants |> maps
+  (fn Antiq (_, {start, stop, range = (pos, _)}) =>
+      [(start, Markup.antiquote),
+       (stop, Markup.antiquote),
+       (pos, Markup.antiquoted),
+       (pos, Markup.language_antiquotation)]
+    | _ => []);
 
 
 (* scan *)
@@ -102,7 +101,7 @@
 
 fun read' pos syms =
   (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
-    SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
+    SOME ants => (Position.reports (antiq_reports ants); ants)
   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
 
 fun read source = read' (Input.pos_of source) (Input.source_explode source);

--- a/src/Pure/ML/ml_lex.ML	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Oct 16 10:11:20 2015 +0200
@@ -157,7 +157,7 @@
 
 in
 
-fun report_of_token SML (tok as Token ((pos, _), (kind, x))) =
+fun token_report SML (tok as Token ((pos, _), (kind, x))) =
   let
     val (markup, txt) =
       if not (is_keyword tok) then token_kind_markup SML kind
@@ -328,7 +328,8 @@
         (Scan.recover (Scan.bulk (!!! "bad input" scan))
           (fn msg => recover msg >> map Antiquote.Text))
       |> Source.exhaust
-      |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token SML))
+      |> tap (Position.reports o Antiquote.antiq_reports)
+      |> tap (Position.reports_text o maps (fn Antiquote.Text t => [token_report SML t] | _ => []))
       |> tap (List.app check);
   in input @ termination end;
 

--- a/src/Pure/PIDE/command.ML	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Oct 16 10:11:20 2015 +0200
@@ -193,7 +193,7 @@
   Toplevel.setmp_thread_position tr
     (fn () =>
       Outer_Syntax.side_comments span |> maps (fn cmt =>
-        (Thy_Output.check_text (Token.input_of cmt) st'; [])
+        (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
           handle exn =>
             if Exn.is_interrupt exn then reraise exn
             else Runtime.exn_messages_ids exn)) ();

--- 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 =

--- a/src/Pure/Thy/thy_output.ML	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Oct 16 10:11:20 2015 +0200
@@ -24,8 +24,7 @@
   val boolean: string -> bool
   val integer: string -> int
   val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
-  val report_text: Input.source -> unit
-  val check_text: Input.source -> Toplevel.state -> unit
+  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
@@ -37,7 +36,7 @@
   val output: Proof.context -> Pretty.T list -> string
   val verbatim_text: Proof.context -> string -> string
   val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition
-  val document_command: (xstring * Position.T) option * Input.source ->
+  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
     Toplevel.transition -> Toplevel.transition
 end;
 
@@ -160,17 +159,7 @@
 end;
 
 
-(* eval antiquotes *)
-
-fun read_antiquotes state source =
-  let
-    val ants =
-      Antiquote.read' (Input.pos_of source) (Symbol_Pos.trim_blanks (Input.source_explode source));
-
-    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
-      | words (Antiquote.Antiq _) = [];
-    val _ = Position.reports (maps words ants);
-  in ants end;
+(* eval antiquote *)
 
 fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
   | eval_antiquote state (Antiquote.Antiq (ss, {range = (pos, _), ...})) =
@@ -192,18 +181,42 @@
       in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
 
 
-(* check_text *)
+(* output text *)
 
-fun report_text source =
-  Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
+fun output_text state {markdown} source =
+  let
+    val pos = Input.pos_of source;
+    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
+    val syms = Input.source_explode source;
+
+    val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
+    val output_antiquotes = map output_antiquote #> implode;
 
-fun check_text source state =
- (report_text source;
-  if Toplevel.is_skipped_proof state then ()
-  else
-    source
-    |> read_antiquotes state
-    |> List.app (ignore o eval_antiquote state));
+    fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
+    and output_block (Markdown.Paragraph lines) =
+          cat_lines (map (output_antiquotes o Markdown.line_source) lines)
+      | output_block (Markdown.List (marker, body)) =
+          let val env = Markdown.print_kind (#kind marker) in
+            "%\n\\begin{" ^ env ^ "}%\n" ^
+            output_blocks body ^
+            "%\n\\end{" ^ env ^ "}%\n"
+          end;
+  in
+    if Toplevel.is_skipped_proof state then ""
+    else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
+      andalso false (* FIXME *)
+    then
+      let
+        val ants = Antiquote.read' pos syms;
+        val blocks = Markdown.read_antiquotes ants;
+        val _ = Position.reports (Markdown.reports blocks);
+      in output_blocks blocks end
+    else
+      let
+        val ants = Antiquote.read' pos (Symbol_Pos.trim_blanks syms);
+        val _ = Position.reports (Markdown.text_reports ants);
+      in output_antiquotes ants end
+  end;
 
 
 
@@ -232,21 +245,18 @@
 
 (* output token *)
 
-fun output_token state =
-  let
-    val make_text = read_antiquotes state #> map (eval_antiquote state) #> implode;
-    val output_text = make_text #> Symbol.explode #> Latex.output_ctrl_symbols;
-    fun output No_Token = ""
-      | output (Basic_Token tok) = Latex.output_token tok
-      | output (Markup_Token (cmd, source)) =
-          "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text source ^ "%\n}\n"
-      | output (Markup_Env_Token (cmd, source)) =
-          "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
-          output_text source ^
-          "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
-      | output (Raw_Token source) =
-          "%\n" ^ output_text source ^ "\n";
-  in output end;
+fun output_token state tok =
+  (case tok of
+    No_Token => ""
+  | Basic_Token tok => Latex.output_token tok
+  | Markup_Token (cmd, source) =>
+      "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
+  | Markup_Env_Token (cmd, source) =>
+      "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
+      output_text state {markdown = true} source ^
+      "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
+  | Raw_Token source =>
+      "%\n" ^ output_text state {markdown = true} source ^ "\n");
 
 
 (* command spans *)
@@ -729,15 +739,15 @@
   Toplevel.keep (fn state =>
     if Toplevel.is_toplevel state then
      (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
-      check_text txt state)
+      ignore (output_text state {markdown = false} txt))
     else raise Toplevel.UNDEF);
 
-fun document_command (loc, txt) =
+fun document_command markdown (loc, txt) =
   Toplevel.keep (fn state =>
     (case loc of
-      NONE => check_text txt state
+      NONE => ignore (output_text state markdown txt)
     | SOME (_, pos) =>
         error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
-  Toplevel.present_local_theory loc (check_text txt);
+  Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
 
 end;

--- a/src/Pure/Tools/rail.ML	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/Pure/Tools/rail.ML	Fri Oct 16 10:11:20 2015 +0200
@@ -63,7 +63,7 @@
 fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
   | reports_of_token (Token ((pos, _), (Keyword, x))) =
       map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
-  | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
+  | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq]
   | reports_of_token _ = [];
 
 

--- a/src/Pure/pure_syn.ML	Thu Oct 15 22:25:57 2015 +0200
+++ b/src/Pure/pure_syn.ML	Fri Oct 16 10:11:20 2015 +0200
@@ -19,31 +19,31 @@
 
 val _ =
   Outer_Syntax.command ("chapter", @{here}) "chapter heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("section", @{here}) "section heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subsection", @{here}) "subsection heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
 
 val _ =
   Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
-    (Parse.document_source >> (fn s => Toplevel.keep (fn _ => Thy_Output.report_text s)));
+    (Parse.document_source >> (fn s => Thy_Output.document_command {markdown = true} (NONE, s)));
 
 val _ =
   Outer_Syntax.command ("theory", @{here}) "begin theory"