(* Title: Tools/Haskell/haskell.ml
Author: Makarius
Support for Isabelle tools in Haskell.
*)
signature HASKELL =
sig
val generate_file_cmd: (string * Position.T) * Input.source ->
Toplevel.transition -> Toplevel.transition
val export_file_cmd: string * Input.source ->
Toplevel.transition -> Toplevel.transition
val source_modules: Path.T list
end;
structure Haskell: HASKELL =
struct
(* commands *)
val header = "{- GENERATED by Isabelle! -}\n";
fun generate_file_cmd (file, source) =
Toplevel.keep (fn state =>
let
val ctxt = Toplevel.context_of state;
val thy = Toplevel.theory_of state;
val path = Resources.check_path ctxt (Resources.master_directory thy) file;
val text = header ^ GHC.read_source ctxt source;
val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path));
val _ = File.generate path text;
in () end);
fun export_file_cmd (name, source) =
Toplevel.keep (fn state =>
let
val ctxt = Toplevel.context_of state;
val thy = Toplevel.theory_of state;
val text = header ^ GHC.read_source ctxt source;
val _ = Export.export thy name [text];
in () end);
(* source modules *)
val source_modules =
[\<^file>\<open>~~/src/Tools/Haskell/Library.hs\<close>,
\<^file>\<open>~~/src/Tools/Haskell/Buffer.hs\<close>,
\<^file>\<open>~~/src/Tools/Haskell/Properties.hs\<close>,
\<^file>\<open>~~/src/Tools/Haskell/Markup.hs\<close>,
\<^file>\<open>~~/src/Tools/Haskell/XML.hs\<close>,
\<^file>\<open>~~/src/Tools/Haskell/YXML.hs\<close>];
end;