more uniform treatment of formal comments within document source;
more robust nesting;

--- a/lib/texinputs/isabelle.sty	Sat Feb 03 15:34:22 2018 +0100
+++ b/lib/texinputs/isabelle.sty	Sat Feb 03 20:34:26 2018 +0100
@@ -239,7 +239,7 @@
 % cancel text
 
 \usepackage[normalem]{ulem}
-\newcommand{\isamarkupcancel}[1]{\xout{#1}}
+\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
 
 
 % tagged regions

--- a/src/Pure/General/antiquote.ML	Sat Feb 03 15:34:22 2018 +0100
+++ b/src/Pure/General/antiquote.ML	Sat Feb 03 20:34:26 2018 +0100
@@ -17,8 +17,9 @@
   val scan_control: control scanner
   val scan_antiq: antiq scanner
   val scan_antiquote: text_antiquote scanner
-  val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
-  val read: Input.source -> text_antiquote list
+  val scan_antiquote_comments: text_antiquote scanner
+  val parse_comments: Position.T -> Symbol_Pos.T list -> text_antiquote list
+  val read_comments: Input.source -> text_antiquote list
 end;
 
 structure Antiquote: ANTIQUOTE =
@@ -79,14 +80,24 @@
 val err_prefix = "Antiquotation lexical error: ";
 
 val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
+val scan_nl_opt = Scan.optional scan_nl [];
 
-val scan_txt =
-  scan_nl ||
-  Scan.repeats1
-   (Scan.many1 (fn (s, _) =>
-      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso
-        s <> "\n" andalso Symbol.not_eof s) ||
-    $$$ "@" --| Scan.ahead (~$$ "{")) @@@ Scan.optional scan_nl [];
+val scan_plain_txt =
+  Scan.many1 (fn (s, _) =>
+    not (Comment.is_symbol s) andalso
+    not (Symbol.is_control s) andalso
+    s <> Symbol.open_ andalso
+    s <> "@" andalso
+    s <> "\n" andalso
+    Symbol.not_eof s) ||
+  Scan.one (Comment.is_symbol o Symbol_Pos.symbol) >> single ||
+  $$$ "@" --| Scan.ahead (~$$ "{");
+
+val scan_text =
+  scan_nl || Scan.repeats1 scan_plain_txt @@@ scan_nl_opt;
+
+val scan_text_comments =
+  scan_nl || Scan.repeats1 (Comment.scan >> #2 || scan_plain_txt) @@@ scan_nl_opt;
 
 val scan_antiq_body =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
@@ -122,21 +133,24 @@
        body = body});
 
 val scan_antiquote =
-  scan_txt >> Text || scan_control >> Control || scan_antiq >> Antiq;
+  scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq;
+
+val scan_antiquote_comments =
+  scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq;
 
 end;
 
 
-(* read *)
+(* parse and read (with formal comments) *)
 
-fun parse pos syms =
-  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
+fun parse_comments pos syms =
+  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote_comments) syms of
     SOME ants => ants
   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
 
-fun read source =
+fun read_comments source =
   let
-    val ants = parse (Input.pos_of source) (Input.source_explode source);
+    val ants = parse_comments (Input.pos_of source) (Input.source_explode source);
     val _ = Position.reports (antiq_reports ants);
   in ants end;
 

--- a/src/Pure/General/comment.ML	Sat Feb 03 15:34:22 2018 +0100
+++ b/src/Pure/General/comment.ML	Sat Feb 03 20:34:26 2018 +0100
@@ -8,6 +8,7 @@
 sig
   datatype kind = Comment | Cancel | Latex
   val markups: kind -> Markup.T list
+  val is_symbol: Symbol.symbol -> bool
   val scan_comment: (kind * Symbol_Pos.T list) scanner
   val scan_cancel: (kind * Symbol_Pos.T list) scanner
   val scan_latex: (kind * Symbol_Pos.T list) scanner

--- a/src/Pure/Thy/document_antiquotation.ML	Sat Feb 03 15:34:22 2018 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML	Sat Feb 03 20:34:26 2018 +0100
@@ -29,7 +29,8 @@
   val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   val boolean: string -> bool
   val integer: string -> int
-  val evaluate: Proof.context -> Antiquote.text_antiquote -> Latex.text list
+  val evaluate: (Symbol_Pos.T list -> Latex.text list) -> Proof.context ->
+    Antiquote.text_antiquote -> Latex.text list
 end;
 
 structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
@@ -167,9 +168,9 @@
 
 in
 
-fun evaluate ctxt antiq =
+fun evaluate eval_text ctxt antiq =
   (case antiq of
-    Antiquote.Text ss => [Latex.symbols ss]
+    Antiquote.Text ss => eval_text ss
   | Antiquote.Control {name, body, ...} =>
       eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   | Antiquote.Antiq {range = (pos, _), body, ...} =>

--- a/src/Pure/Thy/markdown.ML	Sat Feb 03 15:34:22 2018 +0100
+++ b/src/Pure/Thy/markdown.ML	Sat Feb 03 20:34:26 2018 +0100
@@ -191,7 +191,7 @@
   the_default [] #> flat;
 
 val read_antiquotes = Antiquote.split_lines #> map make_line #> read_lines;
-val read_source = Antiquote.read #> read_antiquotes;
+val read_source = Antiquote.read_comments #> read_antiquotes;
 
 end;
 

--- a/src/Pure/Thy/thy_output.ML	Sat Feb 03 15:34:22 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Feb 03 20:34:26 2018 +0100
@@ -40,12 +40,36 @@
 
 (* output document source *)
 
-fun output_document ctxt {markdown} source =
+val output_symbols = single o Latex.symbols_output;
+
+fun output_comment ctxt (kind, syms) =
+  (case kind of
+    Comment.Comment =>
+      Input.cartouche_content syms
+      |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false)
+          {markdown = false}
+      |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
+  | Comment.Cancel =>
+      Symbol_Pos.cartouche_content syms
+      |> output_symbols
+      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
+  | Comment.Latex =>
+      [Latex.symbols (Symbol_Pos.cartouche_content syms)])
+and output_comment_document ctxt (comment, syms) =
+  (case comment of
+    SOME kind => output_comment ctxt (kind, syms)
+  | NONE => [Latex.symbols syms])
+and output_document_text ctxt syms =
+  (case Comment.read_body syms of
+    SOME res => maps (output_comment_document ctxt) res
+  | NONE => [Latex.symbols syms])
+and output_document ctxt {markdown} source =
   let
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
 
-    val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt);
+    val output_antiquotes =
+      maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt);
 
     fun output_line line =
       (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
@@ -61,14 +85,14 @@
     else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
     then
       let
-        val ants = Antiquote.parse pos syms;
+        val ants = Antiquote.parse_comments pos syms;
         val reports = Antiquote.antiq_reports ants;
         val blocks = Markdown.read_antiquotes ants;
         val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
       in output_blocks blocks end
     else
       let
-        val ants = Antiquote.parse pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
+        val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
         val reports = Antiquote.antiq_reports ants;
         val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
       in output_antiquotes ants end
@@ -79,8 +103,6 @@
 
 local
 
-val output_symbols = single o Latex.symbols_output;
-
 val output_symbols_antiq =
   (fn Antiquote.Text syms => output_symbols syms
     | Antiquote.Control {name = (name, _), body, ...} =>
@@ -89,32 +111,19 @@
     | Antiquote.Antiq {body, ...} =>
         Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
 
-fun output_symbols_comment ctxt {antiq} (comment, syms) =
+fun output_comment_symbols ctxt {antiq} (comment, syms) =
   (case (comment, antiq) of
     (NONE, false) => output_symbols syms
   | (NONE, true) =>
-      Antiquote.parse (#1 (Symbol_Pos.range syms)) syms
+      Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms
       |> maps output_symbols_antiq
-  | (SOME Comment.Comment, _) =>
-      let
-        val source = Input.cartouche_content syms;
-        val ctxt' = ctxt
-          |> Config.put Document_Antiquotation.thy_output_display false;
-      in
-        output_document ctxt' {markdown = false} source
-        |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
-      end
-  | (SOME Comment.Cancel, _) =>
-      output_symbols (Symbol_Pos.cartouche_content syms)
-      |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
-  | (SOME Comment.Latex, _) =>
-      [Latex.symbols (Symbol_Pos.cartouche_content syms)]);
+  | (SOME comment, _) => output_comment ctxt (comment, syms));
 
 in
 
 fun output_body ctxt antiq bg en syms =
   (case Comment.read_body syms of
-    SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res
+    SOME res => maps (output_comment_symbols ctxt {antiq = antiq}) res
   | NONE => output_symbols syms) |> Latex.enclose_body bg en
 and output_token ctxt tok =
   let
@@ -145,7 +154,7 @@
       val _ =
         comment |> Option.app (fn kind =>
           Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));
-      val _ = output_symbols_comment ctxt {antiq = false} (comment, syms);
+      val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
 
 end;

--- a/src/Pure/Tools/rail.ML	Sat Feb 03 15:34:22 2018 +0100
+++ b/src/Pure/Tools/rail.ML	Sat Feb 03 20:34:26 2018 +0100
@@ -340,7 +340,9 @@
 fun output_rules ctxt rules =
   let
     val output_antiq =
-      Latex.output_text o Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
+      Antiquote.Antiq #>
+      Document_Antiquotation.evaluate (single o Latex.symbols) ctxt #>
+      Latex.output_text;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"