1 /* Title: Pure/GUI/color_value.scala
2 Module: PIDE-GUI
3 Author: Makarius
2 Author: Makarius
4
3
5 Cached color values.
4 Cached color values.
6 */
5 */
7
6