src/Pure/Thy/rail.ML
changeset 48764 4fe0920d5049
parent 43947 9b00f09f7721
child 48911 5debc3e4fa81
     1.1 --- a/src/Pure/Thy/rail.ML	Fri Aug 10 21:53:20 2012 +0200
     1.2 +++ b/src/Pure/Thy/rail.ML	Fri Aug 10 22:25:45 2012 +0200
     1.3 @@ -63,16 +63,18 @@
     1.4  val scan_keyword =
     1.5    Scan.one (member (op =) ["|", "*", "+", "?", "(", ")", "\\", ";", ":", "@"] o Symbol_Pos.symbol);
     1.6  
     1.7 +val err_prefix = "Rail lexical error: ";
     1.8 +
     1.9  val scan_token =
    1.10    scan_space >> K [] ||
    1.11    Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
    1.12    scan_keyword >> (token Keyword o single) ||
    1.13    Lexicon.scan_id >> token Ident ||
    1.14 -  Symbol_Pos.scan_string_q >> (token String o #1 o #2);
    1.15 +  Symbol_Pos.scan_string_q err_prefix >> (token String o #1 o #2);
    1.16  
    1.17  val scan =
    1.18    (Scan.repeat scan_token >> flat) --|
    1.19 -    Symbol_Pos.!!! (fn () => "Rail lexical error: bad input")
    1.20 +    Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
    1.21        (Scan.ahead (Scan.one Symbol_Pos.is_eof));
    1.22  
    1.23  in