author | wenzelm |
Thu, 21 Jul 2022 15:01:48 +0200 | |
changeset 75685 | 07cd3b243c69 |
parent 75683 | 7ca63aea3c6c |
child 75686 | 42f19e398ee4 |
permissions | -rw-r--r-- |
69383 | 1 |
(* Title: Pure/Tools/generated_files.ML |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
3 |
|
69383 | 4 |
Generated source files for other languages: with antiquotations, without Isabelle symbols. |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
5 |
*) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
6 |
|
69383 | 7 |
signature GENERATED_FILES = |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
8 |
sig |
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
9 |
val add_files: Path.binding * Bytes.T -> theory -> theory |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
10 |
type file = {path: Path.T, pos: Position.T, content: Bytes.T} |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
11 |
val file_binding: file -> Path.binding |
70051 | 12 |
val file_markup: file -> Markup.T |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
13 |
val print_file: file -> string |
70051 | 14 |
val report_file: Proof.context -> Position.T -> file -> unit |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
15 |
val get_files: theory -> file list |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
16 |
val get_file: theory -> Path.binding -> file |
70051 | 17 |
val get_files_in: Path.binding list * theory -> (file * Position.T) list |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
18 |
val check_files_in: Proof.context -> |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
19 |
(string * Position.T) list * (string * Position.T) option -> Path.binding list * theory |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
20 |
val write_file: Path.T -> file -> unit |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
21 |
val export_file: theory -> file -> unit |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
22 |
type file_type = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
23 |
{name: string, ext: string, make_comment: string -> string, make_string: string -> string} |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
24 |
val file_type: |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
25 |
binding -> {ext: string, make_comment: string -> string, make_string: string -> string} -> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
26 |
theory -> theory |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
27 |
val antiquotation: binding -> 'a Token.context_parser -> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
28 |
({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) -> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
29 |
theory -> theory |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
30 |
val set_string: string -> Proof.context -> Proof.context |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
31 |
val generate_file: Path.binding * Input.source -> Proof.context -> local_theory |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
32 |
val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
33 |
val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
34 |
val export_generated_files_cmd: Proof.context -> |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
35 |
((string * Position.T) list * (string * Position.T) option) list -> unit |
75685 | 36 |
val check_external_files: Proof.context -> |
37 |
Input.source list * Input.source -> Path.T list * Path.T |
|
38 |
val get_external_files: Path.T -> Path.T list * Path.T -> unit |
|
70051 | 39 |
val with_compile_dir: (Path.T -> unit) -> unit |
70054
a884b2967dd7
clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents:
70053
diff
changeset
|
40 |
val compile_generated_files: Proof.context -> |
a884b2967dd7
clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents:
70053
diff
changeset
|
41 |
(Path.binding list * theory) list -> |
a884b2967dd7
clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents:
70053
diff
changeset
|
42 |
(Path.T list * Path.T) list -> |
a884b2967dd7
clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents:
70053
diff
changeset
|
43 |
(Path.binding list * bool option) list -> |
a884b2967dd7
clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents:
70053
diff
changeset
|
44 |
Path.binding -> Input.source -> unit |
70051 | 45 |
val compile_generated_files_cmd: Proof.context -> |
46 |
((string * Position.T) list * (string * Position.T) option) list -> |
|
72841 | 47 |
(Input.source list * Input.source) list -> |
70054
a884b2967dd7
clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
wenzelm
parents:
70053
diff
changeset
|
48 |
((string * Position.T) list * bool option) list -> |
70051 | 49 |
string * Position.T -> Input.source -> unit |
70067
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
50 |
val execute: Path.T -> Input.source -> string -> string |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
51 |
end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
52 |
|
69383 | 53 |
structure Generated_Files: GENERATED_FILES = |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
54 |
struct |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
55 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
56 |
(** context data **) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
57 |
|
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
58 |
type file = Path.T * (Position.T * Bytes.T); |
72050 | 59 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
60 |
type file_type = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
61 |
{name: string, ext: string, make_comment: string -> string, make_string: string -> string}; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
62 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
63 |
type antiquotation = Token.src -> Proof.context -> file_type -> string; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
64 |
|
72046
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
65 |
fun err_dup_files path pos pos' = |
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
66 |
error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']); |
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
67 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
68 |
structure Data = Theory_Data |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
69 |
( |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
70 |
type T = |
72050 | 71 |
file list Symtab.table * (*files for named theory*) |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
72 |
file_type Name_Space.table * (*file types*) |
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
73 |
antiquotation Name_Space.table; (*antiquotations*) |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
74 |
val empty = |
72050 | 75 |
(Symtab.empty, |
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
76 |
Name_Space.empty_table Markup.file_typeN, |
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
77 |
Name_Space.empty_table Markup.antiquotationN); |
72046
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
78 |
fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) = |
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
79 |
let |
72050 | 80 |
val files' = |
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
81 |
(files1, files2) |> Symtab.join (fn _ => |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
82 |
Library.merge (fn ((path1, (pos1, bytes1)), (path2, (pos2, bytes2))) => |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
83 |
if path1 <> path2 then false |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
84 |
else if pos1 = pos2 andalso Bytes.eq (bytes1, bytes2) then true |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
85 |
else err_dup_files path1 pos1 pos2)); |
72046
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
86 |
val types' = Name_Space.merge_tables (types1, types2); |
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
87 |
val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2); |
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
88 |
in (files', types', antiqs') end; |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
89 |
); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
90 |
|
72050 | 91 |
fun lookup_files thy = |
92 |
Symtab.lookup_list (#1 (Data.get thy)) (Context.theory_long_name thy); |
|
93 |
||
94 |
fun update_files thy_files' thy = |
|
95 |
(Data.map o @{apply 3(1)}) (Symtab.update (Context.theory_long_name thy, thy_files')) thy; |
|
96 |
||
97 |
fun add_files (binding, content) thy = |
|
70055
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70054
diff
changeset
|
98 |
let |
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70054
diff
changeset
|
99 |
val _ = Path.proper_binding binding; |
36fb663145e5
type Path.binding may be empty: check later via proper_binding;
wenzelm
parents:
70054
diff
changeset
|
100 |
val (path, pos) = Path.dest_binding binding; |
72050 | 101 |
val thy_files = lookup_files thy; |
102 |
val thy_files' = |
|
103 |
(case AList.lookup (op =) thy_files path of |
|
72046
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
104 |
SOME (pos', _) => err_dup_files path pos pos' |
72050 | 105 |
| NONE => (path, (pos, content)) :: thy_files); |
106 |
in update_files thy_files' thy end; |
|
72046
c386d1b77762
more thorough extend/merge (for Theory.join_theory);
wenzelm
parents:
70991
diff
changeset
|
107 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
108 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
109 |
(* get files *) |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
110 |
|
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
111 |
type file = {path: Path.T, pos: Position.T, content: Bytes.T}; |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
112 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
113 |
fun file_binding (file: file) = Path.binding (#path file, #pos file); |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
114 |
|
70051 | 115 |
fun file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file)); |
116 |
||
117 |
fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file))); |
|
118 |
||
119 |
fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file); |
|
120 |
||
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
121 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
122 |
fun get_files thy = |
72050 | 123 |
lookup_files thy |> rev |> map (fn (path, (pos, content)) => |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
124 |
{path = path, pos = pos, content = content}: file); |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
125 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
126 |
fun get_file thy binding = |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
127 |
let val (path, pos) = Path.dest_binding binding in |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
128 |
(case find_first (fn file => #path file = path) (get_files thy) of |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
129 |
SOME file => file |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
130 |
| NONE => |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
131 |
error ("Missing generated file " ^ Path.print path ^ |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
132 |
" in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos)) |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
133 |
end; |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
134 |
|
70051 | 135 |
fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy) |
136 |
| get_files_in (files, thy) = |
|
137 |
map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files; |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
138 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
139 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
140 |
(* check and output files *) |
69628 | 141 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
142 |
fun check_files_in ctxt (files, opt_thy) = |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
143 |
let |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
144 |
val thy = |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
145 |
(case opt_thy of |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
146 |
SOME name => Theory.check {long = false} ctxt name |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
147 |
| NONE => Proof_Context.theory_of ctxt); |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
148 |
in (map Path.explode_binding files, thy) end; |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
149 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
150 |
fun write_file dir (file: file) = |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
151 |
let |
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72375
diff
changeset
|
152 |
val path = Path.expand (dir + #path file); |
72375 | 153 |
val _ = Isabelle_System.make_directory (Path.dir path); |
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
154 |
val content = #content file; |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
155 |
val write_content = |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
156 |
(case try Bytes.read path of |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
157 |
SOME old_content => not (Bytes.eq (content, old_content)) |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
158 |
| NONE => true) |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
159 |
in if write_content then Bytes.write path content else () end; |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
160 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
161 |
fun export_file thy (file: file) = |
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
162 |
Export.export thy (file_binding file) (Bytes.contents_blob (#content file)); |
70013 | 163 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
164 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
165 |
(* file types *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
166 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
167 |
fun get_file_type thy ext = |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
168 |
if ext = "" then error "Bad file extension" |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
169 |
else |
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
170 |
(#2 (Data.get thy), NONE) |-> Name_Space.fold_table |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
171 |
(fn (_, file_type) => fn res => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
172 |
if #ext file_type = ext then SOME file_type else res) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
173 |
|> (fn SOME file_type => file_type |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
174 |
| NONE => error ("Unknown file type for extension " ^ quote ext)); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
175 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
176 |
fun file_type binding {ext, make_comment, make_string} thy = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
177 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
178 |
val name = Binding.name_of binding; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
179 |
val pos = Binding.pos_of binding; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
180 |
val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string}; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
181 |
|
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
182 |
val table = #2 (Data.get thy); |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
183 |
val space = Name_Space.space_of_table table; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
184 |
val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
185 |
val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
186 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
187 |
val _ = |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
188 |
(case try (#name o get_file_type thy) ext of |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
189 |
NONE => () |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
190 |
| SOME name' => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
191 |
error ("Extension " ^ quote ext ^ " already registered for file type " ^ |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
192 |
quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos)); |
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
193 |
in thy |> (Data.map o @{apply 3(2)}) (K data') end; |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
194 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
195 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
196 |
(* antiquotations *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
197 |
|
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
198 |
val get_antiquotations = #3 o Data.get o Proof_Context.theory_of; |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
199 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
200 |
fun antiquotation name scan body thy = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
201 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
202 |
fun ant src ctxt file_type : string = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
203 |
let val (x, ctxt') = Token.syntax scan src ctxt |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
204 |
in body {context = ctxt', source = src, file_type = file_type, argument = x} end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
205 |
in |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
206 |
thy |
69385
be9f187dcd50
clarified signature: allow to add_files/get_files by other tools;
wenzelm
parents:
69383
diff
changeset
|
207 |
|> (Data.map o @{apply 3(3)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2) |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
208 |
end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
209 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
210 |
val scan_antiq = |
74373
6e4093927dbb
outer syntax: support for control-cartouche tokens;
wenzelm
parents:
74147
diff
changeset
|
211 |
Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control || |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
212 |
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
213 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
214 |
fun read_source ctxt (file_type: file_type) source = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
215 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
216 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
217 |
Context_Position.report ctxt (Input.pos_of source) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
218 |
(Markup.language |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
219 |
{name = #name file_type, symbols = false, antiquotes = true, |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
220 |
delimited = Input.is_delimited source}); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
221 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
222 |
val (input, _) = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
223 |
Input.source_explode source |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
224 |
|> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq)); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
225 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
226 |
val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
227 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
228 |
fun expand antiq = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
229 |
(case antiq of |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
230 |
Antiquote.Text s => s |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
231 |
| Antiquote.Control {name, body, ...} => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
232 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
233 |
val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
234 |
val (src', ant) = Token.check_src ctxt get_antiquotations src; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
235 |
in ant src' ctxt file_type end |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
236 |
| Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq)))); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
237 |
in implode (map expand input) end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
238 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
239 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
240 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
241 |
(** Isar commands **) |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
242 |
|
70051 | 243 |
(* generate_file *) |
244 |
||
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
245 |
fun generate_file (binding, source) lthy = |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
246 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
247 |
val thy = Proof_Context.theory_of lthy; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
248 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
249 |
val (path, pos) = Path.dest_binding binding; |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
250 |
val file_type = |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
251 |
get_file_type thy (#2 (Path.split_ext path)) |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
252 |
handle ERROR msg => error (msg ^ Position.here pos); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
253 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
254 |
val header = #make_comment file_type " generated by Isabelle "; |
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
255 |
val content = Bytes.string (header ^ "\n" ^ read_source lthy file_type source); |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
70013
diff
changeset
|
256 |
in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end; |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
257 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
258 |
fun generate_file_cmd (file, source) lthy = |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
259 |
generate_file (Path.explode_binding file, source) lthy; |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
260 |
|
70051 | 261 |
|
262 |
(* export_generated_files *) |
|
263 |
||
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
264 |
fun export_generated_files ctxt args = |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
265 |
let val thy = Proof_Context.theory_of ctxt in |
70051 | 266 |
(case map #1 (maps get_files_in args) of |
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
267 |
[] => () |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
268 |
| files => |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
269 |
(List.app (export_file thy) files; |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
270 |
writeln (Export.message thy Path.current); |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
271 |
writeln (cat_lines (map (prefix " " o print_file) files)))) |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
272 |
end; |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
273 |
|
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
274 |
fun export_generated_files_cmd ctxt args = |
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
275 |
export_generated_files ctxt (map (check_files_in ctxt) args); |
70051 | 276 |
|
277 |
||
75685 | 278 |
(* external files *) |
279 |
||
280 |
fun check_external_files ctxt (raw_files, raw_base_dir) = |
|
281 |
let |
|
282 |
val base_dir = Resources.check_dir ctxt NONE raw_base_dir; |
|
283 |
fun check source = |
|
284 |
(Resources.check_file ctxt (SOME base_dir) source; |
|
285 |
Path.explode (Input.string_of source)); |
|
286 |
val files = map check raw_files; |
|
287 |
in (files, base_dir) end; |
|
288 |
||
289 |
fun get_external_files dir (files, base_dir) = |
|
290 |
files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir); |
|
291 |
||
292 |
||
70051 | 293 |
(* compile_generated_files *) |
294 |
||
295 |
val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K ""); |
|
296 |
||
297 |
fun with_compile_dir body : unit = |
|
298 |
body (Path.explode (Config.get (Context.the_local_context ()) compile_dir)); |
|
299 |
||
300 |
fun compile_generated_files ctxt args external export export_prefix source = |
|
301 |
Isabelle_System.with_tmp_dir "compile" (fn dir => |
|
302 |
let |
|
303 |
val thy = Proof_Context.theory_of ctxt; |
|
304 |
||
305 |
val files = maps get_files_in args; |
|
306 |
val _ = List.app (fn (file, pos) => report_file ctxt pos file) files; |
|
307 |
val _ = List.app (write_file dir o #1) files; |
|
75685 | 308 |
val _ = List.app (get_external_files dir) external; |
70051 | 309 |
val _ = |
310 |
ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt)) |
|
311 |
ML_Compiler.flags (Input.pos_of source) |
|
312 |
(ML_Lex.read "Generated_Files.with_compile_dir (" @ |
|
313 |
ML_Lex.read_source source @ ML_Lex.read ")"); |
|
314 |
val _ = |
|
315 |
export |> List.app (fn (bindings, executable) => |
|
70053 | 316 |
bindings |> List.app (fn binding0 => |
70051 | 317 |
let |
70053 | 318 |
val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe); |
319 |
val (path, pos) = Path.dest_binding binding; |
|
70051 | 320 |
val content = |
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
321 |
(case try Bytes.read (dir + path) of |
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
322 |
SOME bytes => Bytes.contents_blob bytes |
70051 | 323 |
| NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos)); |
324 |
val _ = Export.report_export thy export_prefix; |
|
325 |
val binding' = |
|
326 |
Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding; |
|
327 |
in |
|
328 |
(if is_some executable then Export.export_executable else Export.export) |
|
75604
39df30349778
more scalable generated files and code export, using Bytes.T;
wenzelm
parents:
74561
diff
changeset
|
329 |
thy binding' content |
70051 | 330 |
end)); |
331 |
val _ = |
|
332 |
if null export then () |
|
333 |
else writeln (Export.message thy (Path.path_of_binding export_prefix)); |
|
334 |
in () end); |
|
335 |
||
336 |
fun compile_generated_files_cmd ctxt args external export export_prefix source = |
|
337 |
compile_generated_files ctxt |
|
338 |
(map (check_files_in ctxt) args) |
|
75685 | 339 |
(map (check_external_files ctxt) external) |
70051 | 340 |
((map o apfst o map) Path.explode_binding export) |
341 |
(Path.explode_binding export_prefix) |
|
342 |
source; |
|
343 |
||
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
344 |
|
70067
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
345 |
(* execute compiler -- auxiliary *) |
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
346 |
|
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
347 |
fun execute dir title compile = |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
348 |
Isabelle_System.bash_process (Bash.script compile |> Bash.cwd dir) |
73279 | 349 |
|> Process_Result.check |
350 |
|> Process_Result.out |
|
70067
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
351 |
handle ERROR msg => |
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
352 |
let val (s, pos) = Input.source_content title |
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
353 |
in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end; |
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
354 |
|
9b34dbeb1103
auxiliary operation for common uses of 'compile_generated_files';
wenzelm
parents:
70055
diff
changeset
|
355 |
|
70047
96fe857a7a6f
clarified signature: more explicit operations for corresponding Isar commands;
wenzelm
parents:
70015
diff
changeset
|
356 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
357 |
(** concrete file types **) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
358 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
359 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
360 |
Theory.setup |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
361 |
(file_type \<^binding>\<open>Haskell\<close> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
362 |
{ext = "hs", |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
363 |
make_comment = enclose "{-" "-}", |
75683 | 364 |
make_string = GHC.print_string} #> |
365 |
file_type \<^binding>\<open>Java\<close> |
|
366 |
{ext = "java", |
|
367 |
make_comment = enclose "/*" "*/", |
|
368 |
make_string = Java.print_string} #> |
|
369 |
file_type \<^binding>\<open>Scala\<close> |
|
370 |
{ext = "scala", |
|
371 |
make_comment = enclose "/*" "*/", |
|
372 |
make_string = Java.print_string}); |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
373 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
374 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
375 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
376 |
(** concrete antiquotations **) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
377 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
378 |
(* ML expression as string literal *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
379 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
380 |
structure Local_Data = Proof_Data |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
381 |
( |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
382 |
type T = string option; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
383 |
fun init _ = NONE; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
384 |
); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
385 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
386 |
val set_string = Local_Data.put o SOME; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
387 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
388 |
fun the_string ctxt = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
389 |
(case Local_Data.get ctxt of |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
390 |
SOME s => s |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
391 |
| NONE => raise Fail "No result string"); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
392 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
393 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
394 |
Theory.setup |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
395 |
(antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
396 |
(fn {context = ctxt, file_type, argument, ...} => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
397 |
ctxt |> Context.proof_map |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
398 |
(ML_Context.expression (Input.pos_of argument) |
69383 | 399 |
(ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @ |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
400 |
ML_Lex.read_source argument @ ML_Lex.read "))")) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
401 |
|> the_string |> #make_string file_type)); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
402 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
403 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
404 |
(* file-system paths *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
405 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
406 |
fun path_antiquotation binding check = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
407 |
antiquotation binding |
72841 | 408 |
(Args.context -- Scan.lift Parse.path_input >> |
409 |
(fn (ctxt, source) => (check ctxt (SOME Path.current) source |> Path.implode))) |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
410 |
(fn {file_type, argument, ...} => #make_string file_type argument); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
411 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
412 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
413 |
Theory.setup |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
414 |
(path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
415 |
path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
416 |
path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
417 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
418 |
end; |