# HG changeset patch
# User wenzelm
# Date 1084210002 -7200
# Node ID 0e987111a17e92aa24c5974464f7b4b174cf8bf9
# Parent  df34201f1a15313504353eab6b024e9a41a78937
changed Symbol.beginning;

diff -r df34201f1a15 -r 0e987111a17e src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Mon May 10 19:26:25 2004 +0200
+++ b/src/Pure/Isar/antiquote.ML	Mon May 10 19:26:42 2004 +0200
@@ -72,7 +72,7 @@
       (pos, Symbol.explode s) of
     (xs, (_, [])) => xs
   | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
-      quote (Symbol.beginning ss) ^ Position.str_of pos'));
+      quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
 
 
 end;
diff -r df34201f1a15 -r 0e987111a17e src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Mon May 10 19:26:25 2004 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Mon May 10 19:26:42 2004 +0200
@@ -264,7 +264,7 @@
             Syntax.scan_nat >> token Nat ||
             scan_symid >> token SymIdent))
       end) >> #2;
-  in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning cs))) scanner end;
+  in !! (lex_err (fn cs => "bad input " ^ quote (Symbol.beginning 10 cs))) scanner end;
 
 
 (* token sources *)
diff -r df34201f1a15 -r 0e987111a17e src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Mon May 10 19:26:25 2004 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Mon May 10 19:26:42 2004 +0200
@@ -143,7 +143,7 @@
   in
     (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
       (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
-    | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning cs))))
+    | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning 10 cs))))
   end;