allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
authorwenzelm
Sat Apr 30 23:20:50 2011 +0200 (2011-04-30)
changeset 42508e21362bf1d93
parent 42507 651aef3cc854
child 42509 9d107a52b634
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
src/Pure/General/antiquote.ML
src/Pure/Thy/rail.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Sat Apr 30 20:58:36 2011 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Sat Apr 30 23:20:50 2011 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val is_text: 'a antiquote -> bool
     1.5    val report: ('a -> unit) -> 'a antiquote -> unit
     1.6    val check_nesting: 'a antiquote list -> unit
     1.7 +  val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
     1.8    val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
     1.9    val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
    1.10    val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list
    1.11 @@ -75,17 +76,17 @@
    1.12    Scan.trace (Symbol_Pos.scan_string_qq || Symbol_Pos.scan_string_bq) >> #2 ||
    1.13    Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    1.14  
    1.15 +val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    1.16 +val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
    1.17 +
    1.18 +in
    1.19 +
    1.20  val scan_antiq =
    1.21    Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    1.22      Symbol_Pos.!!! "missing closing brace of antiquotation"
    1.23        (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    1.24    >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    1.25  
    1.26 -val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    1.27 -val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
    1.28 -
    1.29 -in
    1.30 -
    1.31  fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
    1.32  val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
    1.33  
     2.1 --- a/src/Pure/Thy/rail.ML	Sat Apr 30 20:58:36 2011 +0200
     2.2 +++ b/src/Pure/Thy/rail.ML	Sat Apr 30 23:20:50 2011 +0200
     2.3 @@ -12,7 +12,8 @@
     2.4  
     2.5  (* datatype token *)
     2.6  
     2.7 -datatype kind = Keyword | Ident | String | EOF;
     2.8 +datatype kind =
     2.9 +  Keyword | Ident | String | Antiq of bool * (Symbol_Pos.T list * Position.range) | EOF;
    2.10  
    2.11  datatype token = Token of Position.range * (kind * string);
    2.12  
    2.13 @@ -29,6 +30,7 @@
    2.14   fn Keyword => "rail keyword"
    2.15    | Ident => "identifier"
    2.16    | String => "single-quoted string"
    2.17 +  | Antiq _ => "antiquotation"
    2.18    | EOF => "end-of-file";
    2.19  
    2.20  fun print (Token ((pos, _), (k, x))) =
    2.21 @@ -65,7 +67,9 @@
    2.22    scan_space >> K [] ||
    2.23    scan_keyword >> (token Keyword o single) ||
    2.24    Lexicon.scan_id >> token Ident ||
    2.25 -  Symbol_Pos.scan_string_q >> (token String o #1 o #2);
    2.26 +  Symbol_Pos.scan_string_q >> (token String o #1 o #2) ||
    2.27 +  (Symbol_Pos.$$$ "@" |-- Antiquote.scan_antiq >> pair true || Antiquote.scan_antiq >> pair false)
    2.28 +    >> (fn antiq as (_, (ss, _)) => token (Antiq antiq) ss);
    2.29  
    2.30  val scan =
    2.31    (Scan.repeat scan_token >> flat) --|
    2.32 @@ -104,11 +108,11 @@
    2.33  fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
    2.34  fun enum sep scan = enum1 sep scan || Scan.succeed [];
    2.35  
    2.36 -fun parse_token kind =
    2.37 -  Scan.some (fn tok => if kind_of tok = kind then SOME (content_of tok) else NONE);
    2.38 +val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
    2.39 +val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
    2.40  
    2.41 -val ident = parse_token Ident;
    2.42 -val string = parse_token String;
    2.43 +val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
    2.44 +val plain_antiq = Scan.some (fn tok => (case kind_of tok of Antiq (false, a) => SOME a | _ => NONE));
    2.45  
    2.46  
    2.47  
    2.48 @@ -123,7 +127,8 @@
    2.49    Plus of rails * rails |
    2.50    Newline of int |
    2.51    Nonterminal of string |
    2.52 -  Terminal of string;
    2.53 +  Terminal of string |
    2.54 +  Antiquote of bool * (Symbol_Pos.T list * Position.range);
    2.55  
    2.56  fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
    2.57  and reverse (Bar cats) = Bar (map reverse_cat cats)
    2.58 @@ -166,10 +171,12 @@
    2.59   ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
    2.60    $$$ "\\" >> K (Newline 0) ||
    2.61    ident >> Nonterminal ||
    2.62 -  string >> Terminal) x
    2.63 +  string >> Terminal ||
    2.64 +  antiq >> Antiquote) x
    2.65  and body4e x = (Scan.option body4 >> (cat o the_list)) x;
    2.66  
    2.67 -val rule = ident -- ($$$ ":" |-- !!! body) || body >> pair "";
    2.68 +val rule_name = ident >> Antiquote.Text || plain_antiq >> Antiquote.Antiq;
    2.69 +val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
    2.70  val rules = enum1 ";" (Scan.option rule) >> map_filter I;
    2.71  
    2.72  in
    2.73 @@ -202,44 +209,54 @@
    2.74    | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
    2.75    | vertical_range atom y = (atom, y + 1);
    2.76  
    2.77 -
    2.78 -fun output_text s = "\\isa{" ^ Output.output s ^ "}";
    2.79 +fun output_rules state rules =
    2.80 +  let
    2.81 +    val output_antiq = Thy_Output.eval_antiq (#1 (Keyword.get_lexicons ())) state;
    2.82 +    fun output_text s = "\\isa{" ^ Output.output s ^ "}";
    2.83  
    2.84 -fun output_cat c (Cat (_, rails)) = outputs c rails
    2.85 -and outputs c [rail] = output c rail
    2.86 -  | outputs _ rails = implode (map (output "") rails)
    2.87 -and output _ (Bar []) = ""
    2.88 -  | output c (Bar [cat]) = output_cat c cat
    2.89 -  | output _ (Bar (cat :: cats)) =
    2.90 -      "\\rail@bar\n" ^ output_cat "" cat ^
    2.91 -      implode (map (fn Cat (y, rails) =>
    2.92 -          "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
    2.93 -      "\\rail@endbar\n"
    2.94 -  | output c (Plus (cat, Cat (y, rails))) =
    2.95 -      "\\rail@plus\n" ^ output_cat c cat ^
    2.96 -      "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
    2.97 -      "\\rail@endplus\n"
    2.98 -  | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
    2.99 -  | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text s ^ "}[]\n"
   2.100 -  | output c (Terminal s) = "\\rail@" ^ c ^ "term{" ^ output_text s ^ "}[]\n";
   2.101 +    fun output_cat c (Cat (_, rails)) = outputs c rails
   2.102 +    and outputs c [rail] = output c rail
   2.103 +      | outputs _ rails = implode (map (output "") rails)
   2.104 +    and output _ (Bar []) = ""
   2.105 +      | output c (Bar [cat]) = output_cat c cat
   2.106 +      | output _ (Bar (cat :: cats)) =
   2.107 +          "\\rail@bar\n" ^ output_cat "" cat ^
   2.108 +          implode (map (fn Cat (y, rails) =>
   2.109 +              "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
   2.110 +          "\\rail@endbar\n"
   2.111 +      | output c (Plus (cat, Cat (y, rails))) =
   2.112 +          "\\rail@plus\n" ^ output_cat c cat ^
   2.113 +          "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
   2.114 +          "\\rail@endplus\n"
   2.115 +      | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
   2.116 +      | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text s ^ "}[]\n"
   2.117 +      | output c (Terminal s) = "\\rail@" ^ c ^ "term{" ^ output_text s ^ "}[]\n"
   2.118 +      | output c (Antiquote (b, a)) =
   2.119 +          "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
   2.120  
   2.121 -fun output_rule (name, rail) =
   2.122 -  let val (rail', y') = vertical_range rail 0 in
   2.123 -    "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ output_text name ^ "}\n" ^
   2.124 -    output "" rail' ^
   2.125 -    "\\rail@end\n"
   2.126 +    fun output_rule (name, rail) =
   2.127 +      let
   2.128 +        val (rail', y') = vertical_range rail 0;
   2.129 +        val out_name =
   2.130 +          (case name of
   2.131 +            Antiquote.Text s => output_text s
   2.132 +          | Antiquote.Antiq a => output_antiq a);
   2.133 +      in
   2.134 +        "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
   2.135 +        output "" rail' ^
   2.136 +        "\\rail@end\n"
   2.137 +      end;
   2.138 +  in
   2.139 +    "\\begin{railoutput}\n" ^
   2.140 +    implode (map output_rule rules) ^
   2.141 +    "\\end{railoutput}\n"
   2.142    end;
   2.143  
   2.144 -fun output_rules rules =
   2.145 -  "\\begin{railoutput}\n" ^
   2.146 -  implode (map output_rule rules) ^
   2.147 -  "\\end{railoutput}\n";
   2.148 -
   2.149  in
   2.150  
   2.151  val _ =
   2.152    Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
   2.153 -    (fn _ => output_rules o read);
   2.154 +    (fn {state, ...} => output_rules state o read);
   2.155  
   2.156  end;
   2.157  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Sat Apr 30 20:58:36 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Apr 30 23:20:50 2011 +0200
     3.3 @@ -27,6 +27,7 @@
     3.4      ({source: Args.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> unit
     3.5    datatype markup = Markup | MarkupEnv | Verbatim
     3.6    val modes: string list Unsynchronized.ref
     3.7 +  val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
     3.8    val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
     3.9    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    3.10      (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
    3.11 @@ -173,17 +174,19 @@
    3.12  
    3.13  val modes = Unsynchronized.ref ([]: string list);
    3.14  
    3.15 +fun eval_antiq lex state (ss, (pos, _)) =
    3.16 +  let
    3.17 +    val (opts, src) = Token.read_antiq lex antiq (ss, pos);
    3.18 +    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
    3.19 +    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
    3.20 +    val print_ctxt = Context_Position.set_visible false preview_ctxt;
    3.21 +    val _ = cmd preview_ctxt;
    3.22 +  in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end;
    3.23 +
    3.24  fun eval_antiquote lex state (txt, pos) =
    3.25    let
    3.26      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
    3.27 -      | expand (Antiquote.Antiq (ss, (pos, _))) =
    3.28 -          let
    3.29 -            val (opts, src) = Token.read_antiq lex antiq (ss, pos);
    3.30 -            fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
    3.31 -            val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
    3.32 -            val print_ctxt = Context_Position.set_visible false preview_ctxt;
    3.33 -            val _ = cmd preview_ctxt;
    3.34 -          in Print_Mode.with_modes (! modes @ Latex.modes) (fn () => cmd print_ctxt) () end
    3.35 +      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq
    3.36        | expand (Antiquote.Open _) = ""
    3.37        | expand (Antiquote.Close _) = "";
    3.38      val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);