src/Pure/General/symbol_pos.ML
changeset 30586 9674f64a0702
parent 30573 49899f26fbd1
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Mar 19 13:28:55 2009 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Mar 19 15:22:53 2009 +0100
     1.3 @@ -20,7 +20,11 @@
     1.4    val is_eof: T -> bool
     1.5    val stopper: T Scan.stopper
     1.6    val !!! : string -> (T list -> 'a) -> T list -> 'a
     1.7 +  val change_prompt: ('a -> 'b) -> 'a -> 'b
     1.8    val scan_pos: T list -> Position.T * T list
     1.9 +  val scan_string: T list -> (Position.T * (T list * Position.T)) * T list
    1.10 +  val scan_alt_string: T list -> (Position.T * (T list * Position.T)) * T list
    1.11 +  val scan_quoted: T list -> T list * T list
    1.12    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.13      T list -> T list * T list
    1.14    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.15 @@ -83,12 +87,44 @@
    1.16        (case msg of NONE => "" | SOME s => "\n" ^ s);
    1.17    in Scan.!! err scan end;
    1.18  
    1.19 +fun change_prompt scan = Scan.prompt "# " scan;
    1.20 +
    1.21  fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
    1.22  fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
    1.23  
    1.24  val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
    1.25  
    1.26  
    1.27 +(* Isabelle strings *)
    1.28 +
    1.29 +local
    1.30 +
    1.31 +val char_code =
    1.32 +  Scan.one (Symbol.is_ascii_digit o symbol) --
    1.33 +  Scan.one (Symbol.is_ascii_digit o symbol) --
    1.34 +  Scan.one (Symbol.is_ascii_digit o symbol) :|--
    1.35 +  (fn (((a, pos), (b, _)), (c, _)) =>
    1.36 +    let val (n, _) = Library.read_int [a, b, c]
    1.37 +    in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
    1.38 +
    1.39 +fun scan_str q =
    1.40 +  $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
    1.41 +  Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    1.42 +
    1.43 +fun scan_strs q =
    1.44 +  (scan_pos --| $$$ q) -- !!! "missing quote at end of string"
    1.45 +    (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
    1.46 +
    1.47 +in
    1.48 +
    1.49 +val scan_string = scan_strs "\"";
    1.50 +val scan_alt_string = scan_strs "`";
    1.51 +
    1.52 +val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
    1.53 +
    1.54 +end;
    1.55 +
    1.56 +
    1.57  (* ML-style comments *)
    1.58  
    1.59  local
    1.60 @@ -99,7 +135,7 @@
    1.61    Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
    1.62    Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
    1.63  
    1.64 -val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
    1.65 +val scan_body = change_prompt (Scan.pass 0 (Scan.repeat scan_cmt >> flat));
    1.66  
    1.67  in
    1.68