1.1 --- a/doc-src/antiquote_setup.ML	Mon Apr 28 14:41:32 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Apr 28 14:42:13 2008 +0200
     1.3 @@ -135,39 +135,40 @@
     1.4  
     1.5  val arg = enclose "{" "}" o clean_string;
     1.6  
     1.7 -fun output_entity index kind src ctxt (logic, name) =
     1.8 +fun output_entity markup index kind src 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 +    |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.16      |> (if ! O.quotes then quote else I)
    1.17      |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.18          else enclose "\\isa{" "}"));
    1.19  
    1.20 -fun entity index kind =
    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 index kind);
    1.24 +    (output_entity markup index kind);
    1.25      
    1.26 -fun entity_antiqs kind =
    1.27 - [(kind, entity NONE kind),
    1.28 -  (kind ^ "_def", entity (SOME true) kind), 
    1.29 -  (kind ^ "_ref", entity (SOME false) kind)];
    1.30 +fun entity_antiqs markup kind =
    1.31 + [(kind, entity markup NONE kind),
    1.32 +  (kind ^ "_def", entity markup (SOME true) kind), 
    1.33 +  (kind ^ "_ref", entity markup (SOME false) kind)];
    1.34  
    1.35  in
    1.36  
    1.37  val _ = O.add_commands
    1.38 - (entity_antiqs "syntax" @
    1.39 -  entity_antiqs "command" @
    1.40 -  entity_antiqs "keyword" @
    1.41 -  entity_antiqs "element" @
    1.42 -  entity_antiqs "method" @
    1.43 -  entity_antiqs "attribute" @
    1.44 -  entity_antiqs "fact" @
    1.45 -  entity_antiqs "term" @
    1.46 -  entity_antiqs "case" @
    1.47 -  entity_antiqs "antiquotation");
    1.48 + (entity_antiqs "" "syntax" @
    1.49 +  entity_antiqs "isacommand" "command" @
    1.50 +  entity_antiqs "isakeyword" "keyword" @
    1.51 +  entity_antiqs "" "element" @
    1.52 +  entity_antiqs "" "method" @
    1.53 +  entity_antiqs "" "attribute" @
    1.54 +  entity_antiqs "" "fact" @
    1.55 +  entity_antiqs "" "variable" @
    1.56 +  entity_antiqs "" "case" @
    1.57 +  entity_antiqs "" "antiquotation");
    1.58  
    1.59  end;
    1.60