# 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 \<open>Support for Isabelle tool development in Haskell\<close>
+
+theory Haskell
+  imports Pure
+  keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
+begin
+
+ML \<open>
+  Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
+    (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- 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)));
+\<close>
+
+ML \<open>
+  Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
+    (Parse.name -- (\<^keyword>\<open>=\<close> |-- 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)));
+\<close>
+
+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