src/Pure/General/antiquote.ML
changeset 62797 e08c44eed27f
parent 62749 eba34ff9671c
child 67193 4ade0d387429
     1.1 --- a/src/Pure/General/antiquote.ML	Fri Apr 01 17:23:15 2016 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Fri Apr 01 17:37:46 2016 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5  fun range ants =
     1.6    if null ants then Position.no_range
     1.7 -  else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants)));
     1.8 +  else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
     1.9  
    1.10  
    1.11  (* split lines *)
    1.12 @@ -110,9 +110,9 @@
    1.13      Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
    1.14        (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
    1.15      (fn (pos1, (pos2, ((body, pos3), pos4))) =>
    1.16 -      {start = Position.set_range (pos1, pos2),
    1.17 -       stop = Position.set_range (pos3, pos4),
    1.18 -       range = Position.range pos1 pos4,
    1.19 +      {start = Position.range_position (pos1, pos2),
    1.20 +       stop = Position.range_position (pos3, pos4),
    1.21 +       range = Position.range (pos1, pos4),
    1.22         body = body});
    1.23  
    1.24  val scan_antiquote =