tuned output;
authorwenzelm
Sun, 13 Nov 2022 21:59:19 +0100
changeset 76517 b67c9ed2c810
parent 76516 ca88e5496553
child 76518 b30b8e23383c
tuned output;
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 *)