diff --git a/src/Pure/Tools/prismjs.ML b/src/Pure/Tools/prismjs.ML
--- a/src/Pure/Tools/prismjs.ML
+++ b/src/Pure/Tools/prismjs.ML
@@ -1,79 +1,81 @@
 (*  Title:      Pure/Tools/prismjs.ML
     Author:     Makarius
 
 Support for the Prism.js syntax highlighter -- via Isabelle/Scala.
 *)
 
 signature PRISMJS =
 sig
   type language
   val languages: unit -> language list
   val language_names: language -> string list
   val language_name: language -> string
   val language_alias: language -> string list
   val check_language: Proof.context -> string * Position.T -> string
   datatype token = Token of string list * content
   and content = Atom of string | Nested of token list
   val decode_token: token XML.Decode.T
   val decode_content: content XML.Decode.T
   val token_types: token -> string list
   val token_content: token -> content
   val token_string: token -> string
   val content_string: content -> string
   val tokenize: {text: string, language: string} -> token list
 end;
 
 structure Prismjs: PRISMJS =
 struct
 
 (* languages *)
 
 abstype language = Language of string list
 with
 
 fun language_names (Language names) = names;
 val language_name = hd o language_names;
 val language_alias = tl o language_names;
 
 fun languages () =
   \<^scala>\<open>Prismjs.languages\<close> []
   |> map (split_lines #> Language);
 
 fun check_language ctxt arg =
   let
     val langs = languages () |> maps language_names |> sort_strings |> map (rpair ());
     val name =
       Completion.check_item Markup.prismjs_languageN
         (fn (name, _) => Markup.entity Markup.prismjs_languageN name)
         langs ctxt arg;
   in name end;
 
 end;
 
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o language_name);
+
 
 (* tokenize *)
 
 datatype token = Token of string list * content
 and content = Atom of string | Nested of token list;
 
 local open XML.Decode in
 
 fun decode_token body = body |> pair (list string) decode_content |> Token
 and decode_content body =
   body |> variant
    [fn ([a], []) => Atom a,
     fn ([], a) => Nested (list decode_token a)]
 
 end;
 
 fun token_types (Token (types, _)) = types;
 fun token_content (Token (_, content)) = content;
 fun token_string tok = content_string (token_content tok)
 and content_string (Atom string) = string
   | content_string (Nested tokens) = implode (map token_string tokens);
 
 fun tokenize {text, language} =
   \<^scala>\<open>Prismjs.tokenize\<close> [text, language]
   |> map (YXML.parse_body #> decode_token);
 
 end;