1.1 --- a/doc-src/antiquote_setup.ML	Mon Mar 09 21:12:14 2009 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Mar 09 21:23:40 2009 +0100
     1.3 @@ -132,7 +132,8 @@
     1.4  
     1.5  fun entity check markup kind index =
     1.6    ThyOutput.antiquotation
     1.7 -    (case index of NONE => kind | SOME true => kind ^ "_def" | SOME false => kind ^ "_ref")
     1.8 +    (translate (fn " " => "_" | c => c) kind ^
     1.9 +      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
    1.10      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    1.11      (fn {context = ctxt, ...} => fn (logic, name) =>
    1.12        let
    1.13 @@ -174,6 +175,7 @@
    1.14  val _ = entity_antiqs no_check "" "variable";
    1.15  val _ = entity_antiqs no_check "" "case";
    1.16  val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
    1.17 +val _ = entity_antiqs (K ThyOutput.defined_option) "" "antiquotation option";
    1.18  val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
    1.19  val _ = entity_antiqs no_check "" "inference";
    1.20  val _ = entity_antiqs no_check "isatt" "executable";