26 fun defconst name strs = |
26 fun defconst name strs = |
27 "\n(defconst isar-keywords-" ^ name ^ |
27 "\n(defconst isar-keywords-" ^ name ^ |
28 "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; |
28 "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; |
29 |
29 |
30 fun make_elisp_commands commands kind = |
30 fun make_elisp_commands commands kind = |
31 defconst kind (mapfilter (fn (c, k) => if k = kind then Some c else None) commands); |
31 defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands); |
32 |
32 |
33 fun make_elisp_syntax (keywords, commands) = |
33 fun make_elisp_syntax (keywords, commands) = |
34 ";;\n\ |
34 ";;\n\ |
35 \;; Keyword classification tables for Isabelle/Isar.\n\ |
35 \;; Keyword classification tables for Isabelle/Isar.\n\ |
36 \;; This file generated by Isabelle -- DO NOT EDIT!\n\ |
36 \;; This file generated by Isabelle -- DO NOT EDIT!\n\ |
37 \;;\n\ |
37 \;;\n\ |
38 \;; $" ^ "Id$\n\ |
38 \;; $" ^ "Id$\n\ |
39 \;;\n" ^ |
39 \;;\n" ^ |
40 defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^ |
40 defconst "minor" (filter Syntax.is_identifier keywords) ^ |
41 implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ |
41 implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^ |
42 "\n(provide 'isar-keywords)\n"; |
42 "\n(provide 'isar-keywords)\n"; |
43 |
43 |
44 val keywords_file = "isar-keywords.el"; |
44 val keywords_file = "isar-keywords.el"; |
45 |
45 |
46 in |
46 in |
47 |
47 |
48 fun write_keywords () = |
48 fun write_keywords () = |
49 File.write (Path.unpack keywords_file) (make_elisp_syntax (OuterSyntax.dest_syntax ())); |
49 File.write (Path.unpack keywords_file) |
|
50 (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())); |
50 |
51 |
51 end; |
52 end; |
52 |
53 |
53 |
54 |
54 |
55 |