# HG changeset patch # User wenzelm # Date 1445109310 -7200 # Node ID 8e46cea6a45a2f61b9740d0cc80c4fe81e6d7492 # Parent e16649b70107c189e52048512b329e719bb6eac8 added 'paragraph', 'subparagraph'; diff -r e16649b70107 -r 8e46cea6a45a NEWS --- 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 *** diff -r e16649b70107 -r 8e46cea6a45a lib/texinputs/isabelle.sty --- 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} diff -r e16649b70107 -r 8e46cea6a45a src/Doc/Isar_Ref/Document_Preparation.thy --- 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 \ any"} \\ @{command_def "subsection"} & : & @{text "any \ any"} \\ @{command_def "subsubsection"} & : & @{text "any \ any"} \\ + @{command_def "paragraph"} & : & @{text "any \ any"} \\ + @{command_def "subparagraph"} & : & @{text "any \ any"} \\ @{command_def "text"} & : & @{text "any \ any"} \\ @{command_def "txt"} & : & @{text "any \ any"} \\ @{command_def "text_raw"} & : & @{text "any \ any"} \\ @@ -44,33 +46,29 @@ @{rail \ (@@{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} \} - \<^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 \\isamarkupchapter\}, @{verbatim \\isamarkupsection\}, - @{verbatim \\isamarkupsubsection\}, @{verbatim \\isamarkupsubsubsection\}. + \<^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 \\isamarkupchapter\}, @{verbatim + \\isamarkupsection\}, @{verbatim \\isamarkupsubsection\} etc.\ \<^descr> @{command text} and @{command txt} specify paragraphs of plain text. This corresponds to a {\LaTeX} environment @{verbatim \\begin{isamarkuptext}\} @{text "\"} @{verbatim \\end{isamarkuptext}\} 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 diff -r e16649b70107 -r 8e46cea6a45a src/Pure/Isar/outer_syntax.scala --- 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 } } diff -r e16649b70107 -r 8e46cea6a45a src/Pure/Thy/thy_header.ML --- 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) -- diff -r e16649b70107 -r 8e46cea6a45a src/Pure/Thy/thy_header.scala --- 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)) ~ diff -r e16649b70107 -r 8e46cea6a45a src/Pure/Tools/update_header.scala --- 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)) } } } diff -r e16649b70107 -r 8e46cea6a45a src/Pure/pure_syn.ML --- 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});