# HG changeset patch
# User haftmann
# Date 1415434797 -3600
# Node ID 7fbeedd05b4cf44d2359d2a73a703d5b4a7e4ba2
# Parent  994fe0ba8335686c573df81ff0621a328059cf8e
reverted commit accident from 994fe0ba8335

diff -r 994fe0ba8335 -r 7fbeedd05b4c src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Sat Nov 08 09:16:47 2014 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala	Sat Nov 08 09:19:57 2014 +0100
@@ -22,7 +22,7 @@
   /* font rendering information */
 
   val font_family: String = "IsabelleText"
-  val font_size: Int = 32
+  val font_size: Int = 14
   val font = new Font(font_family, Font.BOLD, font_size)
 
   val rendering_hints =
@@ -41,7 +41,7 @@
 
   /* rendering parameters */
 
-  val gap_x = 5
+  val gap_x = 20
   val pad_x = 8
   val pad_y = 5