1.1 --- a/doc-src/antiquote_setup.ML	Wed May 14 20:30:53 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Wed May 14 20:31:17 2008 +0200
     1.3 @@ -138,42 +138,50 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun no_check _ _ = true;
     1.8 +
     1.9 +fun thy_check intern defined ctxt =
    1.10 +  let val thy = ProofContext.theory_of ctxt
    1.11 +  in defined thy o intern thy end;
    1.12 +
    1.13  val arg = enclose "{" "}" o clean_string;
    1.14  
    1.15 -fun output_entity markup index kind ctxt (logic, name) =
    1.16 -  (case index of
    1.17 -    NONE => ""
    1.18 -  | SOME is_def =>
    1.19 -      "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    1.20 -  ^
    1.21 -  (Output.output name
    1.22 -    |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.23 -    |> (if ! O.quotes then quote else I)
    1.24 -    |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.25 -        else enclose "\\mbox{\\isa{" "}}"));
    1.26 +fun output_entity check markup index kind ctxt (logic, name) =
    1.27 +  if check ctxt name then
    1.28 +    (case index of
    1.29 +      NONE => ""
    1.30 +    | SOME is_def =>
    1.31 +        "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    1.32 +    ^
    1.33 +    (Output.output name
    1.34 +      |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")                                    
    1.35 +      |> (if ! O.quotes then quote else I)
    1.36 +      |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.37 +          else enclose "\\mbox{\\isa{" "}}"))
    1.38 +  else error ("Undefined " ^ kind ^ " " ^ quote name);
    1.39  
    1.40 -fun entity markup index kind =
    1.41 +fun entity check markup index kind =
    1.42    O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    1.43 -    (K (output_entity markup index kind));
    1.44 +    (K (output_entity check markup index kind));
    1.45      
    1.46 -fun entity_antiqs markup kind =
    1.47 - [(kind, entity markup NONE kind),
    1.48 -  (kind ^ "_def", entity markup (SOME true) kind), 
    1.49 -  (kind ^ "_ref", entity markup (SOME false) kind)];
    1.50 +fun entity_antiqs check markup kind =
    1.51 + [(kind, entity check markup NONE kind),
    1.52 +  (kind ^ "_def", entity check markup (SOME true) kind), 
    1.53 +  (kind ^ "_ref", entity check markup (SOME false) kind)];
    1.54  
    1.55  in
    1.56  
    1.57  val _ = O.add_commands
    1.58 - (entity_antiqs "" "syntax" @
    1.59 -  entity_antiqs "isacommand" "command" @
    1.60 -  entity_antiqs "isakeyword" "keyword" @
    1.61 -  entity_antiqs "isakeyword" "element" @
    1.62 -  entity_antiqs "" "method" @
    1.63 -  entity_antiqs "" "attribute" @
    1.64 -  entity_antiqs "" "fact" @
    1.65 -  entity_antiqs "" "variable" @
    1.66 -  entity_antiqs "" "case" @
    1.67 -  entity_antiqs "" "antiquotation");
    1.68 + (entity_antiqs no_check "" "syntax" @
    1.69 +  entity_antiqs (K (is_some o OuterSyntax.command_keyword)) "isacommand" "command" @
    1.70 +  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "keyword" @
    1.71 +  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "element" @
    1.72 +  entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
    1.73 +  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
    1.74 +  entity_antiqs no_check "" "fact" @
    1.75 +  entity_antiqs no_check "" "variable" @
    1.76 +  entity_antiqs no_check "" "case" @
    1.77 +  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation");
    1.78  
    1.79  end;
    1.80