CookBook/antiquote_setup_plus.ML
changeset 15 9da9ba2b095b
child 26 2311f81d7a22
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/antiquote_setup_plus.ML	Thu Oct 02 04:48:41 2008 -0400
@@ -0,0 +1,16 @@
+(*
+Auxiliary antiquotations for the Cookbook.
+
+*)
+
+local structure O = ThyOutput
+in
+  fun check_exists f = 
+    if File.exists (Path.explode ("~~/src/" ^ f)) then ()
+    else error ("Source file " ^ quote f ^ " does not exist.")
+  
+  val _ = O.add_commands
+   [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
+         (check_exists name; Pretty.str name))))];
+
+end
\ No newline at end of file