# HG changeset patch # User wenzelm # Date 1668373159 -3600 # Node ID b67c9ed2c810b90d8989794a1b32cea735d6cd69 # Parent ca88e5496553816754f9aba2e07d85802e65f31b tuned output; diff -r ca88e5496553 -r b67c9ed2c810 src/Pure/Tools/prismjs.ML --- a/src/Pure/Tools/prismjs.ML Sun Nov 13 21:31:45 2022 +0100 +++ b/src/Pure/Tools/prismjs.ML Sun Nov 13 21:59:19 2022 +0100 @@ -50,6 +50,8 @@ end; +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o language_name); + (* tokenize *)