src/Pure/PIDE/markup.scala
Sat, 20 Nov 2021 18:15:09 +0100 wenzelm more symbolic latex_output via XML;
less more (0) -100 -30 -10 -1 tip