src/Pure/General/antiquote.ML
changeset 42508 e21362bf1d93
parent 42503 27514b6fbe93
child 43947 9b00f09f7721
     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