plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
(* Title: Pure/pure_syn.ML
Author: Makarius
Outer syntax for bootstrapping Isabelle/Pure.
*)
structure Pure_Syn: sig end =
struct
val _ =
Outer_Syntax.markup_command Outer_Syntax.Markup ("header", @{here}) "theory header"
(Parse.document_source >> Thy_Output.header_markup);
val _ =
Outer_Syntax.markup_command Outer_Syntax.Markup ("chapter", @{here}) "chapter heading"
(Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
val _ =
Outer_Syntax.markup_command Outer_Syntax.Markup ("section", @{here}) "section heading"
(Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
val _ =
Outer_Syntax.markup_command Outer_Syntax.Markup ("subsection", @{here}) "subsection heading"
(Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
val _ =
Outer_Syntax.markup_command Outer_Syntax.Markup ("subsubsection", @{here}) "subsubsection heading"
(Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
val _ =
Outer_Syntax.command ("theory", @{here}) "begin theory"
(Thy_Header.args >>
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
end;