1.1 --- a/doc-src/antiquote_setup.ML	Tue Oct 19 18:50:48 2010 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Tue Oct 19 19:16:27 2010 +0100
     1.3 @@ -56,6 +56,13 @@
     1.4  
     1.5  fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
     1.6  
     1.7 +val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);
     1.8 +
     1.9 +fun ml_name txt =
    1.10 +  (case filter is_name (ML_Lex.tokenize txt) of
    1.11 +    toks as [_] => ML_Lex.flatten toks
    1.12 +  | _ => error ("Single ML name expected in input: " ^ quote txt));
    1.13 +
    1.14  fun index_ml name kind ml = Thy_Output.antiquotation name
    1.15    (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
    1.16    (fn {context = ctxt, ...} => fn (txt1, txt2) =>
    1.17 @@ -70,7 +77,7 @@
    1.18        val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
    1.19        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.20      in
    1.21 -      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    1.22 +      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
    1.23        (txt'
    1.24        |> (if Config.get ctxt Thy_Output.quotes then quote else I)
    1.25        |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"