src/Pure/General/antiquote.ML
changeset 30589 cbe27c4ef417
parent 30587 ad19c99529eb
child 30590 1d9c9fcf8513
     1.1 --- a/src/Pure/General/antiquote.ML	Thu Mar 19 15:22:53 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Thu Mar 19 15:44:14 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature ANTIQUOTE =
     1.5  sig
     1.6    datatype antiquote =
     1.7 -    Text of string | Antiq of Symbol_Pos.T list * Position.T |
     1.8 +    Text of Symbol_Pos.T list | Antiq of Symbol_Pos.T list * Position.T |
     1.9      Open of Position.T | Close of Position.T
    1.10    val is_antiq: antiquote -> bool
    1.11    val read: Symbol_Pos.T list * Position.T -> antiquote list
    1.12 @@ -19,7 +19,7 @@
    1.13  (* datatype antiquote *)
    1.14  
    1.15  datatype antiquote =
    1.16 -  Text of string |
    1.17 +  Text of Symbol_Pos.T list |
    1.18    Antiq of Symbol_Pos.T list * Position.T |
    1.19    Open of Position.T |
    1.20    Close of Position.T;
    1.21 @@ -68,7 +68,7 @@
    1.22  in
    1.23  
    1.24  val scan_antiquote =
    1.25 - (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
    1.26 + (Scan.repeat1 scan_txt >> (Text o flat) ||
    1.27    scan_antiq ||
    1.28    Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
    1.29    Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);