src/Pure/General/antiquote.ML
changeset 30683 e8ac1f9d9469
parent 30641 72980f8d7ee8
child 39507 839873937ddd
     1.1 --- a/src/Pure/General/antiquote.ML	Tue Mar 24 11:39:25 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Tue Mar 24 11:57:41 2009 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    datatype 'a antiquote =
     1.6      Text of 'a |
     1.7 -    Antiq of Symbol_Pos.T list * Position.T |
     1.8 +    Antiq of Symbol_Pos.T list * Position.range |
     1.9      Open of Position.T |
    1.10      Close of Position.T
    1.11    val is_text: 'a antiquote -> bool
    1.12 @@ -26,7 +26,7 @@
    1.13  
    1.14  datatype 'a antiquote =
    1.15    Text of 'a |
    1.16 -  Antiq of Symbol_Pos.T list * Position.T |
    1.17 +  Antiq of Symbol_Pos.T list * Position.range |
    1.18    Open of Position.T |
    1.19    Close of Position.T;
    1.20  
    1.21 @@ -39,7 +39,7 @@
    1.22  val report_antiq = Position.report Markup.antiq;
    1.23  
    1.24  fun report report_text (Text x) = report_text x
    1.25 -  | report _ (Antiq (_, pos)) = report_antiq pos
    1.26 +  | report _ (Antiq (_, (pos, _))) = report_antiq pos
    1.27    | report _ (Open pos) = report_antiq pos
    1.28    | report _ (Close pos) = report_antiq pos;
    1.29  
    1.30 @@ -79,7 +79,7 @@
    1.31    Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    1.32      Symbol_Pos.!!! "missing closing brace of antiquotation"
    1.33        (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    1.34 -  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
    1.35 +  >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    1.36  
    1.37  val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    1.38  val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";