author | wenzelm |
Fri, 21 May 2021 12:29:29 +0200 | |
changeset 73761 | ef1a18e20ace |
parent 73752 | eeb076fc569f |
child 74831 | 32490add64b4 |
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 |
|
67381 | 10 |
val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source -> |
11 |
Toplevel.transition -> Toplevel.transition |
|
60095 | 12 |
val bootstrap_thy: theory |
13 |
end; |
|
14 |
||
15 |
structure Pure_Syn: PURE_SYN = |
|
48879 | 16 |
struct |
17 |
||
62912 | 18 |
val semi = Scan.option (Parse.$$$ ";"); |
19 |
||
73752 | 20 |
fun output_document state markdown txt = |
21 |
let |
|
22 |
val ctxt = Toplevel.presentation_context state; |
|
73761 | 23 |
val _ = Context_Position.reports ctxt (Document_Output.document_reports txt); |
24 |
in Document_Output.output_document ctxt markdown txt end; |
|
67569
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
25 |
|
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
26 |
fun document_command markdown (loc, txt) = |
67381 | 27 |
Toplevel.keep (fn state => |
28 |
(case loc of |
|
67569
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
29 |
NONE => ignore (output_document state markdown txt) |
67381 | 30 |
| SOME (_, pos) => |
31 |
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o |
|
32 |
Toplevel.present_local_theory loc (fn state => |
|
67569
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
33 |
ignore (output_document state markdown txt)); |
67381 | 34 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
35 |
val _ = |
64556 | 36 |
Outer_Syntax.command ("chapter", \<^here>) "chapter heading" |
67381 | 37 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
38 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
39 |
val _ = |
64556 | 40 |
Outer_Syntax.command ("section", \<^here>) "section heading" |
67381 | 41 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
58918 | 42 |
|
48879 | 43 |
val _ = |
64556 | 44 |
Outer_Syntax.command ("subsection", \<^here>) "subsection heading" |
67381 | 45 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
46 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
47 |
val _ = |
64556 | 48 |
Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading" |
67381 | 49 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
50 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
51 |
val _ = |
64556 | 52 |
Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading" |
67381 | 53 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
61463 | 54 |
|
55 |
val _ = |
|
64556 | 56 |
Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading" |
67381 | 57 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
61463 | 58 |
|
59 |
val _ = |
|
64556 | 60 |
Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)" |
67381 | 61 |
(Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
62 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
63 |
val _ = |
64556 | 64 |
Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)" |
67381 | 65 |
(Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); |
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
66 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
67 |
val _ = |
64556 | 68 |
Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)" |
67381 | 69 |
(Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
70 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
71 |
val _ = |
64556 | 72 |
Outer_Syntax.command ("theory", \<^here>) "begin theory" |
58852 | 73 |
(Thy_Header.args >> |
74 |
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
|
48879 | 75 |
|
60095 | 76 |
|
62876 | 77 |
val bootstrap_thy = Context.the_global_context (); |
60095 | 78 |
|
79 |
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false); |
|
80 |
||
48879 | 81 |
end; |