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