author | wenzelm |
Sat, 01 Dec 2018 16:11:59 +0100 | |
changeset 69383 | 747f8b052e59 |
parent 69381 | src/Pure/Tools/generate_file.ML@4c9b4e2c5460 |
child 69385 | be9f187dcd50 |
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 |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
9 |
type file_type = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
10 |
{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
|
11 |
val file_type: |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
12 |
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
|
13 |
theory -> theory |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
14 |
val antiquotation: binding -> 'a Token.context_parser -> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
15 |
({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
|
16 |
theory -> theory |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
17 |
val set_string: string -> Proof.context -> Proof.context |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
18 |
val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory |
69383 | 19 |
val write: theory -> Path.T -> Path.T list |
20 |
val export: theory -> string -> Path.T list |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
21 |
end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
22 |
|
69383 | 23 |
structure Generated_Files: GENERATED_FILES = |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
24 |
struct |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
25 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
26 |
(** context data **) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
27 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
28 |
type file_type = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
29 |
{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
|
30 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
31 |
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
|
32 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
33 |
structure Data = Theory_Data |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
34 |
( |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
35 |
type T = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
36 |
file_type Name_Space.table * (*file types*) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
37 |
antiquotation Name_Space.table * (*antiquotations*) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
38 |
(Path.T * (Position.T * string)) list; (*generated files for current theory*) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
39 |
val empty = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
40 |
(Name_Space.empty_table Markup.file_typeN, |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
41 |
Name_Space.empty_table Markup.antiquotationN, |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
42 |
[]); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
43 |
val extend = @{apply 3(3)} (K []); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
44 |
fun merge ((types1, antiqs1, _), (types2, antiqs2, _)) = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
45 |
(Name_Space.merge_tables (types1, types2), |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
46 |
Name_Space.merge_tables (antiqs1, antiqs2), |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
47 |
[]); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
48 |
); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
49 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
50 |
val get_files = rev o #3 o Data.get; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
51 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
52 |
fun add_files (path, (pos, text)) = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
53 |
(Data.map o @{apply 3(3)}) (fn files => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
54 |
(case AList.lookup (op =) files path of |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
55 |
SOME (pos', _) => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
56 |
error ("Duplicate generated file " ^ Path.print path ^ Position.here_list [pos, pos']) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
57 |
| NONE => (path, (pos, text)) :: files)); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
58 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
59 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
60 |
(* file types *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
61 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
62 |
fun the_file_type thy ext = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
63 |
if ext = "" then error "Bad file extension" |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
64 |
else |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
65 |
(#1 (Data.get thy), NONE) |-> Name_Space.fold_table |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
66 |
(fn (_, file_type) => fn res => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
67 |
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
|
68 |
|> (fn SOME file_type => file_type |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
69 |
| 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
|
70 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
71 |
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
|
72 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
73 |
val name = Binding.name_of binding; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
74 |
val pos = Binding.pos_of binding; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
75 |
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
|
76 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
77 |
val table = #1 (Data.get thy); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
78 |
val space = Name_Space.space_of_table table; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
79 |
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
|
80 |
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
|
81 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
82 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
83 |
(case try (#name o the_file_type thy) ext of |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
84 |
NONE => () |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
85 |
| SOME name' => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
86 |
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
|
87 |
quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos)); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
88 |
in thy |> (Data.map o @{apply 3(1)}) (K data') end; |
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 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
91 |
(* antiquotations *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
92 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
93 |
val get_antiquotations = #2 o Data.get o Proof_Context.theory_of; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
94 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
95 |
fun antiquotation name scan body thy = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
96 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
97 |
fun ant src ctxt file_type : string = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
98 |
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
|
99 |
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
|
100 |
in |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
101 |
thy |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
102 |
|> (Data.map o @{apply 3(2)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
103 |
end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
104 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
105 |
val scan_antiq = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
106 |
Antiquote.scan_control >> Antiquote.Control || |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
107 |
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
|
108 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
109 |
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
|
110 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
111 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
112 |
Context_Position.report ctxt (Input.pos_of source) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
113 |
(Markup.language |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
114 |
{name = #name file_type, symbols = false, antiquotes = true, |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
115 |
delimited = Input.is_delimited source}); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
116 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
117 |
val (input, _) = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
118 |
Input.source_explode source |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
119 |
|> 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
|
120 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
121 |
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
|
122 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
123 |
fun expand antiq = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
124 |
(case antiq of |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
125 |
Antiquote.Text s => s |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
126 |
| Antiquote.Control {name, body, ...} => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
127 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
128 |
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
|
129 |
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
|
130 |
in ant src' ctxt file_type end |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
131 |
| 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
|
132 |
in implode (map expand input) end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
133 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
134 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
135 |
(* generate files *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
136 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
137 |
fun generate_file_cmd ((file, pos), source) lthy = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
138 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
139 |
val thy = Proof_Context.theory_of lthy; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
140 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
141 |
val path = Path.expand (Path.explode file); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
142 |
fun err_path msg = error (msg ^ ": " ^ Path.print path ^ Position.here pos); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
143 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
144 |
if Path.is_absolute path then err_path "Illegal absolute path" |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
145 |
else if Path.has_parent path then err_path "Illegal parent path" |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
146 |
else (); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
147 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
148 |
val file_type = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
149 |
the_file_type thy (#2 (Path.split_ext path)) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
150 |
handle ERROR msg => error (msg ^ Position.here pos); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
151 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
152 |
val header = #make_comment file_type " generated by Isabelle "; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
153 |
val text = header ^ "\n" ^ read_source lthy file_type source; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
154 |
in lthy |> (Local_Theory.background_theory o add_files) (path, (pos, text)) end; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
155 |
|
69383 | 156 |
fun write thy dir = |
157 |
get_files thy |> map (fn (path, (_, text)) => |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
158 |
let |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
159 |
val path' = Path.expand (Path.append dir path); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
160 |
val _ = Isabelle_System.mkdirs (Path.dir path'); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
161 |
val _ = File.generate path' text; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
162 |
in path end); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
163 |
|
69383 | 164 |
fun export thy prefix = |
165 |
get_files thy |> map (fn (path, (_, text)) => |
|
166 |
let |
|
167 |
val name = (if prefix = "" then "" else prefix ^ "/") ^ Path.implode path; |
|
168 |
val _ = Export.export thy name [text]; |
|
169 |
in path end); |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
170 |
|
69383 | 171 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
172 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
173 |
(** concrete file types **) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
174 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
175 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
176 |
Theory.setup |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
177 |
(file_type \<^binding>\<open>Haskell\<close> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
178 |
{ext = "hs", |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
179 |
make_comment = enclose "{-" "-}", |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
180 |
make_string = GHC.print_string}); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
181 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
182 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
183 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
184 |
(** concrete antiquotations **) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
185 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
186 |
(* ML expression as string literal *) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
187 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
188 |
structure Local_Data = Proof_Data |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
189 |
( |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
190 |
type T = string option; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
191 |
fun init _ = NONE; |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
192 |
); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
193 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
194 |
val set_string = Local_Data.put o SOME; |
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 |
fun the_string ctxt = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
197 |
(case Local_Data.get ctxt of |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
198 |
SOME s => s |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
199 |
| NONE => raise Fail "No result string"); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
200 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
201 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
202 |
Theory.setup |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
203 |
(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
|
204 |
(fn {context = ctxt, file_type, argument, ...} => |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
205 |
ctxt |> Context.proof_map |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
206 |
(ML_Context.expression (Input.pos_of argument) |
69383 | 207 |
(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
|
208 |
ML_Lex.read_source argument @ ML_Lex.read "))")) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
209 |
|> the_string |> #make_string file_type)); |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
210 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
211 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
212 |
(* file-system paths *) |
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 path_antiquotation binding check = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
215 |
antiquotation binding |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
216 |
(Args.context -- Scan.lift (Parse.position Parse.path) >> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
217 |
(fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode))) |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
218 |
(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
|
219 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
220 |
val _ = |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
221 |
Theory.setup |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
222 |
(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
|
223 |
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
|
224 |
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
|
225 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
diff
changeset
|
226 |
end; |