src/Pure/General/symbol_pos.ML
changeset 44818 9b00f09f7721
parent 44647 e8ba493027a3
child 49758 a72f8ffecf31
equal deleted inserted replaced
44817:ba88bb44c192 44818:9b00f09f7721
    11   val $$$ : Symbol.symbol -> T list -> T list * T list
    11   val $$$ : Symbol.symbol -> T list -> T list * T list
    12   val ~$$$ : Symbol.symbol -> T list -> T list * T list
    12   val ~$$$ : Symbol.symbol -> T list -> T list * T list
    13   val content: T list -> string
    13   val content: T list -> string
    14   val is_eof: T -> bool
    14   val is_eof: T -> bool
    15   val stopper: T Scan.stopper
    15   val stopper: T Scan.stopper
    16   val !!! : string -> (T list -> 'a) -> T list -> 'a
    16   val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
    17   val change_prompt: ('a -> 'b) -> 'a -> 'b
    17   val change_prompt: ('a -> 'b) -> 'a -> 'b
    18   val scan_pos: T list -> Position.T * T list
    18   val scan_pos: T list -> Position.T * T list
    19   val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
    19   val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
    20   val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
    20   val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
    21   val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
    21   val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
    63 fun !!! text scan =
    63 fun !!! text scan =
    64   let
    64   let
    65     fun get_pos [] = " (past end-of-text!)"
    65     fun get_pos [] = " (past end-of-text!)"
    66       | get_pos ((_, pos) :: _) = Position.str_of pos;
    66       | get_pos ((_, pos) :: _) = Position.str_of pos;
    67 
    67 
    68     fun err (syms, msg) =
    68     fun err (syms, msg) = fn () =>
    69       text ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
    69       text () ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
    70       (case msg of NONE => "" | SOME s => "\n" ^ s);
    70       (case msg of NONE => "" | SOME m => "\n" ^ m ());
    71   in Scan.!! err scan end;
    71   in Scan.!! err scan end;
    72 
    72 
    73 fun change_prompt scan = Scan.prompt "# " scan;
    73 fun change_prompt scan = Scan.prompt "# " scan;
    74 
    74 
    75 fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
    75 fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
    89   (fn (((a, pos), (b, _)), (c, _)) =>
    89   (fn (((a, pos), (b, _)), (c, _)) =>
    90     let val (n, _) = Library.read_int [a, b, c]
    90     let val (n, _) = Library.read_int [a, b, c]
    91     in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
    91     in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
    92 
    92 
    93 fun scan_str q =
    93 fun scan_str q =
    94   $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
    94   $$$ "\\" |-- !!! (fn () => "bad escape character in string") ($$$ q || $$$ "\\" || char_code) ||
    95   Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    95   Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
    96 
    96 
    97 fun scan_strs q =
    97 fun scan_strs q =
    98   (scan_pos --| $$$ q) -- !!! "missing quote at end of string"
    98   (scan_pos --| $$$ q) -- !!! (fn () => "missing quote at end of string")
    99     (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
    99     (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
   100 
   100 
   101 in
   101 in
   102 
   102 
   103 val scan_string_q = scan_strs "'";
   103 val scan_string_q = scan_strs "'";