1.1 --- a/doc-src/antiquote_setup.ML Wed May 07 13:04:12 2008 +0200
1.2 +++ b/doc-src/antiquote_setup.ML Wed May 07 13:05:13 2008 +0200
1.3 @@ -140,13 +140,13 @@
1.4
1.5 val arg = enclose "{" "}" o clean_string;
1.6
1.7 -fun output_entity markup index kind src ctxt (logic, name) =
1.8 +fun output_entity markup index kind ctxt (logic, name) =
1.9 (case index of
1.10 NONE => ""
1.11 | SOME is_def =>
1.12 "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
1.13 ^
1.14 - (Output.output (if ! O.source then str_of_source src else name)
1.15 + (Output.output name
1.16 |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
1.17 |> (if ! O.quotes then quote else I)
1.18 |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.19 @@ -154,7 +154,7 @@
1.20
1.21 fun entity markup index kind =
1.22 O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
1.23 - (output_entity markup index kind);
1.24 + (K (output_entity markup index kind));
1.25
1.26 fun entity_antiqs markup kind =
1.27 [(kind, entity markup NONE kind),