src/Tools/Haskell/haskell.ML
author wenzelm
Sat Nov 10 19:39:38 2018 +0100 (11 months ago ago)
changeset 69287 94fa3376ba33
parent 69253 9f21381600e3
child 69294 4c3704ecb0e6
permissions -rw-r--r--
added ML antiquotation @{master_dir};
     1 (*  Title:      Tools/Haskell/haskell.ml
     2     Author:     Makarius
     3 
     4 Support for Isabelle tools in Haskell.
     5 *)
     6 
     7 signature HASKELL =
     8 sig
     9   val generate_file_cmd: (string * Position.T) * Input.source ->
    10     Toplevel.transition -> Toplevel.transition
    11   val export_file_cmd: string * Input.source ->
    12     Toplevel.transition -> Toplevel.transition
    13   val sources: Path.T list
    14   val install_sources: Path.T -> unit
    15 end;
    16 
    17 structure Haskell: HASKELL =
    18 struct
    19 
    20 (* commands *)
    21 
    22 val header = "{- generated by Isabelle -}\n";
    23 
    24 fun generate_file_cmd (file, source) =
    25   Toplevel.keep (fn state =>
    26     let
    27       val ctxt = Toplevel.context_of state;
    28       val thy = Toplevel.theory_of state;
    29 
    30       val path = Resources.check_path ctxt (Resources.master_directory thy) file;
    31       val text = header ^ GHC.read_source ctxt source;
    32       val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path));
    33       val _ = File.generate path text;
    34     in () end);
    35 
    36 fun export_file_cmd (name, source) =
    37   Toplevel.keep (fn state =>
    38     let
    39       val ctxt = Toplevel.context_of state;
    40       val thy = Toplevel.theory_of state;
    41 
    42       val text = header ^ GHC.read_source ctxt source;
    43       val _ = Export.export thy name [text];
    44     in () end);
    45 
    46 
    47 (* sources *)
    48 
    49 val sources =
    50  [\<^path>\<open>Library.hs\<close>,
    51   \<^path>\<open>Value.hs\<close>,
    52   \<^path>\<open>Buffer.hs\<close>,
    53   \<^path>\<open>Properties.hs\<close>,
    54   \<^path>\<open>Markup.hs\<close>,
    55   \<^path>\<open>XML.hs\<close>,
    56   \<^path>\<open>XML/Encode.hs\<close>,
    57   \<^path>\<open>XML/Decode.hs\<close>,
    58   \<^path>\<open>YXML.hs\<close>,
    59   \<^path>\<open>Pretty.hs\<close>,
    60   \<^path>\<open>Term.hs\<close>,
    61   \<^path>\<open>Term_XML/Encode.hs\<close>,
    62   \<^path>\<open>Term_XML/Decode.hs\<close>];
    63 
    64 fun install_sources dir =
    65   sources |> List.app (fn path => Isabelle_System.copy_file_base (\<^master_dir>, path) dir);
    66 
    67 end;