author | wenzelm |
Wed, 26 Sep 2012 14:52:18 +0200 | |
changeset 49572 | 0d2f81eb7bf4 |
parent 49571 | 7e6fc0254d23 |
child 49573 | 0f087257ba04 |
--- a/src/Tools/Graphview/src/parameters.scala Wed Sep 26 14:50:46 2012 +0200 +++ b/src/Tools/Graphview/src/parameters.scala Wed Sep 26 14:52:18 2012 +0200 @@ -16,11 +16,6 @@ val font_family: String = "IsabelleText" val font_size: Int = 16 - //Should not fail since this is in the isabelle environment. - def tooltip_css(): String = - File.try_read( - Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS"))) - object Colors { val Filter_Colors = List(