# HG changeset patch # User wenzelm # Date 1541076809 -3600 # Node ID 8365124a86ae6b108b70a11766a86bd5d16a0548 # Parent d4cec24a1d87d97fa18de436ad42ba016e9dec7e support for Isabelle tool development in Haskell; diff -r d4cec24a1d87 -r 8365124a86ae src/Tools/Haskell/Haskell.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Haskell.thy Thu Nov 01 13:53:29 2018 +0100 @@ -0,0 +1,42 @@ +(* Title: Tools/Haskell/Haskell.thy + Author: Makarius +*) + +section \Support for Isabelle tool development in Haskell\ + +theory Haskell + imports Pure + keywords "generate_haskell_file" "export_haskell_file" :: thy_decl +begin + +ML \ + Outer_Syntax.command \<^command_keyword>\generate_haskell_file\ "generate Haskell file" + (Parse.position Parse.path -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) >> + (fn (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 = GHC.read_source ctxt source; + val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path)); + val _ = if try File.read path = SOME text then () else File.write path text; + in () end))); +\ + +ML \ + Outer_Syntax.command \<^command_keyword>\export_haskell_file\ "export Haskell file" + (Parse.name -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) >> + (fn (name, source) => + Toplevel.keep (fn state => + let + val ctxt = Toplevel.context_of state; + val thy = Toplevel.theory_of state; + + val text = GHC.read_source ctxt source; + val _ = Export.export thy name [text]; + in () end))); +\ + +end diff -r d4cec24a1d87 -r 8365124a86ae src/Tools/ROOT --- a/src/Tools/ROOT Thu Nov 01 12:23:54 2018 +0100 +++ b/src/Tools/ROOT Thu Nov 01 13:53:29 2018 +0100 @@ -8,3 +8,7 @@ session SML in SML = Pure + theories Examples + +session Haskell in Haskell = Pure + + theories + Haskell