less space-wasting serialization setup: highest cell of array has been unused so far
--- 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;
--- 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