| author | wenzelm |
| Wed, 02 Mar 2022 21:14:09 +0100 | |
| changeset 75189 | f304a2a5080f |
| 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 |