--- a/CookBook/antiquote_setup.ML Wed Sep 17 19:20:37 2008 -0400
+++ b/CookBook/antiquote_setup.ML Tue Sep 30 03:30:40 2008 -0400
@@ -1,5 +1,5 @@
(* Title: Doc/antiquote_setup.ML
- ID: $Id: antiquote_setup.ML,v 1.30 2008/09/16 12:39:56 wenzelm Exp $
+ ID: $Id: antiquote_setup.ML,v 1.32 2008/09/29 10:31:56 haftmann Exp $
Author: Makarius
Auxiliary antiquotations for the Isabelle manuals.
@@ -75,7 +75,7 @@
else txt1 ^ ": " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
val _ = writeln (ml (txt1, txt2));
- val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
+ val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
in
"\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
((if ! O.source then str_of_source src else txt')
@@ -205,7 +205,8 @@
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");
+ entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @
+ entity_antiqs (K ThyInfo.known_thy) "" "theory");
end;