equal
deleted
inserted
replaced
4 Outer syntax for Isabelle/Pure. |
4 Outer syntax for Isabelle/Pure. |
5 *) |
5 *) |
6 |
6 |
7 structure Isar_Syn: sig end = |
7 structure Isar_Syn: sig end = |
8 struct |
8 struct |
9 |
|
10 (** markup commands **) |
|
11 |
|
12 val _ = |
|
13 Outer_Syntax.markup_command Outer_Syntax.Markup_Env |
|
14 @{command_spec "text"} "formal comment (theory)" |
|
15 (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup); |
|
16 |
|
17 val _ = |
|
18 Outer_Syntax.markup_command Outer_Syntax.Verbatim |
|
19 @{command_spec "text_raw"} "raw document preparation text" |
|
20 (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup); |
|
21 |
|
22 val _ = |
|
23 Outer_Syntax.markup_command Outer_Syntax.Markup_Env |
|
24 @{command_spec "txt"} "formal comment (proof)" |
|
25 (Parse.document_source >> Thy_Output.proof_markup); |
|
26 |
|
27 val _ = |
|
28 Outer_Syntax.markup_command Outer_Syntax.Verbatim |
|
29 @{command_spec "txt_raw"} "raw document preparation text (proof)" |
|
30 (Parse.document_source >> Thy_Output.proof_markup); |
|
31 |
|
32 |
|
33 |
9 |
34 (** theory commands **) |
10 (** theory commands **) |
35 |
11 |
36 (* sorts *) |
12 (* sorts *) |
37 |
13 |