src/Pure/ML/ml_process.scala
Sat, 14 Jun 2025 14:31:54 +0200 wenzelm clarified signature;
Mon, 01 Jul 2024 12:40:54 +0200 wenzelm clarified signature: more explicit XML.Body types, more uniform Symbol.encode_yxml;
Sat, 01 Jun 2024 12:35:38 +0200 wenzelm unused;
less more (0) -30 -10 -3 tip