author | wenzelm |
Wed, 29 Nov 2023 00:07:54 +0100 | |
changeset 79074 | 7f24c5be57bd |
parent 74838 | 4c8d9479f916 |
permissions | -rw-r--r-- |
74836
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ex/Alternative_Headings.thy |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
3 |
*) |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
4 |
|
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
5 |
chapter \<open>Alternative document headings\<close> |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
6 |
|
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
7 |
theory Alternative_Headings |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
8 |
imports Pure |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
9 |
keywords |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
10 |
"chapter*" "section*" "subsection*" "subsubsection*" :: document_heading |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
11 |
begin |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
12 |
|
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
13 |
ML \<open> |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
14 |
local |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
15 |
|
74838
4c8d9479f916
more uniform treatment of optional_argument for Latex elements;
wenzelm
parents:
74836
diff
changeset
|
16 |
fun alternative_heading name body = |
4c8d9479f916
more uniform treatment of optional_argument for Latex elements;
wenzelm
parents:
74836
diff
changeset
|
17 |
[XML.Elem (Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*", body)]; |
74836
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
18 |
|
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
19 |
fun document_heading (name, pos) = |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
20 |
Outer_Syntax.command (name, pos) (name ^ " heading") |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
21 |
(Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >> |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
22 |
Document_Output.document_output |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
23 |
{markdown = false, markup = alternative_heading name}); |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
24 |
|
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
25 |
val _ = |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
26 |
List.app document_heading |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
27 |
[\<^command_keyword>\<open>chapter*\<close>, |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
28 |
\<^command_keyword>\<open>section*\<close>, |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
29 |
\<^command_keyword>\<open>subsection*\<close>, |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
30 |
\<^command_keyword>\<open>subsubsection*\<close>]; |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
31 |
|
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
32 |
in end\<close> |
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
33 |
|
a97ec0954c50
example: alternative document headings, based on more general document output markup;
wenzelm
parents:
diff
changeset
|
34 |
end |