src/Pure/GUI/gui.scala
Fri, 27 Dec 2024 19:49:45 +0100 wenzelm proper bullet symbols for GUI text -- in contrast to Isabelle \<bullet> 0x002219;
less more (0) -100 -30 -10 -1 tip