author | wenzelm |
Tue, 06 Nov 2018 14:53:56 +0100 | |
changeset 69248 | 9f21381600e3 |
parent 69240 | 16ca270090b6 |
child 69282 | 94fa3376ba33 |
permissions | -rw-r--r-- |
69225 | 1 |
(* Title: Tools/Haskell/haskell.ml |
2 |
Author: Makarius |
|
3 |
||
4 |
Support for Isabelle tools in Haskell. |
|
5 |
*) |
|
6 |
||
7 |
signature HASKELL = |
|
8 |
sig |
|
9 |
val generate_file_cmd: (string * Position.T) * Input.source -> |
|
10 |
Toplevel.transition -> Toplevel.transition |
|
11 |
val export_file_cmd: string * Input.source -> |
|
12 |
Toplevel.transition -> Toplevel.transition |
|
69239
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
13 |
val sources: Path.T list |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
14 |
val install_sources: Path.T -> unit |
69225 | 15 |
end; |
16 |
||
17 |
structure Haskell: HASKELL = |
|
18 |
struct |
|
19 |
||
20 |
(* commands *) |
|
21 |
||
69227 | 22 |
val header = "{- generated by Isabelle -}\n"; |
69225 | 23 |
|
24 |
fun generate_file_cmd (file, source) = |
|
25 |
Toplevel.keep (fn state => |
|
26 |
let |
|
27 |
val ctxt = Toplevel.context_of state; |
|
28 |
val thy = Toplevel.theory_of state; |
|
29 |
||
30 |
val path = Resources.check_path ctxt (Resources.master_directory thy) file; |
|
31 |
val text = header ^ GHC.read_source ctxt source; |
|
32 |
val _ = Isabelle_System.mkdirs (Path.dir (Path.expand path)); |
|
33 |
val _ = File.generate path text; |
|
34 |
in () end); |
|
35 |
||
36 |
fun export_file_cmd (name, source) = |
|
37 |
Toplevel.keep (fn state => |
|
38 |
let |
|
39 |
val ctxt = Toplevel.context_of state; |
|
40 |
val thy = Toplevel.theory_of state; |
|
41 |
||
42 |
val text = header ^ GHC.read_source ctxt source; |
|
43 |
val _ = Export.export thy name [text]; |
|
44 |
in () end); |
|
45 |
||
46 |
||
69239
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
47 |
(* sources *) |
69225 | 48 |
|
69239
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
49 |
val sources = |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
50 |
[\<^path>\<open>Library.hs\<close>, |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
51 |
\<^path>\<open>Value.hs\<close>, |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
52 |
\<^path>\<open>Buffer.hs\<close>, |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
53 |
\<^path>\<open>Properties.hs\<close>, |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
54 |
\<^path>\<open>Markup.hs\<close>, |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
55 |
\<^path>\<open>XML.hs\<close>, |
69240 | 56 |
\<^path>\<open>XML/Encode.hs\<close>, |
57 |
\<^path>\<open>XML/Decode.hs\<close>, |
|
58 |
\<^path>\<open>YXML.hs\<close>, |
|
69248 | 59 |
\<^path>\<open>Pretty.hs\<close>, |
69240 | 60 |
\<^path>\<open>Term.hs\<close>, |
61 |
\<^path>\<open>Term_XML/Encode.hs\<close>, |
|
62 |
\<^path>\<open>Term_XML/Decode.hs\<close>]; |
|
69239
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
63 |
|
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
64 |
val master_dir = Resources.master_directory \<^theory>; |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
65 |
|
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
66 |
fun install_sources dir = |
6cd985a78d6e
support sub-directories, i.e. structure module names;
wenzelm
parents:
69233
diff
changeset
|
67 |
sources |> List.app (fn path => Isabelle_System.copy_file_base (master_dir, path) dir); |
69225 | 68 |
|
69 |
end; |