src/Pure/PIDE/markup.scala
Sun, 29 Jun 2025 16:16:22 +0200 wenzelm clarified signature: more explicit operations;
less more (0) -100 -30 -10 -1 tip