diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/antiquote_setup_plus.ML --- /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