src/Tools/Code/code_scala.ML
Fri, 25 Sep 2020 14:37:07 +0200 wenzelm more robust: avoid spurious line breaks that might confuse the scala interpreter;
less more (0) -100 -30 -10 -1 tip