# HG changeset patch # User wenzelm # Date 1541273096 -3600 # Node ID 043cbeb0b1cf4d792fcfc978cc9a59ba2f242e22 # Parent 21ee588bac7d0fc37c49e351fd851eb94c7974e0# Parent f4263f7ec9a44909bb715ea77c59e32c83707538 merged diff -r 21ee588bac7d -r 043cbeb0b1cf src/Pure/General/file.ML --- a/src/Pure/General/file.ML Thu Nov 01 18:19:33 2018 +0000 +++ b/src/Pure/General/file.ML Sat Nov 03 20:24:56 2018 +0100 @@ -9,6 +9,7 @@ val standard_path: Path.T -> string val platform_path: Path.T -> string val bash_path: Path.T -> string + val bash_paths: Path.T list -> string val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T val exists: Path.T -> bool @@ -29,6 +30,7 @@ val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit + val generate: Path.T -> string -> unit val output: BinIO.outstream -> string -> unit val write_list: Path.T -> string list -> unit val append_list: Path.T -> string list -> unit @@ -45,7 +47,7 @@ val platform_path = ML_System.platform_path o standard_path; val bash_path = Bash_Syntax.string o standard_path; - +val bash_paths = Bash_Syntax.strings o map standard_path; (* full_path *) @@ -154,6 +156,7 @@ fun write path txt = write_list path [txt]; fun append path txt = append_list path [txt]; +fun generate path txt = if try read path = SOME txt then () else write path txt; fun write_buffer path buf = open_output (Buffer.output buf) path; diff -r 21ee588bac7d -r 043cbeb0b1cf src/Pure/PIDE/xml.ML --- a/src/Pure/PIDE/xml.ML Thu Nov 01 18:19:33 2018 +0000 +++ b/src/Pure/PIDE/xml.ML Sat Nov 03 20:24:56 2018 +0100 @@ -93,7 +93,7 @@ | unwrap_elem _ = NONE; -(* text context *) +(* text content *) fun add_content tree = (case unwrap_elem tree of diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/Buffer.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Buffer.hs Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,23 @@ +{- generated by Isabelle -} + +{- Title: Tools/Haskell/Buffer.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Efficient text buffers. +-} + +module Isabelle.Buffer (T, empty, add, content) +where + +newtype T = Buffer [String] + +empty :: T +empty = Buffer [] + +add :: String -> T -> T +add "" buf = buf +add x (Buffer xs) = Buffer (x : xs) + +content :: T -> String +content (Buffer xs) = concat (reverse xs) diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/Build.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Build.thy Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,24 @@ +(* Title: Tools/Haskell/Build.thy + Author: Makarius +*) + +section \Build Isabelle/Haskell modules\ + +theory Build imports Haskell +begin + +ML_command \ + Isabelle_System.with_tmp_dir "ghc" (fn dir => + let + val (out, rc) = + Isabelle_System.bash_output + (cat_lines + ["set -e", + "cd " ^ File.bash_path dir, + "cp " ^ File.bash_paths Haskell.source_modules ^ " .", + "\"$ISABELLE_GHC\" " ^ File.bash_paths (map Path.base Haskell.source_modules)]); + in if rc = 0 then writeln out else error out end + ) +\ + +end diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/Haskell.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Haskell.thy Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,372 @@ +(* Title: Tools/Haskell/Haskell.thy + Author: Makarius + +Support for Isabelle tools in Haskell. +*) + +theory Haskell + imports Pure + keywords "generate_haskell_file" "export_haskell_file" :: thy_decl +begin + +ML_file "haskell.ML" + + +section \Commands\ + +ML \ + Outer_Syntax.command \<^command_keyword>\generate_haskell_file\ "generate Haskell file" + (Parse.position Parse.path -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) + >> Haskell.generate_file_cmd); + + Outer_Syntax.command \<^command_keyword>\export_haskell_file\ "export Haskell file" + (Parse.name -- (\<^keyword>\=\ |-- Parse.input Parse.embedded) + >> Haskell.export_file_cmd); +\ + + +section \Source modules\ + +generate_haskell_file Library.hs = \ +{- Title: Tools/Haskell/Library.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Basic library of Isabelle idioms. +-} + +module Isabelle.Library + ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line) +where + +{- functions -} + +(|>) :: a -> (a -> b) -> b +x |> f = f x + +(|->) :: (a, b) -> (a -> b -> c) -> c +(x, y) |-> f = f x y + +(#>) :: (a -> b) -> (b -> c) -> a -> c +(f #> g) x = x |> f |> g + +(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d +(f #-> g) x = x |> f |-> g + + +{- lists -} + +fold :: (a -> b -> b) -> [a] -> b -> b +fold _ [] y = y +fold f (x : xs) y = fold f xs (f x y) + +fold_rev :: (a -> b -> b) -> [a] -> b -> b +fold_rev _ [] y = y +fold_rev f (x : xs) y = f x (fold_rev f xs y) + +single :: a -> [a] +single x = [x] + + +{- strings -} + +quote :: String -> String +quote s = "\"" ++ s ++ "\"" + +trim_line :: String -> String +trim_line line = + case reverse line of + '\n' : '\r' : rest -> reverse rest + '\n' : rest -> reverse rest + _ -> line +\ + +generate_haskell_file Buffer.hs = \ +{- Title: Tools/Haskell/Buffer.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Efficient text buffers. +-} + +module Isabelle.Buffer (T, empty, add, content) +where + +newtype T = Buffer [String] + +empty :: T +empty = Buffer [] + +add :: String -> T -> T +add "" buf = buf +add x (Buffer xs) = Buffer (x : xs) + +content :: T -> String +content (Buffer xs) = concat (reverse xs) +\ + +generate_haskell_file Properties.hs = \ +{- Title: Tools/Haskell/Properties.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Property lists. +-} + +module Isabelle.Properties (Entry, T, defined, get, put, remove) +where + +import qualified Data.List as List + + +type Entry = (String, String) +type T = [Entry] + +defined :: T -> String -> Bool +defined props name = any (\(a, _) -> a == name) props + +get :: T -> String -> Maybe String +get props name = List.lookup name props + +put :: Entry -> T -> T +put entry props = entry : remove (fst entry) props + +remove :: String -> T -> T +remove name props = + if defined props name then filter (\(a, _) -> a /= name) props + else props +\ + +generate_haskell_file Markup.hs = \ +{- Title: Haskell/Tools/Markup.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Quasi-abstract markup elements. +-} + +module Isabelle.Markup (T, empty, is_empty, Output, no_output) +where + +import qualified Isabelle.Properties as Properties + + +type T = (String, Properties.T) + +empty :: T +empty = ("", []) + +is_empty :: T -> Bool +is_empty ("", _) = True +is_empty _ = False + + +type Output = (String, String) + +no_output :: Output +no_output = ("", "") +\ + +generate_haskell_file XML.hs = \ +{- Title: Tools/Haskell/XML.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Untyped XML trees and representation of ML values. +-} + +module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of) +where + +import qualified Data.List as List + +import Isabelle.Library +import qualified Isabelle.Properties as Properties +import qualified Isabelle.Markup as Markup +import qualified Isabelle.Buffer as Buffer + + +{- types -} + +type Attributes = Properties.T +type Body = [Tree] +data Tree = Elem Markup.T Body | Text String + + +{- wrapped elements -} + +xml_elemN = "xml_elem"; +xml_nameN = "xml_name"; +xml_bodyN = "xml_body"; + +wrap_elem (((a, atts), body1), body2) = + Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2) + +unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) = + if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts' + then Just (((a, atts), body1), body2) else Nothing +unwrap_elem _ = Nothing + + +{- text content -} + +add_content tree = + case unwrap_elem tree of + Just (_, ts) -> fold add_content ts + Nothing -> + case tree of + Elem _ ts -> fold add_content ts + Text s -> Buffer.add s + +content_of body = Buffer.empty |> fold add_content body |> Buffer.content + + +{- string representation -} + +encode '<' = "<" +encode '>' = ">" +encode '&' = "&" +encode '\'' = "'" +encode '\"' = """ +encode c = [c] + +instance Show Tree where + show tree = + Buffer.empty |> show_tree tree |> Buffer.content + where + show_tree (Elem (name, atts) []) = + Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>" + show_tree (Elem (name, atts) ts) = + Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #> + fold show_tree ts #> + Buffer.add " Buffer.add name #> Buffer.add ">" + show_tree (Text s) = Buffer.add (show_text s) + + show_elem name atts = + unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts) + + show_text = concatMap encode +\ + +generate_haskell_file YXML.hs = \ +{- Title: Tools/Haskell/YXML.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Efficient text representation of XML trees. Suitable for direct +inlining into plain text. +-} + +module Isabelle.YXML (charX, charY, strX, strY, detect, + buffer_body, buffer, string_of_body, string_of, parse_body, parse) +where + +import qualified Data.Char as Char +import qualified Data.List as List + +import Isabelle.Library +import qualified Isabelle.Markup as Markup +import qualified Isabelle.XML as XML +import qualified Isabelle.Buffer as Buffer + + +{- markers -} + +charX, charY :: Char +charX = Char.chr 5 +charY = Char.chr 6 + +strX, strY, strXY, strXYX :: String +strX = [charX] +strY = [charY] +strXY = strX ++ strY +strXYX = strXY ++ strX + +detect :: String -> Bool +detect = any (\c -> c == charX || c == charY) + + +{- output -} + +buffer_attrib (a, x) = + Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x + +buffer_body :: XML.Body -> Buffer.T -> Buffer.T +buffer_body = fold buffer + +buffer :: XML.Tree -> Buffer.T -> Buffer.T +buffer (XML.Elem (name, atts) ts) = + Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #> + buffer_body ts #> + Buffer.add strXYX +buffer (XML.Text s) = Buffer.add s + +string_of_body :: XML.Body -> String +string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content + +string_of :: XML.Tree -> String +string_of = string_of_body . single + + +{- parse -} + +-- split: fields or non-empty tokens + +split :: Bool -> Char -> String -> [String] +split _ _ [] = [] +split fields sep str = splitting str + where + splitting rest = + case span (/= sep) rest of + (_, []) -> cons rest [] + (prfx, _ : rest') -> cons prfx (splitting rest') + cons item = if fields || not (null item) then (:) item else id + + +-- structural errors + +err msg = error ("Malformed YXML: " ++ msg) +err_attribute = err "bad attribute" +err_element = err "bad element" +err_unbalanced "" = err "unbalanced element" +err_unbalanced name = err ("unbalanced element " ++ quote name) + + +-- stack operations + +add x ((elem, body) : pending) = (elem, x : body) : pending + +push "" _ _ = err_element +push name atts pending = ((name, atts), []) : pending + +pop ((("", _), _) : _) = err_unbalanced "" +pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending + + +-- parsing + +parse_attrib s = + case List.elemIndex '=' s of + Just i | i > 0 -> (take i s, drop (i + 1) s) + _ -> err_attribute + +parse_chunk ["", ""] = pop +parse_chunk ("" : name : atts) = push name (map parse_attrib atts) +parse_chunk txts = fold (add . XML.Text) txts + +parse_body :: String -> XML.Body +parse_body source = + case fold parse_chunk chunks [(("", []), [])] of + [(("", _), result)] -> reverse result + ((name, _), _) : _ -> err_unbalanced name + where chunks = split False charX source |> map (split True charY) + +parse :: String -> XML.Tree +parse source = + case parse_body source of + [result] -> result + [] -> XML.Text "" + _ -> err "multiple results" +\ + +end diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/Library.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Library.hs Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,53 @@ +{- generated by Isabelle -} + +{- Title: Tools/Haskell/Library.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Basic library of Isabelle idioms. +-} + +module Isabelle.Library + ((|>), (|->), (#>), (#->), fold, fold_rev, single, quote, trim_line) +where + +{- functions -} + +(|>) :: a -> (a -> b) -> b +x |> f = f x + +(|->) :: (a, b) -> (a -> b -> c) -> c +(x, y) |-> f = f x y + +(#>) :: (a -> b) -> (b -> c) -> a -> c +(f #> g) x = x |> f |> g + +(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d +(f #-> g) x = x |> f |-> g + + +{- lists -} + +fold :: (a -> b -> b) -> [a] -> b -> b +fold _ [] y = y +fold f (x : xs) y = fold f xs (f x y) + +fold_rev :: (a -> b -> b) -> [a] -> b -> b +fold_rev _ [] y = y +fold_rev f (x : xs) y = f x (fold_rev f xs y) + +single :: a -> [a] +single x = [x] + + +{- strings -} + +quote :: String -> String +quote s = "\"" ++ s ++ "\"" + +trim_line :: String -> String +trim_line line = + case reverse line of + '\n' : '\r' : rest -> reverse rest + '\n' : rest -> reverse rest + _ -> line diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/Markup.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Markup.hs Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,29 @@ +{- generated by Isabelle -} + +{- Title: Haskell/Tools/Markup.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Quasi-abstract markup elements. +-} + +module Isabelle.Markup (T, empty, is_empty, Output, no_output) +where + +import qualified Isabelle.Properties as Properties + + +type T = (String, Properties.T) + +empty :: T +empty = ("", []) + +is_empty :: T -> Bool +is_empty ("", _) = True +is_empty _ = False + + +type Output = (String, String) + +no_output :: Output +no_output = ("", "") diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/Properties.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/Properties.hs Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,31 @@ +{- generated by Isabelle -} + +{- Title: Tools/Haskell/Properties.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Property lists. +-} + +module Isabelle.Properties (Entry, T, defined, get, put, remove) +where + +import qualified Data.List as List + + +type Entry = (String, String) +type T = [Entry] + +defined :: T -> String -> Bool +defined props name = any (\(a, _) -> a == name) props + +get :: T -> String -> Maybe String +get props name = List.lookup name props + +put :: Entry -> T -> T +put entry props = entry : remove (fst entry) props + +remove :: String -> T -> T +remove name props = + if defined props name then filter (\(a, _) -> a /= name) props + else props diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/XML.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/XML.hs Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,80 @@ +{- generated by Isabelle -} + +{- Title: Tools/Haskell/XML.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Untyped XML trees and representation of ML values. +-} + +module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of) +where + +import qualified Data.List as List + +import Isabelle.Library +import qualified Isabelle.Properties as Properties +import qualified Isabelle.Markup as Markup +import qualified Isabelle.Buffer as Buffer + + +{- types -} + +type Attributes = Properties.T +type Body = [Tree] +data Tree = Elem Markup.T Body | Text String + + +{- wrapped elements -} + +xml_elemN = "xml_elem"; +xml_nameN = "xml_name"; +xml_bodyN = "xml_body"; + +wrap_elem (((a, atts), body1), body2) = + Elem (xml_elemN, (xml_nameN, a) : atts) (Elem (xml_bodyN, []) body1 : body2) + +unwrap_elem (Elem (name, (n, a) : atts) (Elem (name', atts') body1 : body2)) = + if name == xml_elemN && n == xml_nameN && name' == xml_bodyN && null atts' + then Just (((a, atts), body1), body2) else Nothing +unwrap_elem _ = Nothing + + +{- text content -} + +add_content tree = + case unwrap_elem tree of + Just (_, ts) -> fold add_content ts + Nothing -> + case tree of + Elem _ ts -> fold add_content ts + Text s -> Buffer.add s + +content_of body = Buffer.empty |> fold add_content body |> Buffer.content + + +{- string representation -} + +encode '<' = "<" +encode '>' = ">" +encode '&' = "&" +encode '\'' = "'" +encode '\"' = """ +encode c = [c] + +instance Show Tree where + show tree = + Buffer.empty |> show_tree tree |> Buffer.content + where + show_tree (Elem (name, atts) []) = + Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>" + show_tree (Elem (name, atts) ts) = + Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #> + fold show_tree ts #> + Buffer.add " Buffer.add name #> Buffer.add ">" + show_tree (Text s) = Buffer.add (show_text s) + + show_elem name atts = + unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts) + + show_text = concatMap encode diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/YXML.hs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/YXML.hs Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,120 @@ +{- generated by Isabelle -} + +{- Title: Tools/Haskell/YXML.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Efficient text representation of XML trees. Suitable for direct +inlining into plain text. +-} + +module Isabelle.YXML (charX, charY, strX, strY, detect, + buffer_body, buffer, string_of_body, string_of, parse_body, parse) +where + +import qualified Data.Char as Char +import qualified Data.List as List + +import Isabelle.Library +import qualified Isabelle.Markup as Markup +import qualified Isabelle.XML as XML +import qualified Isabelle.Buffer as Buffer + + +{- markers -} + +charX, charY :: Char +charX = Char.chr 5 +charY = Char.chr 6 + +strX, strY, strXY, strXYX :: String +strX = [charX] +strY = [charY] +strXY = strX ++ strY +strXYX = strXY ++ strX + +detect :: String -> Bool +detect = any (\c -> c == charX || c == charY) + + +{- output -} + +buffer_attrib (a, x) = + Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x + +buffer_body :: XML.Body -> Buffer.T -> Buffer.T +buffer_body = fold buffer + +buffer :: XML.Tree -> Buffer.T -> Buffer.T +buffer (XML.Elem (name, atts) ts) = + Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #> + buffer_body ts #> + Buffer.add strXYX +buffer (XML.Text s) = Buffer.add s + +string_of_body :: XML.Body -> String +string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content + +string_of :: XML.Tree -> String +string_of = string_of_body . single + + +{- parse -} + +-- split: fields or non-empty tokens + +split :: Bool -> Char -> String -> [String] +split _ _ [] = [] +split fields sep str = splitting str + where + splitting rest = + case span (/= sep) rest of + (_, []) -> cons rest [] + (prfx, _ : rest') -> cons prfx (splitting rest') + cons item = if fields || not (null item) then (:) item else id + + +-- structural errors + +err msg = error ("Malformed YXML: " ++ msg) +err_attribute = err "bad attribute" +err_element = err "bad element" +err_unbalanced "" = err "unbalanced element" +err_unbalanced name = err ("unbalanced element " ++ quote name) + + +-- stack operations + +add x ((elem, body) : pending) = (elem, x : body) : pending + +push "" _ _ = err_element +push name atts pending = ((name, atts), []) : pending + +pop ((("", _), _) : _) = err_unbalanced "" +pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending + + +-- parsing + +parse_attrib s = + case List.elemIndex '=' s of + Just i | i > 0 -> (take i s, drop (i + 1) s) + _ -> err_attribute + +parse_chunk ["", ""] = pop +parse_chunk ("" : name : atts) = push name (map parse_attrib atts) +parse_chunk txts = fold (add . XML.Text) txts + +parse_body :: String -> XML.Body +parse_body source = + case fold parse_chunk chunks [(("", []), [])] of + [(("", _), result)] -> reverse result + ((name, _), _) : _ -> err_unbalanced name + where chunks = split False charX source |> map (split True charY) + +parse :: String -> XML.Tree +parse source = + case parse_body source of + [result] -> result + [] -> XML.Text "" + _ -> err "multiple results" diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/Haskell/haskell.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Haskell/haskell.ML Sat Nov 03 20:24:56 2018 +0100 @@ -0,0 +1,56 @@ +(* 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>\~~/src/Tools/Haskell/Library.hs\, + \<^file>\~~/src/Tools/Haskell/Buffer.hs\, + \<^file>\~~/src/Tools/Haskell/Properties.hs\, + \<^file>\~~/src/Tools/Haskell/Markup.hs\, + \<^file>\~~/src/Tools/Haskell/XML.hs\, + \<^file>\~~/src/Tools/Haskell/YXML.hs\]; + +end; diff -r 21ee588bac7d -r 043cbeb0b1cf src/Tools/ROOT --- a/src/Tools/ROOT Thu Nov 01 18:19:33 2018 +0000 +++ b/src/Tools/ROOT Sat Nov 03 20:24:56 2018 +0100 @@ -8,3 +8,9 @@ session SML in SML = Pure + theories Examples + +session Haskell in Haskell = Pure + + theories + Haskell + theories [condition = ISABELLE_GHC] + Build