added 'paragraph', 'subparagraph';
authorwenzelm
Sat Oct 17 21:15:10 2015 +0200 (2015-10-17)
changeset 614638e46cea6a45a
parent 61462 e16649b70107
child 61464 d35ff80f27fb
added 'paragraph', 'subparagraph';
NEWS
lib/texinputs/isabelle.sty
src/Doc/Isar_Ref/Document_Preparation.thy
src/Pure/Isar/outer_syntax.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Tools/update_header.scala
src/Pure/pure_syn.ML
     1.1 --- a/NEWS	Sat Oct 17 20:27:12 2015 +0200
     1.2 +++ b/NEWS	Sat Oct 17 21:15:10 2015 +0200
     1.3 @@ -57,19 +57,27 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* Isabelle control symbols for markup and formatting:
     1.8 +* Commands 'paragraph' and 'subparagraph' provide additional section
     1.9 +headings. Thus there are 6 levels of standard headings, as in HTML.
    1.10 +
    1.11 +* Text is structured in paragraphs and nested lists, using notation that
    1.12 +is similar to Markdown. The control symbols for list items are as
    1.13 +follows:
    1.14 +
    1.15 +  \<^item>  itemize
    1.16 +  \<^enum>  enumerate
    1.17 +  \<^descr>  description
    1.18 +
    1.19 +* Text may contain control symbols for markup and formatting as follows:
    1.20  
    1.21    \<^noindent>   \noindent
    1.22    \<^smallskip>   \smallskip
    1.23    \<^medskip>   \medskip
    1.24    \<^bigskip>   \bigskip
    1.25  
    1.26 -* Paragraphs and nested lists may be specified similarly to Markdown,
    1.27 -with control symbols to indicate list items as follows:
    1.28 -
    1.29 -  \<^item>  itemize
    1.30 -  \<^enum>  enumerate
    1.31 -  \<^descr>  description
    1.32 +* Command 'text_raw' has been clarified: input text is processed as in
    1.33 +'text' (with antiquotations and control symbols). The key difference is
    1.34 +the lack of the surrounding isabelle markup environment in output.
    1.35  
    1.36  
    1.37  *** Isar ***
     2.1 --- a/lib/texinputs/isabelle.sty	Sat Oct 17 20:27:12 2015 +0200
     2.2 +++ b/lib/texinputs/isabelle.sty	Sat Oct 17 21:15:10 2015 +0200
     2.3 @@ -133,6 +133,8 @@
     2.4  \newcommand{\isamarkupsection}[1]{\section{#1}}
     2.5  \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
     2.6  \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
     2.7 +\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
     2.8 +\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
     2.9  
    2.10  \newif\ifisamarkup
    2.11  \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
     3.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Oct 17 20:27:12 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Oct 17 21:15:10 2015 +0200
     3.3 @@ -26,6 +26,8 @@
     3.4      @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\
     3.5      @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\
     3.6      @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\
     3.7 +    @{command_def "paragraph"} & : & @{text "any \<rightarrow> any"} \\
     3.8 +    @{command_def "subparagraph"} & : & @{text "any \<rightarrow> any"} \\
     3.9      @{command_def "text"} & : & @{text "any \<rightarrow> any"} \\
    3.10      @{command_def "txt"} & : & @{text "any \<rightarrow> any"} \\
    3.11      @{command_def "text_raw"} & : & @{text "any \<rightarrow> any"} \\
    3.12 @@ -44,33 +46,29 @@
    3.13  
    3.14    @{rail \<open>
    3.15      (@@{command chapter} | @@{command section} | @@{command subsection} |
    3.16 -      @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text}
    3.17 -    ;
    3.18 -    @@{command text_raw} @{syntax text}
    3.19 +      @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph} |
    3.20 +      @@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text}
    3.21    \<close>}
    3.22  
    3.23 -  \<^descr> @{command chapter}, @{command section}, @{command subsection}, and
    3.24 -  @{command subsubsection} mark chapter and section headings within the
    3.25 -  theory source; this works in any context, even before the initial
    3.26 -  @{command theory} command. The corresponding {\LaTeX} macros are
    3.27 -  @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},
    3.28 -  @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}.
    3.29 +  \<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark
    3.30 +  section headings within the theory source. This works in any context, even
    3.31 +  before the initial @{command theory} command. The corresponding {\LaTeX}
    3.32 +  macros are @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim
    3.33 +  \<open>\isamarkupsection\<close>}, @{verbatim \<open>\isamarkupsubsection\<close>} etc.\
    3.34  
    3.35    \<^descr> @{command text} and @{command txt} specify paragraphs of plain text.
    3.36    This corresponds to a {\LaTeX} environment @{verbatim
    3.37    \<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>}
    3.38    etc.
    3.39  
    3.40 -  \<^descr> @{command text_raw} inserts {\LaTeX} source directly into the
    3.41 -  output, without additional markup. Thus the full range of document
    3.42 -  manipulations becomes available, at the risk of messing up document
    3.43 -  output.
    3.44 +  \<^descr> @{command text_raw} is similar to @{command text}, but without
    3.45 +  any surrounding markup environment. This allows to inject arbitrary
    3.46 +  {\LaTeX} source into the generated document.
    3.47  
    3.48  
    3.49 -  Except for @{command "text_raw"}, the text passed to any of the above
    3.50 -  markup commands may refer to formal entities via \emph{document
    3.51 -  antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
    3.52 -  present theory or proof context.
    3.53 +  All text passed to any of the above markup commands may refer to formal
    3.54 +  entities via \emph{document antiquotations}, see also \secref{sec:antiq}.
    3.55 +  These are interpreted in the present theory or proof context.
    3.56  
    3.57    \<^medskip>
    3.58    The proof markup commands closely resemble those for theory
     4.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 17 20:27:12 2015 +0200
     4.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 17 21:15:10 2015 +0200
     4.3 @@ -240,9 +240,11 @@
     4.4        case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
     4.5        case Thy_Header.SUBSECTION => Some(2)
     4.6        case Thy_Header.SUBSUBSECTION => Some(3)
     4.7 +      case Thy_Header.PARAGRAPH => Some(4)
     4.8 +      case Thy_Header.SUBPARAGRAPH => Some(5)
     4.9        case _ =>
    4.10          keywords.command_kind(name) match {
    4.11 -          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
    4.12 +          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
    4.13            case _ => None
    4.14          }
    4.15      }
     5.1 --- a/src/Pure/Thy/thy_header.ML	Sat Oct 17 20:27:12 2015 +0200
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Sat Oct 17 21:15:10 2015 +0200
     5.3 @@ -42,11 +42,14 @@
     5.4  
     5.5  (* bootstrap keywords *)
     5.6  
     5.7 -val headerN = "header";
     5.8 +val headerN = "header";  (* FIXME legacy *)
     5.9 +
    5.10  val chapterN = "chapter";
    5.11  val sectionN = "section";
    5.12  val subsectionN = "subsection";
    5.13  val subsubsectionN = "subsubsection";
    5.14 +val paragraphN = "paragraph";
    5.15 +val subparagraphN = "subparagraph";
    5.16  val textN = "text";
    5.17  val txtN = "txt";
    5.18  val text_rawN = "text_raw";
    5.19 @@ -74,6 +77,8 @@
    5.20       ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.21       ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.22       ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.23 +     ((paragraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.24 +     ((subparagraphN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.25       ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
    5.26       ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
    5.27       ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
    5.28 @@ -147,6 +152,8 @@
    5.29      Parse.command sectionN ||
    5.30      Parse.command subsectionN ||
    5.31      Parse.command subsubsectionN ||
    5.32 +    Parse.command paragraphN ||
    5.33 +    Parse.command subparagraphN ||
    5.34      Parse.command textN ||
    5.35      Parse.command txtN ||
    5.36      Parse.command text_rawN) --
     6.1 --- a/src/Pure/Thy/thy_header.scala	Sat Oct 17 20:27:12 2015 +0200
     6.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Oct 17 21:15:10 2015 +0200
     6.3 @@ -19,11 +19,14 @@
     6.4  
     6.5    type Keywords = List[(String, Option[Keyword.Spec], Option[String])]
     6.6  
     6.7 -  val HEADER = "header"
     6.8 +  val HEADER = "header"  /* FIXME legacy */
     6.9 +
    6.10    val CHAPTER = "chapter"
    6.11    val SECTION = "section"
    6.12    val SUBSECTION = "subsection"
    6.13    val SUBSUBSECTION = "subsubsection"
    6.14 +  val PARAGRAPH = "paragraph"
    6.15 +  val SUBPARAGRAPH = "subparagraph"
    6.16    val TEXT = "text"
    6.17    val TXT = "txt"
    6.18    val TEXT_RAW = "text_raw"
    6.19 @@ -51,6 +54,8 @@
    6.20        (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    6.21        (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    6.22        (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    6.23 +      (PARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    6.24 +      (SUBPARAGRAPH, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
    6.25        (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    6.26        (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
    6.27        (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
    6.28 @@ -115,6 +120,8 @@
    6.29          command(SECTION) |
    6.30          command(SUBSECTION) |
    6.31          command(SUBSUBSECTION) |
    6.32 +        command(PARAGRAPH) |
    6.33 +        command(SUBPARAGRAPH) |
    6.34          command(TEXT) |
    6.35          command(TXT) |
    6.36          command(TEXT_RAW)) ~
     7.1 --- a/src/Pure/Tools/update_header.scala	Sat Oct 17 20:27:12 2015 +0200
     7.2 +++ b/src/Pure/Tools/update_header.scala	Sat Oct 17 21:15:10 2015 +0200
     7.3 @@ -25,15 +25,19 @@
     7.4  
     7.5    /* command line entry point */
     7.6  
     7.7 +  private val headings =
     7.8 +    Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
     7.9 +
    7.10    def main(args: Array[String])
    7.11    {
    7.12      Command_Line.tool0 {
    7.13        args.toList match {
    7.14          case section :: files =>
    7.15 -          if (!Set("chapter", "section", "subsection", "subsubsection").contains(section))
    7.16 +          if (!headings.contains(section))
    7.17              error("Bad heading command: " + quote(section))
    7.18            files.foreach(file => update_header(section, Path.explode(file)))
    7.19 -        case _ => error("Bad arguments:\n" + cat_lines(args))
    7.20 +        case _ =>
    7.21 +            error("Bad arguments:\n" + cat_lines(args))
    7.22        }
    7.23      }
    7.24    }
     8.1 --- a/src/Pure/pure_syn.ML	Sat Oct 17 20:27:12 2015 +0200
     8.2 +++ b/src/Pure/pure_syn.ML	Sat Oct 17 21:15:10 2015 +0200
     8.3 @@ -34,6 +34,14 @@
     8.4      (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
     8.5  
     8.6  val _ =
     8.7 +  Outer_Syntax.command ("paragraph", @{here}) "paragraph heading"
     8.8 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
     8.9 +
    8.10 +val _ =
    8.11 +  Outer_Syntax.command ("subparagraph", @{here}) "subparagraph heading"
    8.12 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});
    8.13 +
    8.14 +val _ =
    8.15    Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
    8.16      (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
    8.17