author | wenzelm |
Sat, 03 Feb 2018 14:39:17 +0100 | |
changeset 67569 | 5d71b114e7a3 |
parent 67381 | 146757999c8d |
child 69965 | da5e7278286b |
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 |
||
67569
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
20 |
fun output_document state markdown txt = |
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
21 |
let |
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
22 |
val ctxt = Toplevel.presentation_context state; |
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
23 |
val _ = |
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
24 |
Context_Position.report ctxt |
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
25 |
(Input.pos_of txt) (Markup.language_document (Input.is_delimited txt)); |
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
26 |
in Thy_Output.output_document ctxt markdown txt end; |
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
27 |
|
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
28 |
fun document_command markdown (loc, txt) = |
67381 | 29 |
Toplevel.keep (fn state => |
30 |
(case loc of |
|
67569
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
31 |
NONE => ignore (output_document state markdown txt) |
67381 | 32 |
| SOME (_, pos) => |
33 |
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o |
|
34 |
Toplevel.present_local_theory loc (fn state => |
|
67569
5d71b114e7a3
avoid proliferation of language_document reports;
wenzelm
parents:
67381
diff
changeset
|
35 |
ignore (output_document state markdown txt)); |
67381 | 36 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
37 |
val _ = |
64556 | 38 |
Outer_Syntax.command ("chapter", \<^here>) "chapter heading" |
67381 | 39 |
(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
|
40 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
41 |
val _ = |
64556 | 42 |
Outer_Syntax.command ("section", \<^here>) "section heading" |
67381 | 43 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
58918 | 44 |
|
48879 | 45 |
val _ = |
64556 | 46 |
Outer_Syntax.command ("subsection", \<^here>) "subsection heading" |
67381 | 47 |
(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
|
48 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
49 |
val _ = |
64556 | 50 |
Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading" |
67381 | 51 |
(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
|
52 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
53 |
val _ = |
64556 | 54 |
Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading" |
67381 | 55 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
61463 | 56 |
|
57 |
val _ = |
|
64556 | 58 |
Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading" |
67381 | 59 |
(Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); |
61463 | 60 |
|
61 |
val _ = |
|
64556 | 62 |
Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)" |
67381 | 63 |
(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
|
64 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
65 |
val _ = |
64556 | 66 |
Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)" |
67381 | 67 |
(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
|
68 |
|
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58928
diff
changeset
|
69 |
val _ = |
64556 | 70 |
Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)" |
67381 | 71 |
(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
|
72 |
|
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58918
diff
changeset
|
73 |
val _ = |
64556 | 74 |
Outer_Syntax.command ("theory", \<^here>) "begin theory" |
58852 | 75 |
(Thy_Header.args >> |
76 |
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization"))); |
|
48879 | 77 |
|
60095 | 78 |
|
62876 | 79 |
val bootstrap_thy = Context.the_global_context (); |
60095 | 80 |
|
81 |
val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false); |
|
82 |
||
48879 | 83 |
end; |