8 struct |
8 struct |
9 |
9 |
10 (** markup commands **) |
10 (** markup commands **) |
11 |
11 |
12 val _ = |
12 val _ = |
13 Outer_Syntax.markup_command Thy_Output.Markup |
13 Outer_Syntax.markup_command Outer_Syntax.Markup_Env |
14 @{command_spec "header"} "theory header" |
|
15 (Parse.document_source >> Isar_Cmd.header_markup); |
|
16 |
|
17 val _ = |
|
18 Outer_Syntax.markup_command Thy_Output.Markup |
|
19 @{command_spec "chapter"} "chapter heading" |
|
20 (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); |
|
21 |
|
22 val _ = |
|
23 Outer_Syntax.markup_command Thy_Output.Markup |
|
24 @{command_spec "section"} "section heading" |
|
25 (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); |
|
26 |
|
27 val _ = |
|
28 Outer_Syntax.markup_command Thy_Output.Markup |
|
29 @{command_spec "subsection"} "subsection heading" |
|
30 (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); |
|
31 |
|
32 val _ = |
|
33 Outer_Syntax.markup_command Thy_Output.Markup |
|
34 @{command_spec "subsubsection"} "subsubsection heading" |
|
35 (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); |
|
36 |
|
37 val _ = |
|
38 Outer_Syntax.markup_command Thy_Output.MarkupEnv |
|
39 @{command_spec "text"} "formal comment (theory)" |
14 @{command_spec "text"} "formal comment (theory)" |
40 (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup); |
15 (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup); |
41 |
16 |
42 val _ = |
17 val _ = |
43 Outer_Syntax.markup_command Thy_Output.Verbatim |
18 Outer_Syntax.markup_command Outer_Syntax.Verbatim |
44 @{command_spec "text_raw"} "raw document preparation text" |
19 @{command_spec "text_raw"} "raw document preparation text" |
45 (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup); |
20 (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup); |
46 |
21 |
47 val _ = |
22 val _ = |
48 Outer_Syntax.markup_command Thy_Output.MarkupEnv |
23 Outer_Syntax.markup_command Outer_Syntax.Markup_Env |
49 @{command_spec "txt"} "formal comment (proof)" |
24 @{command_spec "txt"} "formal comment (proof)" |
50 (Parse.document_source >> Isar_Cmd.proof_markup); |
25 (Parse.document_source >> Thy_Output.proof_markup); |
51 |
26 |
52 val _ = |
27 val _ = |
53 Outer_Syntax.markup_command Thy_Output.Verbatim |
28 Outer_Syntax.markup_command Outer_Syntax.Verbatim |
54 @{command_spec "txt_raw"} "raw document preparation text (proof)" |
29 @{command_spec "txt_raw"} "raw document preparation text (proof)" |
55 (Parse.document_source >> Isar_Cmd.proof_markup); |
30 (Parse.document_source >> Thy_Output.proof_markup); |
56 |
31 |
57 |
32 |
58 |
33 |
59 (** theory commands **) |
34 (** theory commands **) |
60 |
35 |
728 |
703 |
729 val _ = |
704 val _ = |
730 Outer_Syntax.command @{command_spec "help"} |
705 Outer_Syntax.command @{command_spec "help"} |
731 "retrieve outer syntax commands according to name patterns" |
706 "retrieve outer syntax commands according to name patterns" |
732 (Scan.repeat Parse.name >> |
707 (Scan.repeat Parse.name >> |
733 (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_syntax pats))); |
708 (fn pats => Toplevel.keep (fn st => Outer_Syntax.help_syntax (Toplevel.theory_of st) pats))); |
734 |
709 |
735 val _ = |
710 val _ = |
736 Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands" |
711 Outer_Syntax.command @{command_spec "print_commands"} "print outer syntax commands" |
737 (Scan.succeed (Toplevel.imperative Outer_Syntax.print_syntax)); |
712 (Scan.succeed (Toplevel.keep (Outer_Syntax.print_syntax o Toplevel.theory_of))); |
738 |
713 |
739 val _ = |
714 val _ = |
740 Outer_Syntax.command @{command_spec "print_options"} "print configuration options" |
715 Outer_Syntax.command @{command_spec "print_options"} "print configuration options" |
741 (Scan.succeed (Toplevel.unknown_context o |
716 (Scan.succeed (Toplevel.unknown_context o |
742 Toplevel.keep (Attrib.print_options o Toplevel.context_of))); |
717 Toplevel.keep (Attrib.print_options o Toplevel.context_of))); |