src/Tools/WWW_Find/unicode_symbols.ML
changeset 43947 9b00f09f7721
parent 43602 8c89a1fb30f2
child 48992 0518bf89c777
     1.1 --- a/src/Tools/WWW_Find/unicode_symbols.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Tools/WWW_Find/unicode_symbols.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -103,12 +103,13 @@
     1.4        Scan.literal keywords >> token Keyword ||
     1.5        scan_ascii_symbol ||
     1.6        Lexicon.scan_id >> token Name;
     1.7 -    val scan_token = Symbol_Pos.!!! "Lexical error" (Scan.bulk scanner);
     1.8 +    val scan_token = Symbol_Pos.!!! (fn () => "Lexical error") (Scan.bulk scanner);
     1.9    in
    1.10      (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
    1.11        (toks, []) => toks
    1.12 -    | (_, ss) => error ("Lexical error at: " ^ Symbol_Pos.content ss
    1.13 -                        ^ Position.str_of (#1 (Symbol_Pos.range ss))))
    1.14 +    | (_, ss) =>
    1.15 +        error ("Lexical error at: " ^ Symbol_Pos.content ss ^
    1.16 +          Position.str_of (#1 (Symbol_Pos.range ss))))
    1.17    end;
    1.18  
    1.19  val stopper =