--- a/CookBook/antiquote_setup.ML	Tue Sep 16 00:46:29 2008 +0200
+++ b/CookBook/antiquote_setup.ML	Wed Sep 17 19:20:06 2008 -0400
@@ -1,5 +1,5 @@
 (*  Title:      Doc/antiquote_setup.ML
-    ID:         $Id: antiquote_setup.ML,v 1.27 2008/08/09 20:43:46 wenzelm Exp $
+    ID:         $Id: antiquote_setup.ML,v 1.30 2008/09/16 12:39:56 wenzelm Exp $
     Author:     Makarius
 
 Auxiliary antiquotations for the Isabelle manuals.
@@ -143,7 +143,7 @@
       (ThyLoad.check_thy Path.current name; Pretty.str name))))];
 
 
-(* Isar entities (with index) *)
+(* Isabelle entities (with index) *)
 
 local
 
@@ -153,6 +153,9 @@
   let val thy = ProofContext.theory_of ctxt
   in defined thy o intern thy end;
 
+fun check_tool name =
+  File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
+
 val arg = enclose "{" "}" o clean_string;
 
 fun output_entity check markup index kind ctxt (logic, name) =
@@ -174,7 +177,7 @@
         |> (if ! O.quotes then quote else I)
         |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
             else hyper o enclose "\\mbox{\\isa{" "}}"))
-    else error ("Undefined " ^ kind ^ " " ^ quote name)
+    else error ("Bad " ^ kind ^ " " ^ quote name)
   end;
 
 fun entity check markup index kind =
@@ -198,7 +201,11 @@
   entity_antiqs no_check "" "fact" @
   entity_antiqs no_check "" "variable" @
   entity_antiqs no_check "" "case" @
-  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation");
+  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
+  entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
+  entity_antiqs no_check "isatt" "executable" @
+  entity_antiqs (K check_tool) "isatt" "tool" @
+  entity_antiqs (K (File.exists o Path.explode)) "isatt" "file");
 
 end;