more formal Haskell project setup, with dependencies on packages from "stackage";

--- a/lib/scripts/getsettings	Mon Dec 10 22:38:03 2018 +0100
+++ b/lib/scripts/getsettings	Mon Dec 10 23:03:20 2018 +0100
@@ -113,6 +113,7 @@
 if [ -d "$ISABELLE_STACK_ROOT" -a -f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS" ]; then
   if [ -f "$(cat "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS")/$ISABELLE_GHC_VERSION/bin/ghc" ]; then
     ISABELLE_GHC="$ISABELLE_HOME/lib/scripts/ghc"
+    ISABELLE_GHC_STACK=true
   fi
 fi
 

--- a/src/Pure/Tools/ghc.ML	Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Pure/Tools/ghc.ML	Mon Dec 10 23:03:20 2018 +0100
@@ -9,6 +9,8 @@
   val print_codepoint: UTF8.codepoint -> string
   val print_symbol: Symbol.symbol -> string
   val print_string: string -> string
+  val project_template: {depends: string list, modules: string list} -> string
+  val new_project: Path.T -> {name: string, depends: string list, modules: string list} -> unit
 end;
 
 structure GHC: GHC =
@@ -42,4 +44,47 @@
 
 val print_string = quote o implode o map print_symbol o Symbol.explode;
 
+
+(* project setup *)
+
+fun project_template {depends, modules} =
+  Input.source_content_string \<open>{-# START_FILE {{name}}.cabal #-}
+name:                {{name}}
+version:             0.1.0.0
+homepage:            default
+license:             BSD3
+author:              default
+maintainer:          default
+category:            default
+build-type:          Simple
+cabal-version:       >=1.10
+
+executable {{name}}
+  hs-source-dirs:      src
+  main-is:             Main.hs
+  default-language:    Haskell2010
+  build-depends:       \<close> ^ commas ("base >= 4.7 && < 5" :: depends) ^
+  Input.source_content_string \<open>
+  other-modules:       \<close> ^ commas modules ^
+  Input.source_content_string \<open>
+{-# START_FILE Setup.hs #-}
+import Distribution.Simple
+main = defaultMain
+
+{-# START_FILE src/Main.hs #-}
+module Main where
+
+main :: IO ()
+main = return ()
+\<close>;
+
+fun new_project dir {name, depends, modules} =
+  let
+    val template_path = Path.append dir (Path.basic name |> Path.ext "hsfiles");
+    val _ = File.write template_path (project_template {depends = depends, modules = modules});
+    val {rc, err, ...} =
+      Bash.process ("cd " ^ File.bash_path dir ^
+        "; isabelle ghc_stack new " ^ Bash.string name ^ " --bare " ^ File.bash_path template_path);
+  in if rc = 0 then () else error err end;
+
 end;

--- a/src/Tools/Haskell/Haskell.thy	Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Mon Dec 10 23:03:20 2018 +0100
@@ -8,7 +8,7 @@
   imports Pure
 begin
 
-generate_file "Library.hs" = \<open>
+generate_file "Isabelle/Library.hs" = \<open>
 {-  Title:      Tools/Haskell/Library.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -102,7 +102,7 @@
 clean_name = reverse #> dropWhile (== '_') #> reverse
 \<close>
 
-generate_file "Value.hs" = \<open>
+generate_file "Isabelle/Value.hs" = \<open>
 {-  Title:      Haskell/Tools/Value.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -155,7 +155,7 @@
 parse_real = Read.readMaybe
 \<close>
 
-generate_file "Buffer.hs" = \<open>
+generate_file "Isabelle/Buffer.hs" = \<open>
 {-  Title:      Tools/Haskell/Buffer.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -181,7 +181,7 @@
 content (Buffer xs) = concat (reverse xs)
 \<close>
 
-generate_file "Properties.hs" = \<open>
+generate_file "Isabelle/Properties.hs" = \<open>
 {-  Title:      Tools/Haskell/Properties.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -215,7 +215,7 @@
   else props
 \<close>
 
-generate_file "Markup.hs" = \<open>
+generate_file "Isabelle/Markup.hs" = \<open>
 {-  Title:      Haskell/Tools/Markup.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -585,7 +585,7 @@
 no_output = ("", "")
 \<close>
 
-generate_file "Completion.hs" = \<open>
+generate_file "Isabelle/Completion.hs" = \<open>
 {-  Title:      Tools/Haskell/Completion.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -646,7 +646,7 @@
   markup_report [make limit name_props make_names]
 \<close>
 
-generate_file "File.hs" = \<open>
+generate_file "Isabelle/File.hs" = \<open>
 {-  Title:      Tools/Haskell/File.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -681,7 +681,7 @@
   IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s)
 \<close>
 
-generate_file "XML.hs" = \<open>
+generate_file "Isabelle/XML.hs" = \<open>
 {-  Title:      Tools/Haskell/XML.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -760,7 +760,7 @@
       show_text = concatMap encode
 \<close>
 
-generate_file "XML/Encode.hs" = \<open>
+generate_file "Isabelle/XML/Encode.hs" = \<open>
 {-  Title:      Tools/Haskell/XML/Encode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -846,7 +846,7 @@
 variant fs x = [tagged (the (get_index (\f -> f x) fs))]
 \<close>
 
-generate_file "XML/Decode.hs" = \<open>
+generate_file "Isabelle/XML/Decode.hs" = \<open>
 {-  Title:      Tools/Haskell/XML/Decode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -957,7 +957,7 @@
 variant _ _ = err_body
 \<close>
 
-generate_file "YXML.hs" = \<open>
+generate_file "Isabelle/YXML.hs" = \<open>
 {-  Title:      Tools/Haskell/YXML.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -1085,7 +1085,7 @@
     _ -> err "multiple results"
 \<close>
 
-generate_file "Pretty.hs" = \<open>
+generate_file "Isabelle/Pretty.hs" = \<open>
 {-  Title:      Tools/Haskell/Pretty.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -1239,7 +1239,7 @@
 big_list name prts = block (fbreaks (str name : prts))
 \<close>
 
-generate_file "Term.hs" = \<open>
+generate_file "Isabelle/Term.hs" = \<open>
 {-  Title:      Tools/Haskell/Term.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -1286,7 +1286,7 @@
   deriving Show
 \<close>
 
-generate_file "Term_XML/Encode.hs" = \<open>
+generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
 {-  Title:      Tools/Haskell/Term_XML/Encode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
@@ -1328,7 +1328,7 @@
     \case { App a -> Just ([], pair term term a); _ -> Nothing }]
 \<close>
 
-generate_file "Term_XML/Decode.hs" = \<open>
+generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
 {-  Title:      Tools/Haskell/Term_XML/Decode.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)

--- a/src/Tools/Haskell/Test.thy	Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Tools/Haskell/Test.thy	Mon Dec 10 23:03:20 2018 +0100
@@ -8,15 +8,18 @@
 begin
 
 ML \<open>
-  Isabelle_System.with_tmp_dir "ghc" (fn dir =>
+  Isabelle_System.with_tmp_dir "ghc" (fn tmp_dir =>
     let
-      val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> dir;
+      val src_dir = Path.append tmp_dir (Path.explode "src");
+      val files = Generated_Files.write_files \<^theory>\<open>Haskell\<close> src_dir;
+
+      val modules = files
+        |> map (Path.implode #> unsuffix ".hs" #> space_explode "/" #> space_implode ".");
+      val _ = GHC.new_project tmp_dir {name = "isabelle", depends = [], modules = modules};
+
       val (out, rc) =
         Isabelle_System.bash_output
-         (cat_lines
-           ["set -e",
-            "cd " ^ File.bash_path dir,
-            "\"$ISABELLE_GHC\" " ^ File.bash_paths files]);
+          (cat_lines ["set -e", "cd " ^ File.bash_path tmp_dir, "isabelle ghc_stack build 2>&1"]);
     in if rc = 0 then writeln out else error out end)
 \<close>
 

--- a/src/Tools/ROOT	Mon Dec 10 22:38:03 2018 +0100
+++ b/src/Tools/ROOT	Mon Dec 10 23:03:20 2018 +0100
@@ -12,5 +12,5 @@
 session Haskell in Haskell = Pure +
   theories
     Haskell
-  theories [condition = ISABELLE_GHC]
+  theories [condition = ISABELLE_GHC_STACK]
     Test