author | wenzelm |
Tue, 23 Nov 2021 12:29:09 +0100 | |
changeset 74832 | c299abcf7081 |
parent 74831 | 32490add64b4 |
child 74835 | 26c3a9c92e11 |
permissions | -rw-r--r-- |
48879 | 1 |
(* Title: Pure/pure_syn.ML |
2 |
Author: Makarius |
|
3 |
||
60096 | 4 |
Outer syntax for bootstrapping: commands that are accessible outside a |
5 |
regular theory context. |
|
48879 | 6 |
*) |
7 |
||
60095 | 8 |
signature PURE_SYN = |
9 |
sig |
|
10 |
val bootstrap_thy: theory |
|
11 |
end; |
|
12 |
||
13 |
structure Pure_Syn: PURE_SYN = |
|
48879 | 14 |
struct |
15 |
||
62912 | 16 |
val semi = Scan.option (Parse.$$$ ";"); |
17 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
18 |
val _ = |
64556 | 19 |
Outer_Syntax.command ("chapter", \<^here>) "chapter heading" |
74832 | 20 |
(Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
21 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
22 |
val _ = |
64556 | 23 |
Outer_Syntax.command ("section", \<^here>) "section heading" |
74832 | 24 |
(Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); |
58918 | 25 |
|
48879 | 26 |
val _ = |
64556 | 27 |
Outer_Syntax.command ("subsection", \<^here>) "subsection heading" |
74832 | 28 |
(Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
29 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
30 |
val _ = |
64556 | 31 |
Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading" |
74832 | 32 |
(Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
33 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
34 |
val _ = |
64556 | 35 |
Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading" |
74832 | 36 |
(Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); |
61463 | 37 |
|
38 |
val _ = |
|
64556 | 39 |
Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading" |
74832 | 40 |
(Parse.opt_target -- Parse.document_source --| semi >> Document_Output.document_output); |
61463 | 41 |
|
42 |
val _ = |
|
64556 | 43 |
Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)" |
74832 | 44 |
(Parse.opt_target -- Parse.document_source >> Document_Output.document_output_markdown); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
45 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
46 |
val _ = |
64556 | 47 |
Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)" |
74832 | 48 |
(Parse.opt_target -- Parse.document_source >> Document_Output.document_output_markdown); |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
49 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
50 |
val _ = |
64556 | 51 |
Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)" |
74832 | 52 |
(Parse.opt_target -- Parse.document_source >> Document_Output.document_output_markdown); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
53 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
54 |
val _ = |
64556 | 55 |
Outer_Syntax.command ("theory", \<^here>) "begin theory" |
58852 | 56 |
(Thy_Header.args >> |
57 |
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
|
48879 | 58 |
|
60095 | 59 |
|
62876 | 60 |
val bootstrap_thy = Context.the_global_context (); |
60095 | 61 |
|
62 |
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false); |
|
63 |
||
48879 | 64 |
end; |