1.1 --- a/doc-src/antiquote_setup.ML	Tue Sep 16 12:27:05 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Tue Sep 16 14:39:56 2008 +0200
     1.3 @@ -153,6 +153,9 @@
     1.4    let val thy = ProofContext.theory_of ctxt
     1.5    in defined thy o intern thy end;
     1.6  
     1.7 +fun check_tool name =
     1.8 +  File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
     1.9 +
    1.10  val arg = enclose "{" "}" o clean_string;
    1.11  
    1.12  fun output_entity check markup index kind ctxt (logic, name) =
    1.13 @@ -174,7 +177,7 @@
    1.14          |> (if ! O.quotes then quote else I)
    1.15          |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.16              else hyper o enclose "\\mbox{\\isa{" "}}"))
    1.17 -    else error ("Undefined " ^ kind ^ " " ^ quote name)
    1.18 +    else error ("Bad " ^ kind ^ " " ^ quote name)
    1.19    end;
    1.20  
    1.21  fun entity check markup index kind =
    1.22 @@ -199,9 +202,10 @@
    1.23    entity_antiqs no_check "" "variable" @
    1.24    entity_antiqs no_check "" "case" @
    1.25    entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
    1.26 -  entity_antiqs no_check "isatt" "setting" @
    1.27 +  entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
    1.28    entity_antiqs no_check "isatt" "executable" @
    1.29 -  entity_antiqs no_check "isatt" "tool");
    1.30 +  entity_antiqs (K check_tool) "isatt" "tool" @
    1.31 +  entity_antiqs (K (File.exists o Path.explode)) "isatt" "file");
    1.32  
    1.33  end;
    1.34