scala-ide/scala-ide — pull request #757 by sschaef (2014-07-31 13:38:37+00:00)
Title: Hover improvements2

Improved version of the hovers. Addresses all issues discussed in #750 and improves the style of the hovers in some areas. Most important change to the previous PR is that a preference page exists in `Scala→Editor→Hovers`, that allows users to edit the CSS code.