# HG changeset patch
# User wenzelm
# Date 977608385 -3600
# Node ID 3a610089c43ba91bc3a3ef5a67910362779cf6a9
# Parent  c130eb1e863fde13fd20ddd0536d6b64ecc7aaa8
tuned length;

diff -r c130eb1e863f -r 3a610089c43b src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Dec 23 22:52:41 2000 +0100
+++ b/src/Pure/General/symbol.ML	Sat Dec 23 22:53:05 2000 +0100
@@ -102,7 +102,11 @@
   is_symbolic s;
 
 
-fun sym_length ss = foldl (fn (n, s) => if is_printable s then n + 1 else n) (0, ss);
+fun sym_length ss = foldl (fn (n, s) =>
+  (if not (is_printable s) then 0 else
+    (case Library.try String.substring (s, 2, 4) of
+      Some s' => if s' = "long" orelse s' = "Long" then 2 else 1
+    | None => 1)) + n) (0, ss);
 
 
 (* beginning *)
@@ -313,7 +317,7 @@
 
 fun default_output s =
   if not (exists_string (equal "\\") s) then string_size s
-  else string_size (implode (map (fn "\\" => "\\\\" | c => c) (explode s)));	(*sic!*)
+  else string_size (implode (map (fn "\\" => "\\\\" | c => c) (explode s)));    (*sic!*)
 
 
 (* isabelle_font_output *)