doc-src/antiquote_setup.ML

 fun no_check _ _ = true;
 
 fun thy_check intern defined ctxt =
   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) =
   let

       (Output.output name
         |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
         |> (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 =
   O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
     (K (output_entity check markup index kind));

   entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
   entity_antiqs no_check "" "fact" @
   entity_antiqs no_check "" "variable" @
   entity_antiqs no_check "" "case" @
   entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
-  entity_antiqs no_check "isatt" "setting" @
+  entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
   entity_antiqs no_check "isatt" "executable" @
-  entity_antiqs no_check "isatt" "tool");
-
-end;
-
-end;
+  entity_antiqs (K check_tool) "isatt" "tool" @
+  entity_antiqs (K (File.exists o Path.explode)) "isatt" "file");
+
+end;
+
+end;