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