# HG changeset patch
# User wenzelm
# Date 1184168871 -7200
# Node ID 1993b865c5ac5cc6b061a231e18670bccc3942e5
# Parent  54ce229dc8583ef100f6968c7ea377dae1b41139
replaced OuterLex.name_of by more sophisticated OuterLex.text_of;

diff -r 54ce229dc858 -r 1993b865c5ac src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Jul 11 17:47:50 2007 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Wed Jul 11 17:47:51 2007 +0200
@@ -96,7 +96,10 @@
 
 fun fail_with s = Scan.fail_with
   (fn [] => s ^ " expected (past end-of-file!)"
-    | (tok :: _) => s ^ " expected,\nbut " ^ T.name_of tok ^ T.pos_of tok ^ " was found");
+    | (tok :: _) =>
+        (case T.text_of tok of
+          (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
+        | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
 
 fun group s scan = scan || fail_with s;