# HG changeset patch
# User haftmann
# Date 1415434607 -3600
# Node ID 994fe0ba8335686c573df81ff0621a328059cf8e
# Parent  0c45680b7d9d9da994a40cd3a3201d34ad99370c
less space-wasting serialization setup: highest cell of array has been unused so far

diff -r 0c45680b7d9d -r 994fe0ba8335 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Nov 07 23:35:13 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sat Nov 08 09:16:47 2014 +0100
@@ -566,16 +566,16 @@
 writeSTRef = Data.STRef.writeSTRef;
 
 newArray :: Integer -> a -> ST s (STArray s a);
-newArray k = Data.Array.ST.newArray (0, k);
+newArray k = Data.Array.ST.newArray (0, k - 1);
 
 newListArray :: [a] -> ST s (STArray s a);
-newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs) xs;
+newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs - 1) xs;
 
 newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a);
-newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
+newFunArray k f = Data.Array.ST.newListArray (0, k - 1) (map f [0..k-1]);
 
 lengthArray :: STArray s a -> ST s Integer;
-lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
+lengthArray a = Control.Monad.liftM (\(_, l) -> l + 1) (Data.Array.ST.getBounds a);
 
 readArray :: STArray s a -> Integer -> ST s a;
 readArray = Data.Array.ST.readArray;
diff -r 0c45680b7d9d -r 994fe0ba8335 src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Fri Nov 07 23:35:13 2014 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala	Sat Nov 08 09:16:47 2014 +0100
@@ -22,7 +22,7 @@
   /* font rendering information */
 
   val font_family: String = "IsabelleText"
-  val font_size: Int = 14
+  val font_size: Int = 32
   val font = new Font(font_family, Font.BOLD, font_size)
 
   val rendering_hints =
@@ -41,7 +41,7 @@
 
   /* rendering parameters */
 
-  val gap_x = 20
+  val gap_x = 5
   val pad_x = 8
   val pad_y = 5