src/Pure/GUI/gui.scala
changeset 71360 fcf5ee85743d
parent 71357 7f2cd237ee4f
child 71361 21a41356d78f
equal deleted inserted replaced
71359:411c0322c09d 71360:fcf5ee85743d
   254       "CheckBoxMenuItem.font",
   254       "CheckBoxMenuItem.font",
   255       "Label.font",
   255       "Label.font",
   256       "Menu.font",
   256       "Menu.font",
   257       "MenuItem.font",
   257       "MenuItem.font",
   258       "PopupMenu.font",
   258       "PopupMenu.font",
       
   259       "Table.font",
       
   260       "TableHeader.font",
   259       "TextArea.font",
   261       "TextArea.font",
   260       "TextField.font",
   262       "TextField.font",
   261       "TextPane.font",
   263       "TextPane.font",
   262       "Tooltip.font",
   264       "Tooltip.font",
   263       "Tree.font"))
   265       "Tree.font"))