# HG changeset patch
# User wenzelm
# Date 901877610 -7200
# Node ID 7c8abffc4413512b400d222438b9023235056f2d
# Parent  66925577cefe2a6e8c6c2d9cf3d1dde1eff6b014
size / length: printable length;

diff -r 66925577cefe -r 7c8abffc4413 src/Pure/Syntax/symbol.ML
--- a/src/Pure/Syntax/symbol.ML	Fri Jul 31 11:03:31 1998 +0200
+++ b/src/Pure/Syntax/symbol.ML	Fri Jul 31 11:33:30 1998 +0200
@@ -23,6 +23,8 @@
   val beginning: symbol list -> string
   val scan: string list -> symbol * string list
   val explode: string -> symbol list
+  val length: symbol list -> int
+  val size: string -> int
   val input: string -> string
   val output: string -> string
   val source: bool -> (string, 'a) Source.source ->
@@ -246,6 +248,12 @@
   end;
 
 
+(* printable length *)
+
+fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss);
+val sym_size = sym_length o sym_explode;
+
+
 (* input / output *)
 
 fun input str =
@@ -257,8 +265,10 @@
 val output = implode o map char o sym_explode;
 
 
-(*final declaration of this structure!*)
+(*final declarations of this structure!*)
 val explode = sym_explode;
+val length = sym_length;
+val size = sym_size;
 
 
 end;