--- a/NEWS Sat Oct 17 20:27:12 2015 +0200
+++ b/NEWS Sat Oct 17 21:15:10 2015 +0200
@@ -57,19 +57,27 @@
*** Document preparation ***
-* Isabelle control symbols for markup and formatting:
+* Commands 'paragraph' and 'subparagraph' provide additional section
+headings. Thus there are 6 levels of standard headings, as in HTML.
+
+* Text is structured in paragraphs and nested lists, using notation that
+is similar to Markdown. The control symbols for list items are as
+follows:
+
+ \<^item> itemize
+ \<^enum> enumerate
+ \<^descr> description
+
+* Text may contain control symbols for markup and formatting as follows:
\<^noindent> \noindent
\<^smallskip> \smallskip
\<^medskip> \medskip
\<^bigskip> \bigskip
-* Paragraphs and nested lists may be specified similarly to Markdown,
-with control symbols to indicate list items as follows:
-
- \<^item> itemize
- \<^enum> enumerate
- \<^descr> description
+* Command 'text_raw' has been clarified: input text is processed as in
+'text' (with antiquotations and control symbols). The key difference is
+the lack of the surrounding isabelle markup environment in output.
*** Isar ***
--- a/lib/texinputs/isabelle.sty Sat Oct 17 20:27:12 2015 +0200
+++ b/lib/texinputs/isabelle.sty Sat Oct 17 21:15:10 2015 +0200
@@ -133,6 +133,8 @@
\newcommand{\isamarkupsection}[1]{\section{#1}}
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
+\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
\newif\ifisamarkup
\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sat Oct 17 21:15:10 2015 +0200
@@ -26,6 +26,8 @@
@{command_def "section"} & : & @{text "any \<rightarrow> any"} \\
@{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\
@{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\
+ @{command_def "paragraph"} & : & @{text "any \<rightarrow> any"} \\
+ @{command_def "subparagraph"} & : & @{text "any \<rightarrow> any"} \\
@{command_def "text"} & : & @{text "any \<rightarrow> any"} \\
@{command_def "txt"} & : & @{text "any \<rightarrow> any"} \\
@{command_def "text_raw"} & : & @{text "any \<rightarrow> any"} \\
@@ -44,33 +46,29 @@
@{rail \<open>
(@@{command chapter} | @@{command section} | @@{command subsection} |
- @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text}
- ;
- @@{command text_raw} @{syntax text}
+ @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph} |
+ @@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
\<close>}
- \<^descr> @{command chapter}, @{command section}, @{command subsection}, and
- @{command subsubsection} mark chapter and section headings within the
- theory source; this works in any context, even before the initial
- @{command theory} command. The corresponding {\LaTeX} macros are
- @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},
- @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}.
+ \<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark
+ section headings within the theory source. This works in any context, even
+ before the initial @{command theory} command. The corresponding {\LaTeX}
+ macros are @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim
+ \<open>\isamarkupsection\<close>}, @{verbatim \<open>\isamarkupsubsection\<close>} etc.\
\<^descr> @{command text} and @{command txt} specify paragraphs of plain text.
This corresponds to a {\LaTeX} environment @{verbatim
\<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>}
etc.
- \<^descr> @{command text_raw} inserts {\LaTeX} source directly into the
- output, without additional markup. Thus the full range of document
- manipulations becomes available, at the risk of messing up document
- output.
+ \<^descr> @{command text_raw} is similar to @{command text}, but without
+ any surrounding markup environment. This allows to inject arbitrary
+ {\LaTeX} source into the generated document.
- Except for @{command "text_raw"}, the text passed to any of the above
- markup commands may refer to formal entities via \emph{document
- antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
- present theory or proof context.
+ All text passed to any of the above markup commands may refer to formal
+ entities via \emph{document antiquotations}, see also \secref{sec:antiq}.
+ These are interpreted in the present theory or proof context.
\<^medskip>
The proof markup commands closely resemble those for theory
--- a/src/Pure/Isar/outer_syntax.scala Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sat Oct 17 21:15:10 2015 +0200
@@ -240,9 +240,11 @@
case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
case Thy_Header.SUBSECTION => Some(2)
case Thy_Header.SUBSUBSECTION => Some(3)
+ case Thy_Header.PARAGRAPH => Some(4)
+ case Thy_Header.SUBPARAGRAPH => Some(5)
case _ =>
keywords.command_kind(name) match {
- case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
+ case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
case _ => None
}
}
--- a/src/Pure/Thy/thy_header.ML Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Pure/Thy/thy_header.ML Sat Oct 17 21:15:10 2015 +0200
@@ -42,11 +42,14 @@
(* bootstrap keywords *)
-val headerN = "header";
+val headerN = "header"; (* FIXME legacy *)
+
val chapterN = "chapter";
val sectionN = "section";
val subsectionN = "subsection";
val subsubsectionN = "subsubsection";
+val paragraphN = "paragraph";
+val subparagraphN = "subparagraph";
val textN = "text";
val txtN = "txt";
val text_rawN = "text_raw";
@@ -74,6 +77,8 @@
((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((paragraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((subparagraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
((textN, @{here}), SOME ((Keyword.document_body, []), [])),
((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
@@ -147,6 +152,8 @@
Parse.command sectionN ||
Parse.command subsectionN ||
Parse.command subsubsectionN ||
+ Parse.command paragraphN ||
+ Parse.command subparagraphN ||
Parse.command textN ||
Parse.command txtN ||
Parse.command text_rawN) --
--- a/src/Pure/Thy/thy_header.scala Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Pure/Thy/thy_header.scala Sat Oct 17 21:15:10 2015 +0200
@@ -19,11 +19,14 @@
type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
- val HEADER = "header"
+ val HEADER = "header" /* FIXME legacy */
+
val CHAPTER = "chapter"
val SECTION = "section"
val SUBSECTION = "subsection"
val SUBSUBSECTION = "subsubsection"
+ val PARAGRAPH = "paragraph"
+ val SUBPARAGRAPH = "subparagraph"
val TEXT = "text"
val TXT = "txt"
val TEXT_RAW = "text_raw"
@@ -51,6 +54,8 @@
(SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (PARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+ (SUBPARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
(TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
(TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
@@ -115,6 +120,8 @@
command(SECTION) |
command(SUBSECTION) |
command(SUBSUBSECTION) |
+ command(PARAGRAPH) |
+ command(SUBPARAGRAPH) |
command(TEXT) |
command(TXT) |
command(TEXT_RAW)) ~
--- a/src/Pure/Tools/update_header.scala Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Pure/Tools/update_header.scala Sat Oct 17 21:15:10 2015 +0200
@@ -25,15 +25,19 @@
/* command line entry point */
+ private val headings =
+ Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
+
def main(args: Array[String])
{
Command_Line.tool0 {
args.toList match {
case section :: files =>
- if (!Set("chapter", "section", "subsection", "subsubsection").contains(section))
+ if (!headings.contains(section))
error("Bad heading command: " + quote(section))
files.foreach(file => update_header(section, Path.explode(file)))
- case _ => error("Bad arguments:\n" + cat_lines(args))
+ case _ =>
+ error("Bad arguments:\n" + cat_lines(args))
}
}
}
--- a/src/Pure/pure_syn.ML Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Pure/pure_syn.ML Sat Oct 17 21:15:10 2015 +0200
@@ -34,6 +34,14 @@
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
val _ =
+ Outer_Syntax.command ("paragraph", @{here}) "paragraph heading"
+ (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+
+val _ =
+ Outer_Syntax.command ("subparagraph", @{here}) "subparagraph heading"
+ (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
+
+val _ =
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});