--- a/src/Pure/Isar/parse.scala Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/parse.scala Sat Nov 01 15:01:41 2014 +0100
@@ -39,13 +39,7 @@
}
val token = in.first
if (pred(token)) Success((token, pos), proper(in.rest))
- else
- token.text match {
- case (txt, "") =>
- Failure(s + " expected,\nbut " + txt + " was found", in)
- case (txt1, txt2) =>
- Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
- }
+ else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
}
}
}