allow nested @{antiq} (nonterminal) and @@{antiq} terminal;

--- a/src/Pure/General/antiquote.ML	Sat Apr 30 20:58:36 2011 +0200
+++ b/src/Pure/General/antiquote.ML	Sat Apr 30 23:20:50 2011 +0200
@@ -14,6 +14,7 @@
   val is_text: 'a antiquote -> bool
   val report: ('a -> unit) -> 'a antiquote -> unit
   val check_nesting: 'a antiquote list -> unit
+  val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
   val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
   val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
@@ -75,17 +76,17 @@
   Scan.trace (Symbol_Pos.scan_string_qq || Symbol_Pos.scan_string_bq) >> #2 ||
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
 
+val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
+val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
+
+in
+
 val scan_antiq =
   Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
     Symbol_Pos.!!! "missing closing brace of antiquotation"
       (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
   >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
 
-val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
-val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
-
-in
-
 fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
 val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
 

--- a/src/Pure/Thy/rail.ML	Sat Apr 30 20:58:36 2011 +0200
+++ b/src/Pure/Thy/rail.ML	Sat Apr 30 23:20:50 2011 +0200
@@ -12,7 +12,8 @@
 
 (* datatype token *)
 
-datatype kind = Keyword | Ident | String | EOF;
+datatype kind =
+  Keyword | Ident | String | Antiq of bool * (Symbol_Pos.T list * Position.range) | EOF;
 
 datatype token = Token of Position.range * (kind * string);
 
@@ -29,6 +30,7 @@
  fn Keyword => "rail keyword"
   | Ident => "identifier"
   | String => "single-quoted string"
+  | Antiq _ => "antiquotation"
   | EOF => "end-of-file";
 
 fun print (Token ((pos, _), (k, x))) =
@@ -65,7 +67,9 @@
   scan_space >> K [] ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||
-  Symbol_Pos.scan_string_q >> (token String o #1 o #2);
+  Symbol_Pos.scan_string_q >> (token String o #1 o #2) ||
+  (Symbol_Pos.$$$ "@" |-- Antiquote.scan_antiq >> pair true || Antiquote.scan_antiq >> pair false)
+    >> (fn antiq as (_, (ss, _)) => token (Antiq antiq) ss);
 
 val scan =
   (Scan.repeat scan_token >> flat) --|
@@ -104,11 +108,11 @@
 fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
 fun enum sep scan = enum1 sep scan || Scan.succeed [];
 
-fun parse_token kind =
-  Scan.some (fn tok => if kind_of tok = kind then SOME (content_of tok) else NONE);
+val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
+val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
 
-val ident = parse_token Ident;
-val string = parse_token String;
+val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
+val plain_antiq = Scan.some (fn tok => (case kind_of tok of Antiq (false, a) => SOME a | _ => NONE));
 
 
 
@@ -123,7 +127,8 @@
   Plus of rails * rails |
   Newline of int |
   Nonterminal of string |
-  Terminal of string;
+  Terminal of string |
+  Antiquote of bool * (Symbol_Pos.T list * Position.range);
 
 fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
 and reverse (Bar cats) = Bar (map reverse_cat cats)
@@ -166,10 +171,12 @@
  ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   $$$ "\\" >> K (Newline 0) ||
   ident >> Nonterminal ||
-  string >> Terminal) x
+  string >> Terminal ||
+  antiq >> Antiquote) x
 and body4e x = (Scan.option body4 >> (cat o the_list)) x;
 
-val rule = ident -- ($$$ ":" |-- !!! body) || body >> pair "";
+val rule_name = ident >> Antiquote.Text || plain_antiq >> Antiquote.Antiq;
+val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
 val rules = enum1 ";" (Scan.option rule) >> map_filter I;
 
 in
@@ -202,44 +209,54 @@
   | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   | vertical_range atom y = (atom, y + 1);
 
-
-fun output_text s = "\\isa{" ^ Output.output s ^ "}";
+fun output_rules state rules =
+  let
+    val output_antiq = Thy_Output.eval_antiq (#1 (Keyword.get_lexicons ())) state;
+    fun output_text s = "\\isa{" ^ Output.output s ^ "}";
 
-fun output_cat c (Cat (_, rails)) = outputs c rails
-and outputs c [rail] = output c rail
-  | outputs _ rails = implode (map (output "") rails)
-and output _ (Bar []) = ""
-  | output c (Bar [cat]) = output_cat c cat
-  | output _ (Bar (cat :: cats)) =
-      "\\rail@bar\n" ^ output_cat "" cat ^
-      implode (map (fn Cat (y, rails) =>
-          "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
-      "\\rail@endbar\n"
-  | output c (Plus (cat, Cat (y, rails))) =
-      "\\rail@plus\n" ^ output_cat c cat ^
-      "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
-      "\\rail@endplus\n"
-  | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
-  | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text s ^ "}[]\n"
-  | output c (Terminal s) = "\\rail@" ^ c ^ "term{" ^ output_text s ^ "}[]\n";
+    fun output_cat c (Cat (_, rails)) = outputs c rails
+    and outputs c [rail] = output c rail
+      | outputs _ rails = implode (map (output "") rails)
+    and output _ (Bar []) = ""
+      | output c (Bar [cat]) = output_cat c cat
+      | output _ (Bar (cat :: cats)) =
+          "\\rail@bar\n" ^ output_cat "" cat ^
+          implode (map (fn Cat (y, rails) =>
+              "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
+          "\\rail@endbar\n"
+      | output c (Plus (cat, Cat (y, rails))) =
+          "\\rail@plus\n" ^ output_cat c cat ^
+          "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
+          "\\rail@endplus\n"
+      | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
+      | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text s ^ "}[]\n"
+      | output c (Terminal s) = "\\rail@" ^ c ^ "term{" ^ output_text s ^ "}[]\n"
+      | output c (Antiquote (b, a)) =
+          "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
 
-fun output_rule (name, rail) =
-  let val (rail', y') = vertical_range rail 0 in
-    "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ output_text name ^ "}\n" ^
-    output "" rail' ^
-    "\\rail@end\n"
+    fun output_rule (name, rail) =
+      let
+        val (rail', y') = vertical_range rail 0;
+        val out_name =
+          (case name of
+            Antiquote.Text s => output_text s
+          | Antiquote.Antiq a => output_antiq a);
+      in
+        "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
+        output "" rail' ^
+        "\\rail@end\n"
+      end;
+  in
+    "\\begin{railoutput}\n" ^
+    implode (map output_rule rules) ^
+    "\\end{railoutput}\n"
   end;
 
-fun output_rules rules =
-  "\\begin{railoutput}\n" ^
-  implode (map output_rule rules) ^
-  "\\end{railoutput}\n";
-
 in
 
 val _ =
   Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
-    (fn _ => output_rules o read);
+    (fn {state, ...} => output_rules state o read);
 
 end;
 

--- a/src/Pure/Thy/thy_output.ML	Sat Apr 30 20:58:36 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Apr 30 23:20:50 2011 +0200
@@ -27,6 +27,7 @@
     ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit
   datatype markup = Markup | MarkupEnv | Verbatim
   val modes: string list Unsynchronized.ref
+  val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
   val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
   val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
@@ -173,17 +174,19 @@
 
 val modes = Unsynchronized.ref ([]: string list);
 
+fun eval_antiq lex state (ss, (pos, _)) =
+  let
+    val (opts, src) = Token.read_antiq lex antiq (ss, pos);
+    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
+    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
+    val print_ctxt = Context_Position.set_visible false preview_ctxt;
+    val _ = cmd preview_ctxt;
+  in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end;
+
 fun eval_antiquote lex state (txt, pos) =
   let
     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
-      | expand (Antiquote.Antiq (ss, (pos, _))) =
-          let
-            val (opts, src) = Token.read_antiq lex antiq (ss, pos);
-            fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
-            val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
-            val print_ctxt = Context_Position.set_visible false preview_ctxt;
-            val _ = cmd preview_ctxt;
-          in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end
+      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
     val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);