src/Tools/Haskell/haskell.ML

more Haskell operations;
tuned;

(*  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 sources: Path.T list
  val install_sources: Path.T -> unit
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);


(* sources *)

val sources =
 [\<^path>\<open>Library.hs\<close>,
  \<^path>\<open>Value.hs\<close>,
  \<^path>\<open>Buffer.hs\<close>,
  \<^path>\<open>Properties.hs\<close>,
  \<^path>\<open>Markup.hs\<close>,
  \<^path>\<open>XML.hs\<close>,
  \<^path>\<open>XML/Encode.hs\<close>,
  \<^path>\<open>XML/Decode.hs\<close>,
  \<^path>\<open>YXML.hs\<close>,
  \<^path>\<open>Term.hs\<close>,
  \<^path>\<open>Term_XML/Encode.hs\<close>,
  \<^path>\<open>Term_XML/Decode.hs\<close>];

val master_dir = Resources.master_directory \<^theory>;

fun install_sources dir =
  sources |> List.app (fn path => Isabelle_System.copy_file_base (master_dir, path) dir);

end;