src/Pure/GUI/color_value.scala
changeset 64370 865b39487b5d
parent 62570 f4c96158a3b8
child 70083 96776eb41854
equal deleted inserted replaced
64369:6a9816764b37 64370:865b39487b5d
     1 /*  Title:      Pure/GUI/color_value.scala
     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