--- 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;
--- 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
--- /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)
--- /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 \<open>Build Isabelle/Haskell modules\<close>
+
+theory Build imports Haskell
+begin
+
+ML_command \<open>
+ 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
+ )
+\<close>
+
+end
--- /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 \<open>Commands\<close>
+
+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)
+ >> Haskell.generate_file_cmd);
+
+ Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
+ (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
+ >> Haskell.export_file_cmd);
+\<close>
+
+
+section \<open>Source modules\<close>
+
+generate_haskell_file Library.hs = \<open>
+{- 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
+\<close>
+
+generate_haskell_file Buffer.hs = \<open>
+{- 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)
+\<close>
+
+generate_haskell_file Properties.hs = \<open>
+{- 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
+\<close>
+
+generate_haskell_file Markup.hs = \<open>
+{- 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 = ("", "")
+\<close>
+
+generate_haskell_file XML.hs = \<open>
+{- 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
+\<close>
+
+generate_haskell_file YXML.hs = \<open>
+{- 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"
+\<close>
+
+end
--- /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
--- /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 = ("", "")
--- /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
--- /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
--- /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"
--- /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>\<open>~~/src/Tools/Haskell/Library.hs\<close>,
+ \<^file>\<open>~~/src/Tools/Haskell/Buffer.hs\<close>,
+ \<^file>\<open>~~/src/Tools/Haskell/Properties.hs\<close>,
+ \<^file>\<open>~~/src/Tools/Haskell/Markup.hs\<close>,
+ \<^file>\<open>~~/src/Tools/Haskell/XML.hs\<close>,
+ \<^file>\<open>~~/src/Tools/Haskell/YXML.hs\<close>];
+
+end;
--- 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