equal
deleted
inserted
replaced
790 let |
790 let |
791 val msg = |
791 val msg = |
792 if null toks then Pretty.str "Inner syntax error: unexpected end of input" |
792 if null toks then Pretty.str "Inner syntax error: unexpected end of input" |
793 else |
793 else |
794 Pretty.block (Pretty.str "Inner syntax error at: \"" :: |
794 Pretty.block (Pretty.str "Inner syntax error at: \"" :: |
795 Pretty.breaks (map (Pretty.str o Symbol.output o str_of_token) |
795 Pretty.breaks (map (Pretty.str o str_of_token) |
796 (rev (tl (rev toks)))) @ |
796 (rev (tl (rev toks)))) @ |
797 [Pretty.str "\""]); |
797 [Pretty.str "\""]); |
798 val expected = |
798 val expected = |
799 Pretty.strs ("Expected tokens: " :: map (quote o str_of_token) allowed); |
799 Pretty.strs ("Expected tokens: " :: map (quote o str_of_token) allowed); |
800 in |
800 in |