src/Pure/PIDE/markup.scala
Fri, 20 Sep 2024 15:35:16 +0200 wenzelm block markup for specific notation, notably infix and binder;
less more (0) -100 -30 -10 -1 tip