--- a/src/Pure/pure_syn.ML Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/pure_syn.ML Thu Nov 06 11:44:41 2014 +0100
@@ -7,15 +7,32 @@
structure Pure_Syn: sig end =
struct
+(* keywords *)
+
+val keywords: Thy_Header.keywords =
+ [("theory", SOME (("thy_begin", []), ["theory"])),
+ ("ML_file", SOME (("thy_load", []), ["ML"]))];
+
+fun command_spec (name, pos) =
+ (case AList.lookup (op =) keywords name of
+ SOME (SOME spec) => Keyword.command_spec ((name, spec), pos)
+ | _ => error ("Bad command specification " ^ quote name ^ Position.here pos));
+
+val _ = Thy_Header.define_keywords keywords;
+val _ = Theory.setup (fold Thy_Header.declare_keyword keywords);
+
+
+(* commands *)
+
val _ =
Outer_Syntax.command
- (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
+ (command_spec ("theory", @{here})) "begin theory"
(Thy_Header.args >>
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
val _ =
Outer_Syntax.command
- (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
+ (command_spec ("ML_file", @{here})) "ML text from file"
(Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);