# HG changeset patch
# User wenzelm
# Date 899393207 -7200
# Node ID 9e74cf11e4a41fa999c3ce5f28b0e80feb7595ab
# Parent  8f4b72f0c15d9fc58333d355dbdf4fef6147219b
Symbol.beginning;

diff -r 8f4b72f0c15d -r 9e74cf11e4a4 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Jul 02 16:53:55 1998 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Jul 02 17:26:47 1998 +0200
@@ -229,7 +229,7 @@
 val scan_str =
   $$ "'" |-- $$ "'" |--
     !! (fn (cs, _) => "Inner lexical error: malformed literal string at " ^
-      quote ("''" ^ beginning cs))
+      quote ("''" ^ Symbol.beginning cs))
     (Scan.repeat scan_chr --| $$ "'" --| $$ "'");
 
 
diff -r 8f4b72f0c15d -r 9e74cf11e4a4 src/Pure/Syntax/symbol.ML
--- a/src/Pure/Syntax/symbol.ML	Thu Jul 02 16:53:55 1998 +0200
+++ b/src/Pure/Syntax/symbol.ML	Thu Jul 02 17:26:47 1998 +0200
@@ -20,6 +20,7 @@
   val is_letdig: symbol -> bool
   val is_blank: symbol -> bool
   val is_printable: symbol -> bool
+  val beginning: symbol list -> string
   val scan: string list -> symbol * string list
   val explode: string -> symbol list
   val input: string -> string
@@ -201,6 +202,18 @@
   size s > 2 andalso nth_elem (2, explode s) <> "^";
 
 
+(* beginning *)
+
+val smash_blanks = map (fn s => if is_blank s then space else s);
+
+fun beginning raw_ss =
+  let
+    val (all_ss, _) = take_suffix is_blank raw_ss;
+    val dots = if length all_ss > 10 then " ..." else "";
+    val (ss, _) = take_suffix is_blank (take (10, all_ss));
+  in implode (smash_blanks ss) ^ dots end;
+
+
 (* scan *)
 
 val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
diff -r 8f4b72f0c15d -r 9e74cf11e4a4 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Thu Jul 02 16:53:55 1998 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Thu Jul 02 17:26:47 1998 +0200
@@ -146,7 +146,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 (beginning cs))))
+    | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (Symbol.beginning cs))))
   end;
 
 
diff -r 8f4b72f0c15d -r 9e74cf11e4a4 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jul 02 16:53:55 1998 +0200
+++ b/src/Pure/library.ML	Thu Jul 02 17:26:47 1998 +0200
@@ -116,7 +116,6 @@
   val string_of_indexname: string * int -> string
 
   (*strings*)
-  val beginning: string list -> string
   val enclose: string -> string -> string -> string
   val quote: string -> string
   val space_implode: string -> string list -> string
@@ -636,10 +635,6 @@
 
 (** strings **)
 
-(*beginning of text*)
-fun beginning cs =
-  implode (map (fn c => if ord c < ord " " then " " else c) (take (10, cs))) ^ " ...";
-
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;