--- 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 --| $$ "'" --| $$ "'");
--- 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);
--- 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;
--- 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;