CookBook/antiquote_setup_plus.ML
author berghofe
Fri, 10 Oct 2008 17:06:26 +0200
changeset 25 e2f9f94b26d4
parent 15 9da9ba2b095b
child 26 2311f81d7a22
permissions -rw-r--r--
Antiquotation setup is now contained in theory Base.

(*
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