src/Pure/General/symbol_pos.ML
changeset 48764 4fe0920d5049
parent 48743 a72f8ffecf31
child 48770 85eeb06ec1c4
     1.1 --- a/src/Pure/General/symbol_pos.ML	Fri Aug 10 21:53:20 2012 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Fri Aug 10 22:25:45 2012 +0200
     1.3 @@ -16,9 +16,9 @@
     1.4    val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
     1.5    val change_prompt: ('a -> 'b) -> 'a -> 'b
     1.6    val scan_pos: T list -> Position.T * T list
     1.7 -  val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
     1.8 -  val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
     1.9 -  val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
    1.10 +  val scan_string_q: string -> T list -> (Position.T * (T list * Position.T)) * T list
    1.11 +  val scan_string_qq: string -> T list -> (Position.T * (T list * Position.T)) * T list
    1.12 +  val scan_string_bq: string -> T list -> (Position.T * (T list * Position.T)) * T list
    1.13    val recover_string_q: T list -> T list * T list
    1.14    val recover_string_qq: T list -> T list * T list
    1.15    val recover_string_bq: T list -> T list * T list
    1.16 @@ -94,16 +94,17 @@
    1.17      let val (n, _) = Library.read_int [a, b, c]
    1.18      in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
    1.19  
    1.20 -fun scan_str q =
    1.21 -  $$$ "\\" |-- !!! (fn () => "bad escape character in string") ($$$ q || $$$ "\\" || char_code) ||
    1.22 +fun scan_str q err_prefix =
    1.23 +  $$$ "\\" |-- !!! (fn () => err_prefix ^ "bad escape character in string")
    1.24 +    ($$$ q || $$$ "\\" || char_code) ||
    1.25    Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    1.26  
    1.27 -fun scan_strs q =
    1.28 -  (scan_pos --| $$$ q) -- !!! (fn () => "missing quote at end of string")
    1.29 -    (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
    1.30 +fun scan_strs q err_prefix =
    1.31 +  (scan_pos --| $$$ q) -- !!! (fn () => err_prefix ^ "missing quote at end of string")
    1.32 +    (change_prompt ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
    1.33  
    1.34  fun recover_strs q =
    1.35 -  $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q)) >> flat);
    1.36 +  $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
    1.37  
    1.38  in
    1.39