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