reverted commit accident from 994fe0ba8335
authorhaftmann
Sat, 08 Nov 2014 09:19:57 +0100
changeset 58940 7fbeedd05b4c
parent 58939 994fe0ba8335
child 58941 f09dd46352ba
reverted commit accident from 994fe0ba8335
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