5 Configuration for ProofGeneral of LFCS Edinburgh. |
5 Configuration for ProofGeneral of LFCS Edinburgh. |
6 *) |
6 *) |
7 |
7 |
8 signature PROOF_GENERAL = |
8 signature PROOF_GENERAL = |
9 sig |
9 sig |
|
10 val write_keywords: string -> unit |
10 val setup: (theory -> theory) list |
11 val setup: (theory -> theory) list |
11 val init: bool -> unit |
12 val init: bool -> unit |
12 end; |
13 end; |
13 |
14 |
14 structure ProofGeneral: PROOF_GENERAL = |
15 structure ProofGeneral: PROOF_GENERAL = |
15 struct |
16 struct |
|
17 |
|
18 |
|
19 (** generate keyword classification file **) |
|
20 |
|
21 local |
|
22 |
|
23 val regexp_meta = explode ".*+?[]^$"; |
|
24 val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode; |
|
25 |
|
26 fun defconst name strs = |
|
27 "\n(defconst isar-keywords-" ^ name ^ |
|
28 "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; |
|
29 |
|
30 fun make_elisp_commands commands kind = |
|
31 defconst kind (mapfilter (fn (c, k) => if k = kind then Some c else None) commands); |
|
32 |
|
33 fun make_elisp_syntax (keywords, commands) = |
|
34 ";;\n\ |
|
35 \;; Keyword classification tables for Isabelle/Isar.\n\ |
|
36 \;; This file generated by Isabelle -- DO NOT EDIT!\n\ |
|
37 \;;\n\ |
|
38 \;; $Id$\n\ |
|
39 \;;\n" ^ |
|
40 defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^ |
|
41 implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ |
|
42 "\n(provide 'isar-keywords)\n"; |
|
43 |
|
44 in |
|
45 |
|
46 fun write_keywords file = |
|
47 File.write (Path.unpack file) (make_elisp_syntax (OuterSyntax.dest_syntax ())); |
|
48 |
|
49 end; |
|
50 |
16 |
51 |
17 |
52 |
18 (** compile-time theory setup **) |
53 (** compile-time theory setup **) |
19 |
54 |
20 (* token translations *) |
55 (* token translations *) |