src/Tools/Haskell/haskell.ML

tuned message (e.g. see Options.save_prefs);

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