uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
authorwenzelm
Thu Nov 13 23:45:15 2014 +0100 (2014-11-13)
changeset 58999ed09ae4ea2d8
parent 58998 6237574c705b
child 59001 44afb337bb92
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;
NEWS
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/First_Order_Logic.thy
src/Doc/Isar_Ref/Framework.thy
src/Doc/Prog_Prove/Isar.thy
src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/Pure.thy
src/Pure/System/options.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_output.ML
src/Pure/pure_syn.ML
     1.1 --- a/NEWS	Thu Nov 13 17:28:11 2014 +0100
     1.2 +++ b/NEWS	Thu Nov 13 23:45:15 2014 +0100
     1.3 @@ -180,13 +180,20 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* Document headings work uniformly via the commands 'chapter',
     1.8 -'section', 'subsection', 'subsubsection' -- in any context, even
     1.9 -before the initial 'theory' command.  Obsolete proof commands 'sect',
    1.10 -'subsect', 'subsubsect' have been discontinued.  The Obsolete 'header'
    1.11 -command is still retained for some time, but should be replaced by
    1.12 -'chapter', 'section' etc. (using "isabelle update_header"). Minor
    1.13 -INCOMPATIBILITY.
    1.14 +* Document markup commands 'chapter', 'section', 'subsection',
    1.15 +'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
    1.16 +context, even before the initial 'theory' command. Obsolete proof
    1.17 +commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been
    1.18 +discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'
    1.19 +instead. The old 'header' command is still retained for some time, but
    1.20 +should be replaced by 'chapter', 'section' etc. (using "isabelle
    1.21 +update_header"). Minor INCOMPATIBILITY.
    1.22 +
    1.23 +* Diagnostic commands and document markup commands within a proof do not
    1.24 +affect the command tag for output. Thus commands like 'thm' are subject
    1.25 +to proof document structure, and no longer "stick out" accidentally.
    1.26 +Commands 'text' and 'txt' merely differ in the LaTeX style, not their
    1.27 +tags. Potential INCOMPATIBILITY in exotic situations.
    1.28  
    1.29  * Official support for "tt" style variants, via \isatt{...} or
    1.30  \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Nov 13 17:28:11 2014 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Nov 13 23:45:15 2014 +0100
     2.3 @@ -26,10 +26,9 @@
     2.4      @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\
     2.5      @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\
     2.6      @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\
     2.7 -    @{command_def "text"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.8 -    @{command_def "text_raw"} & : & @{text "local_theory \<rightarrow> local_theory"} \\[0.5ex]
     2.9 -    @{command_def "txt"} & : & @{text "proof \<rightarrow> proof"} \\
    2.10 -    @{command_def "txt_raw"} & : & @{text "proof \<rightarrow> proof"} \\
    2.11 +    @{command_def "text"} & : & @{text "any \<rightarrow> any"} \\
    2.12 +    @{command_def "txt"} & : & @{text "any \<rightarrow> any"} \\
    2.13 +    @{command_def "text_raw"} & : & @{text "any \<rightarrow> any"} \\
    2.14    \end{matharray}
    2.15  
    2.16    Markup commands provide a structured way to insert text into the
    2.17 @@ -45,9 +44,10 @@
    2.18  
    2.19    @{rail \<open>
    2.20      (@@{command chapter} | @@{command section} | @@{command subsection} |
    2.21 -      @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text}
    2.22 +      @@{command subsubsection} | @@{command text} | @@{command txt})
    2.23 +      @{syntax target}? @{syntax text}
    2.24      ;
    2.25 -    (@@{command text_raw} | @@{command txt} | @@{command txt_raw}) @{syntax text}
    2.26 +    @@{command text_raw} @{syntax text}
    2.27    \<close>}
    2.28  
    2.29    \begin{description}
    2.30 @@ -59,22 +59,22 @@
    2.31    @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},
    2.32    @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}.
    2.33  
    2.34 -  \item @{command text} and @{command txt} specify paragraphs of plain
    2.35 -  text.  This corresponds to a {\LaTeX} environment @{verbatim
    2.36 -  \<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>} etc.
    2.37 +  \item @{command text} and @{command txt} specify paragraphs of plain text.
    2.38 +  This corresponds to a {\LaTeX} environment @{verbatim
    2.39 +  \<open>\begin{isamarkuptext}\<close>} @{text "\<dots>"} @{verbatim \<open>\end{isamarkuptext}\<close>}
    2.40 +  etc.
    2.41  
    2.42 -  \item @{command text_raw} and @{command txt_raw} insert {\LaTeX}
    2.43 -  source into the output, without additional markup.  Thus the full
    2.44 -  range of document manipulations becomes available, at the risk of
    2.45 -  messing up document output.
    2.46 +  \item @{command text_raw} inserts {\LaTeX} source directly into the
    2.47 +  output, without additional markup. Thus the full range of document
    2.48 +  manipulations becomes available, at the risk of messing up document
    2.49 +  output.
    2.50  
    2.51    \end{description}
    2.52  
    2.53 -  Except for @{command "text_raw"} and @{command "txt_raw"}, the text
    2.54 -  passed to any of the above markup commands may refer to formal
    2.55 -  entities via \emph{document antiquotations}, see also
    2.56 -  \secref{sec:antiq}.  These are interpreted in the present theory or
    2.57 -  proof context, or the named @{text "target"}.
    2.58 +  Except for @{command "text_raw"}, the text passed to any of the above
    2.59 +  markup commands may refer to formal entities via \emph{document
    2.60 +  antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
    2.61 +  present theory or proof context, or the named @{text "target"}.
    2.62  
    2.63    \medskip The proof markup commands closely resemble those for theory
    2.64    specifications, but have a different formal status and produce
     3.1 --- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 13 17:28:11 2014 +0100
     3.2 +++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 13 23:45:15 2014 +0100
     3.3 @@ -414,7 +414,7 @@
     3.4  proof -
     3.5  (*>*)
     3.6  
     3.7 -  txt_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
     3.8 +  text_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
     3.9  
    3.10    have "A \<longrightarrow> B"
    3.11    proof
    3.12 @@ -422,12 +422,12 @@
    3.13      show B sorry %noproof
    3.14    qed
    3.15  
    3.16 -  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.17 +  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.18  
    3.19    have "A \<longrightarrow> B" and A sorry %noproof
    3.20    then have B ..
    3.21  
    3.22 -  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.23 +  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.24  
    3.25    have A sorry %noproof
    3.26    then have "A \<or> B" ..
    3.27 @@ -435,7 +435,7 @@
    3.28    have B sorry %noproof
    3.29    then have "A \<or> B" ..
    3.30  
    3.31 -  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.32 +  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.33  
    3.34    have "A \<or> B" sorry %noproof
    3.35    then have C
    3.36 @@ -447,26 +447,26 @@
    3.37      then show C sorry %noproof
    3.38    qed
    3.39  
    3.40 -  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.41 +  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.42  
    3.43    have A and B sorry %noproof
    3.44    then have "A \<and> B" ..
    3.45  
    3.46 -  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.47 +  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.48  
    3.49    have "A \<and> B" sorry %noproof
    3.50    then obtain A and B ..
    3.51  
    3.52 -  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.53 +  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.54  
    3.55    have "\<bottom>" sorry %noproof
    3.56    then have A ..
    3.57  
    3.58 -  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.59 +  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.60  
    3.61    have "\<top>" ..
    3.62  
    3.63 -  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.64 +  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.65  
    3.66    have "\<not> A"
    3.67    proof
    3.68 @@ -474,12 +474,12 @@
    3.69      then show "\<bottom>" sorry %noproof
    3.70    qed
    3.71  
    3.72 -  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.73 +  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.74  
    3.75    have "\<not> A" and A sorry %noproof
    3.76    then have B ..
    3.77  
    3.78 -  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.79 +  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.80  
    3.81    have "\<forall>x. B x"
    3.82    proof
    3.83 @@ -487,24 +487,24 @@
    3.84      show "B x" sorry %noproof
    3.85    qed
    3.86  
    3.87 -  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.88 +  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.89  
    3.90    have "\<forall>x. B x" sorry %noproof
    3.91    then have "B a" ..
    3.92  
    3.93 -  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.94 +  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
    3.95  
    3.96    have "\<exists>x. B x"
    3.97    proof
    3.98      show "B a" sorry %noproof
    3.99    qed
   3.100  
   3.101 -  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
   3.102 +  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
   3.103  
   3.104    have "\<exists>x. B x" sorry %noproof
   3.105    then obtain a where "B a" ..
   3.106  
   3.107 -  txt_raw \<open>\end{minipage}\<close>
   3.108 +  text_raw \<open>\end{minipage}\<close>
   3.109  
   3.110  (*<*)
   3.111  qed
     4.1 --- a/src/Doc/Isar_Ref/Framework.thy	Thu Nov 13 17:28:11 2014 +0100
     4.2 +++ b/src/Doc/Isar_Ref/Framework.thy	Thu Nov 13 23:45:15 2014 +0100
     4.3 @@ -654,31 +654,31 @@
     4.4  theorem True
     4.5  proof
     4.6  (*>*)
     4.7 -  txt_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
     4.8 +  text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
     4.9    {
    4.10      fix x
    4.11      have "B x" sorry %noproof
    4.12    }
    4.13    note \<open>\<And>x. B x\<close>
    4.14 -  txt_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
    4.15 +  text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
    4.16    {
    4.17      assume A
    4.18      have B sorry %noproof
    4.19    }
    4.20    note \<open>A \<Longrightarrow> B\<close>
    4.21 -  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
    4.22 +  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
    4.23    {
    4.24      def x \<equiv> a
    4.25      have "B x" sorry %noproof
    4.26    }
    4.27    note \<open>B a\<close>
    4.28 -  txt_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
    4.29 +  text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
    4.30    {
    4.31      obtain x where "A x" sorry %noproof
    4.32      have B sorry %noproof
    4.33    }
    4.34    note \<open>B\<close>
    4.35 -  txt_raw \<open>\end{minipage}\<close>
    4.36 +  text_raw \<open>\end{minipage}\<close>
    4.37  (*<*)
    4.38  qed
    4.39  (*>*)
    4.40 @@ -819,14 +819,14 @@
    4.41  text_raw \<open>\begingroup\footnotesize\<close>
    4.42  (*<*)notepad begin
    4.43  (*>*)
    4.44 -  txt_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>
    4.45 +  text_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>
    4.46    have "A \<longrightarrow> B"
    4.47    proof
    4.48      assume A
    4.49      show B
    4.50        sorry %noproof
    4.51    qed
    4.52 -  txt_raw \<open>\end{minipage}\quad
    4.53 +  text_raw \<open>\end{minipage}\quad
    4.54  \begin{minipage}[t]{0.06\textwidth}
    4.55  @{text "begin"} \\
    4.56  \\
    4.57 @@ -886,7 +886,7 @@
    4.58      show "C x y" sorry %noproof
    4.59    qed
    4.60  
    4.61 -txt_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
    4.62 +text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
    4.63  
    4.64  (*<*)
    4.65  next
    4.66 @@ -898,7 +898,7 @@
    4.67      show "C x y" sorry %noproof
    4.68    qed
    4.69  
    4.70 -txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
    4.71 +text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
    4.72  
    4.73  (*<*)
    4.74  next
    4.75 @@ -910,7 +910,7 @@
    4.76      show "C x y" sorry
    4.77    qed
    4.78  
    4.79 -txt_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
    4.80 +text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
    4.81  (*<*)
    4.82  next
    4.83  (*>*)
     5.1 --- a/src/Doc/Prog_Prove/Isar.thy	Thu Nov 13 17:28:11 2014 +0100
     5.2 +++ b/src/Doc/Prog_Prove/Isar.thy	Thu Nov 13 23:45:15 2014 +0100
     5.3 @@ -240,12 +240,12 @@
     5.4  show "R"
     5.5  proof cases
     5.6    assume "P"
     5.7 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
     5.8 -  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
     5.9 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.10 +  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.11  next
    5.12    assume "\<not> P"
    5.13 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.14 -  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.15 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.16 +  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.17  qed(*<*)oops(*>*)
    5.18  text_raw {* }
    5.19  \end{minipage}\index{cases@@{text cases}}
    5.20 @@ -254,16 +254,16 @@
    5.21  \isa{%
    5.22  *}
    5.23  (*<*)lemma "R" proof-(*>*)
    5.24 -have "P \<or> Q" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.25 +have "P \<or> Q" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.26  then show "R"
    5.27  proof
    5.28    assume "P"
    5.29 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.30 -  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.31 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.32 +  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.33  next
    5.34    assume "Q"
    5.35 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.36 -  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.37 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.38 +  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.39  qed(*<*)oops(*>*)
    5.40  
    5.41  text_raw {* }
    5.42 @@ -279,12 +279,12 @@
    5.43  show "P \<longleftrightarrow> Q"
    5.44  proof
    5.45    assume "P"
    5.46 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.47 -  show "Q" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
    5.48 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.49 +  show "Q" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
    5.50  next
    5.51    assume "Q"
    5.52 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.53 -  show "P" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
    5.54 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.55 +  show "P" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
    5.56  qed(*<*)qed(*>*)
    5.57  text_raw {* }
    5.58  \medskip
    5.59 @@ -299,8 +299,8 @@
    5.60  show "\<not> P"
    5.61  proof
    5.62    assume "P"
    5.63 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.64 -  show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.65 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.66 +  show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.67  qed(*<*)oops(*>*)
    5.68  
    5.69  text_raw {* }
    5.70 @@ -313,8 +313,8 @@
    5.71  show "P"
    5.72  proof (rule ccontr)
    5.73    assume "\<not>P"
    5.74 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.75 -  show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.76 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.77 +  show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.78  qed(*<*)oops(*>*)
    5.79  
    5.80  text_raw {* }
    5.81 @@ -332,8 +332,8 @@
    5.82  show "\<forall>x. P(x)"
    5.83  proof
    5.84    fix x
    5.85 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.86 -  show "P(x)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.87 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.88 +  show "P(x)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
    5.89  qed(*<*)oops(*>*)
    5.90  
    5.91  text_raw {* }
    5.92 @@ -345,8 +345,8 @@
    5.93  (*<*)lemma "EX x. P(x)" proof-(*>*)
    5.94  show "\<exists>x. P(x)"
    5.95  proof
    5.96 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.97 -  show "P(witness)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
    5.98 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
    5.99 +  show "P(witness)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.100  qed
   5.101  (*<*)oops(*>*)
   5.102  
   5.103 @@ -367,7 +367,7 @@
   5.104  \end{isamarkuptext}%
   5.105  *}
   5.106  (*<*)lemma True proof- assume 1: "EX x. P x"(*>*)
   5.107 -have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)txt_raw{*\ $\dots$\\*}
   5.108 +have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)text_raw{*\ $\dots$\\*}
   5.109  then obtain x where p: "P(x)" by blast
   5.110  (*<*)oops(*>*)
   5.111  text{*
   5.112 @@ -401,9 +401,9 @@
   5.113  (*<*)lemma "A = (B::'a set)" proof-(*>*)
   5.114  show "A = B"
   5.115  proof
   5.116 -  show "A \<subseteq> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.117 +  show "A \<subseteq> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.118  next
   5.119 -  show "B \<subseteq> A" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.120 +  show "B \<subseteq> A" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.121  qed(*<*)qed(*>*)
   5.122  
   5.123  text_raw {* }
   5.124 @@ -417,8 +417,8 @@
   5.125  proof
   5.126    fix x
   5.127    assume "x \<in> A"
   5.128 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.129 -  show "x \<in> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.130 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.131 +  show "x \<in> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.132  qed(*<*)qed(*>*)
   5.133  
   5.134  text_raw {* }
   5.135 @@ -444,12 +444,12 @@
   5.136  show "formula\<^sub>1 \<longleftrightarrow> formula\<^sub>2" (is "?L \<longleftrightarrow> ?R")
   5.137  proof
   5.138    assume "?L"
   5.139 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.140 -  show "?R" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
   5.141 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.142 +  show "?R" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
   5.143  next
   5.144    assume "?R"
   5.145 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.146 -  show "?L" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
   5.147 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.148 +  show "?L" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
   5.149  qed(*<*)qed(*>*)
   5.150  
   5.151  text{* Instead of duplicating @{text"formula\<^sub>i"} in the text, we introduce
   5.152 @@ -462,8 +462,8 @@
   5.153  
   5.154  lemma "formula"
   5.155  proof -
   5.156 -  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.157 -  show ?thesis (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
   5.158 +  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
   5.159 +  show ?thesis (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
   5.160  qed
   5.161  
   5.162  text{* 
   5.163 @@ -511,12 +511,12 @@
   5.164  \isa{%
   5.165  *}
   5.166  (*<*)lemma "P" proof-(*>*)
   5.167 -have "P\<^sub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.168 -moreover have "P\<^sub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.169 +have "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.170 +moreover have "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.171  moreover
   5.172 -txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*)
   5.173 -moreover have "P\<^sub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.174 -ultimately have "P"  (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.175 +text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*)
   5.176 +moreover have "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.177 +ultimately have "P"  (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.178  (*<*)oops(*>*)
   5.179  
   5.180  text_raw {* }
   5.181 @@ -527,12 +527,12 @@
   5.182  \isa{%
   5.183  *}
   5.184  (*<*)lemma "P" proof-(*>*)
   5.185 -have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.186 -have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$*}
   5.187 -txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*}
   5.188 -have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.189 -from lab\<^sub>1 lab\<^sub>2 txt_raw{*\ $\dots$\\*}
   5.190 -have "P"  (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.191 +have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.192 +have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$*}
   5.193 +text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}
   5.194 +have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.195 +from lab\<^sub>1 lab\<^sub>2 text_raw{*\ $\dots$\\*}
   5.196 +have "P"  (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.197  (*<*)oops(*>*)
   5.198  
   5.199  text_raw {* }
   5.200 @@ -733,12 +733,12 @@
   5.201  show "P(n)"
   5.202  proof (induction n)
   5.203    case 0
   5.204 -  txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
   5.205 -  show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
   5.206 +  text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
   5.207 +  show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
   5.208  next
   5.209    case (Suc n)
   5.210 -  txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
   5.211 -  show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
   5.212 +  text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
   5.213 +  show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
   5.214  qed(*<*)qed(*>*)
   5.215  
   5.216  text_raw {* }
   5.217 @@ -904,18 +904,18 @@
   5.218  show "I x \<Longrightarrow> P x"
   5.219  proof(induction rule: I.induct)
   5.220    case rule\<^sub>1
   5.221 -  txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
   5.222 -  show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.223 +  text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
   5.224 +  show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.225  next
   5.226 -  txt_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
   5.227 +  text_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
   5.228  (*<*)
   5.229    case rule\<^sub>2
   5.230    show ?case sorry
   5.231  (*>*)
   5.232  next
   5.233    case rule\<^sub>n
   5.234 -  txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
   5.235 -  show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
   5.236 +  text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
   5.237 +  show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
   5.238  qed(*<*)qed(*>*)
   5.239  
   5.240  text{*
     6.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Thu Nov 13 17:28:11 2014 +0100
     6.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Thu Nov 13 23:45:15 2014 +0100
     6.3 @@ -121,7 +121,7 @@
     6.4            unfolding H'_def sum_def lin_def by blast
     6.5          
     6.6          have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
     6.7 -        proof (rule decomp_H') txt_raw \<open>\label{decomp-H-use}\<close>
     6.8 +        proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>
     6.9            from HE y1 y2 show "y1 + y2 \<in> H"
    6.10              by (rule subspace.add_closed)
    6.11            from x0 and HE y y1 y2
     7.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Thu Nov 13 17:28:11 2014 +0100
     7.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Nov 13 23:45:15 2014 +0100
     7.3 @@ -179,7 +179,7 @@
     7.4  ML {*
     7.5    Outer_Syntax.command
     7.6      @{command_spec "text_cartouche"} ""
     7.7 -    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.local_theory_markup)
     7.8 +    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.document_command)
     7.9  *}
    7.10  
    7.11  text_cartouche
     8.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Nov 13 17:28:11 2014 +0100
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 13 23:45:15 2014 +0100
     8.3 @@ -7,30 +7,6 @@
     8.4  structure Isar_Syn: sig end =
     8.5  struct
     8.6  
     8.7 -(** markup commands **)
     8.8 -
     8.9 -val _ =
    8.10 -  Outer_Syntax.markup_command Outer_Syntax.Markup_Env
    8.11 -    @{command_spec "text"} "formal comment (theory)"
    8.12 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup);
    8.13 -
    8.14 -val _ =
    8.15 -  Outer_Syntax.markup_command Outer_Syntax.Verbatim
    8.16 -    @{command_spec "text_raw"} "raw document preparation text"
    8.17 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup);
    8.18 -
    8.19 -val _ =
    8.20 -  Outer_Syntax.markup_command Outer_Syntax.Markup_Env
    8.21 -    @{command_spec "txt"} "formal comment (proof)"
    8.22 -    (Parse.document_source >> Thy_Output.proof_markup);
    8.23 -
    8.24 -val _ =
    8.25 -  Outer_Syntax.markup_command Outer_Syntax.Verbatim
    8.26 -    @{command_spec "txt_raw"} "raw document preparation text (proof)"
    8.27 -    (Parse.document_source >> Thy_Output.proof_markup);
    8.28 -
    8.29 -
    8.30 -
    8.31  (** theory commands **)
    8.32  
    8.33  (* sorts *)
     9.1 --- a/src/Pure/Isar/keyword.ML	Thu Nov 13 17:28:11 2014 +0100
     9.2 +++ b/src/Pure/Isar/keyword.ML	Thu Nov 13 23:45:15 2014 +0100
     9.3 @@ -7,7 +7,9 @@
     9.4  signature KEYWORD =
     9.5  sig
     9.6    val diag: string
     9.7 -  val heading: string
     9.8 +  val document_heading: string
     9.9 +  val document_body: string
    9.10 +  val document_raw: string
    9.11    val thy_begin: string
    9.12    val thy_end: string
    9.13    val thy_decl: string
    9.14 @@ -41,8 +43,11 @@
    9.15    val is_literal: keywords -> string -> bool
    9.16    val command_files: keywords -> string -> Path.T -> Path.T list
    9.17    val command_tags: keywords -> string -> string list
    9.18 +  val is_vacuous: keywords -> string -> bool
    9.19    val is_diag: keywords -> string -> bool
    9.20 -  val is_heading: keywords -> string -> bool
    9.21 +  val is_document_heading: keywords -> string -> bool
    9.22 +  val is_document_body: keywords -> string -> bool
    9.23 +  val is_document_raw: keywords -> string -> bool
    9.24    val is_theory_begin: keywords -> string -> bool
    9.25    val is_theory_load: keywords -> string -> bool
    9.26    val is_theory: keywords -> string -> bool
    9.27 @@ -64,7 +69,9 @@
    9.28  (* kinds *)
    9.29  
    9.30  val diag = "diag";
    9.31 -val heading = "heading";
    9.32 +val document_heading = "document_heading";
    9.33 +val document_body = "document_body";
    9.34 +val document_raw = "document_raw";
    9.35  val thy_begin = "thy_begin";
    9.36  val thy_end = "thy_end";
    9.37  val thy_decl = "thy_decl";
    9.38 @@ -87,9 +94,9 @@
    9.39  val prf_script = "prf_script";
    9.40  
    9.41  val kinds =
    9.42 -  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
    9.43 -    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
    9.44 -    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    9.45 +  [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
    9.46 +    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open,
    9.47 +    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    9.48  
    9.49  
    9.50  (* specifications *)
    9.51 @@ -196,9 +203,14 @@
    9.52        | SOME {kind, ...} => Symtab.defined tab kind);
    9.53    in pred end;
    9.54  
    9.55 +val is_vacuous = command_category [diag, document_heading, document_body, document_raw];
    9.56 +
    9.57  val is_diag = command_category [diag];
    9.58  
    9.59 -val is_heading = command_category [heading];
    9.60 +val is_document_heading = command_category [document_heading];
    9.61 +val is_document_body = command_category [document_body];
    9.62 +val is_document_raw = command_category [document_raw];
    9.63 +val is_document = command_category [document_heading, document_body, document_raw];
    9.64  
    9.65  val is_theory_begin = command_category [thy_begin];
    9.66  
    9.67 @@ -215,8 +227,8 @@
    9.68      prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    9.69  
    9.70  val is_proof_body = command_category
    9.71 -  [diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm,
    9.72 -    prf_asm_goal, prf_asm_goal_script, prf_script];
    9.73 +  [diag, document_heading, document_body, document_raw, prf_block, prf_open, prf_close,
    9.74 +    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    9.75  
    9.76  val is_theory_goal = command_category [thy_goal];
    9.77  val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
    10.1 --- a/src/Pure/Isar/keyword.scala	Thu Nov 13 17:28:11 2014 +0100
    10.2 +++ b/src/Pure/Isar/keyword.scala	Thu Nov 13 23:45:15 2014 +0100
    10.3 @@ -14,7 +14,9 @@
    10.4    /* kinds */
    10.5  
    10.6    val DIAG = "diag"
    10.7 -  val HEADING = "heading"
    10.8 +  val DOCUMENT_HEADING = "document_heading"
    10.9 +  val DOCUMENT_BODY = "document_body"
   10.10 +  val DOCUMENT_RAW = "document_raw"
   10.11    val THY_BEGIN = "thy_begin"
   10.12    val THY_END = "thy_end"
   10.13    val THY_DECL = "thy_decl"
   10.14 @@ -39,9 +41,14 @@
   10.15  
   10.16    /* categories */
   10.17  
   10.18 +  val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
   10.19 +
   10.20    val diag = Set(DIAG)
   10.21  
   10.22 -  val heading = Set(HEADING)
   10.23 +  val document_heading = Set(DOCUMENT_HEADING)
   10.24 +  val document_body = Set(DOCUMENT_BODY)
   10.25 +  val document_raw = Set(DOCUMENT_RAW)
   10.26 +  val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
   10.27  
   10.28    val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
   10.29  
   10.30 @@ -54,8 +61,8 @@
   10.31        PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   10.32  
   10.33    val proof_body =
   10.34 -    Set(DIAG, HEADING, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM,
   10.35 -      PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   10.36 +    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
   10.37 +      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   10.38  
   10.39    val theory_goal = Set(THY_GOAL)
   10.40    val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
    11.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Nov 13 17:28:11 2014 +0100
    11.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Nov 13 23:45:15 2014 +0100
    11.3 @@ -6,15 +6,11 @@
    11.4  
    11.5  signature OUTER_SYNTAX =
    11.6  sig
    11.7 -  datatype markup = Markup | Markup_Env | Verbatim
    11.8 -  val is_markup: theory -> markup -> string -> bool
    11.9    val help: theory -> string list -> unit
   11.10    val print_commands: theory -> unit
   11.11    type command_spec = string * Position.T
   11.12    val command: command_spec -> string ->
   11.13      (Toplevel.transition -> Toplevel.transition) parser -> unit
   11.14 -  val markup_command: markup -> command_spec -> string ->
   11.15 -    (Toplevel.transition -> Toplevel.transition) parser -> unit
   11.16    val local_theory': command_spec -> string ->
   11.17      (bool -> local_theory -> local_theory) parser -> unit
   11.18    val local_theory: command_spec -> string ->
   11.19 @@ -47,19 +43,16 @@
   11.20  
   11.21  (* command parsers *)
   11.22  
   11.23 -datatype markup = Markup | Markup_Env | Verbatim;
   11.24 -
   11.25  datatype command = Command of
   11.26   {comment: string,
   11.27 -  markup: markup option,
   11.28    parse: (Toplevel.transition -> Toplevel.transition) parser,
   11.29    pos: Position.T,
   11.30    id: serial};
   11.31  
   11.32  fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2;
   11.33  
   11.34 -fun new_command comment markup parse pos =
   11.35 -  Command {comment = comment, markup = markup, parse = parse, pos = pos, id = serial ()};
   11.36 +fun new_command comment parse pos =
   11.37 +  Command {comment = comment, parse = parse, pos = pos, id = serial ()};
   11.38  
   11.39  fun command_pos (Command {pos, ...}) = pos;
   11.40  
   11.41 @@ -74,45 +67,22 @@
   11.42          command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   11.43  
   11.44  
   11.45 -(* type syntax *)
   11.46 -
   11.47 -datatype syntax = Syntax of
   11.48 - {commands: command Symtab.table,
   11.49 -  markups: (string * markup) list};
   11.50 -
   11.51 -fun make_syntax (commands, markups) =
   11.52 -  Syntax {commands = commands, markups = markups};
   11.53 +(* theory data *)
   11.54  
   11.55  structure Data = Theory_Data
   11.56  (
   11.57 -  type T = syntax;
   11.58 -  val empty = make_syntax (Symtab.empty, []);
   11.59 +  type T = command Symtab.table;
   11.60 +  val empty = Symtab.empty;
   11.61    val extend = I;
   11.62 -  fun merge (Syntax {commands = commands1, markups = markups1},
   11.63 -      Syntax {commands = commands2, markups = markups2}) =
   11.64 -    let
   11.65 -      val commands' = (commands1, commands2)
   11.66 -        |> Symtab.join (fn name => fn (cmd1, cmd2) =>
   11.67 -          if eq_command (cmd1, cmd2) then raise Symtab.SAME
   11.68 -          else err_dup_command name [command_pos cmd1, command_pos cmd2]);
   11.69 -      val markups' = AList.merge (op =) (K true) (markups1, markups2);
   11.70 -    in make_syntax (commands', markups') end;
   11.71 +  fun merge data : T =
   11.72 +    data |> Symtab.join (fn name => fn (cmd1, cmd2) =>
   11.73 +      if eq_command (cmd1, cmd2) then raise Symtab.SAME
   11.74 +      else err_dup_command name [command_pos cmd1, command_pos cmd2]);
   11.75  );
   11.76  
   11.77 -
   11.78 -(* inspect syntax *)
   11.79 -
   11.80 -val get_syntax = Data.get;
   11.81 -
   11.82 -val dest_commands =
   11.83 -  get_syntax #> (fn Syntax {commands, ...} => commands |> Symtab.dest |> sort_wrt #1);
   11.84 -
   11.85 -val lookup_commands =
   11.86 -  get_syntax #> (fn Syntax {commands, ...} => Symtab.lookup commands);
   11.87 -
   11.88 -val is_markup =
   11.89 -  get_syntax #> (fn Syntax {markups, ...} => fn kind => fn name =>
   11.90 -    AList.lookup (op =) markups name = SOME kind);
   11.91 +val get_commands = Data.get;
   11.92 +val dest_commands = get_commands #> Symtab.dest #> sort_wrt #1;
   11.93 +val lookup_commands = Symtab.lookup o get_commands;
   11.94  
   11.95  fun help thy pats =
   11.96    dest_commands thy
   11.97 @@ -132,36 +102,28 @@
   11.98    end;
   11.99  
  11.100  
  11.101 -(* build syntax *)
  11.102 +(* maintain commands *)
  11.103  
  11.104 -fun add_command name cmd thy = thy |> Data.map (fn Syntax {commands, ...} =>
  11.105 +fun add_command name cmd thy =
  11.106    let
  11.107 -    val keywords = Thy_Header.get_keywords thy;
  11.108      val _ =
  11.109 -      Keyword.is_command keywords name orelse
  11.110 +      Keyword.is_command (Thy_Header.get_keywords thy) name orelse
  11.111          err_command "Undeclared outer syntax command " name [command_pos cmd];
  11.112 -
  11.113      val _ =
  11.114 -      (case Symtab.lookup commands name of
  11.115 +      (case lookup_commands thy name of
  11.116          NONE => ()
  11.117        | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
  11.118 -
  11.119      val _ =
  11.120        Context_Position.report_generic (ML_Context.the_generic_context ())
  11.121          (command_pos cmd) (command_markup true (name, cmd));
  11.122 -
  11.123 -    val commands' = Symtab.update (name, cmd) commands;
  11.124 -    val markups' =
  11.125 -      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
  11.126 -        commands' [];
  11.127 -  in make_syntax (commands', markups') end);
  11.128 +  in Data.map (Symtab.update (name, cmd)) thy end;
  11.129  
  11.130  val _ = Theory.setup (Theory.at_end (fn thy =>
  11.131    let
  11.132 -    val keywords = Thy_Header.get_keywords thy;
  11.133 -    val major = Keyword.major_keywords keywords;
  11.134 +    val command_keywords =
  11.135 +      Scan.dest_lexicon (Keyword.major_keywords (Thy_Header.get_keywords thy));
  11.136      val _ =
  11.137 -      (case subtract (op =) (map #1 (dest_commands thy)) (Scan.dest_lexicon major) of
  11.138 +      (case subtract (op =) (map #1 (dest_commands thy)) command_keywords of
  11.139          [] => ()
  11.140        | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
  11.141    in NONE end));
  11.142 @@ -172,10 +134,7 @@
  11.143  type command_spec = string * Position.T;
  11.144  
  11.145  fun command (name, pos) comment parse =
  11.146 -  Theory.setup (add_command name (new_command comment NONE parse pos));
  11.147 -
  11.148 -fun markup_command markup (name, pos) comment parse =
  11.149 -  Theory.setup (add_command name (new_command comment (SOME markup) parse pos));
  11.150 +  Theory.setup (add_command name (new_command comment parse pos));
  11.151  
  11.152  fun local_theory_command trans command_spec comment parse =
  11.153    command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));
    12.1 --- a/src/Pure/Isar/toplevel.ML	Thu Nov 13 17:28:11 2014 +0100
    12.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Nov 13 23:45:15 2014 +0100
    12.3 @@ -65,7 +65,6 @@
    12.4    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    12.5    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    12.6    val forget_proof: bool -> transition -> transition
    12.7 -  val present_proof: (state -> unit) -> transition -> transition
    12.8    val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    12.9    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   12.10    val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   12.11 @@ -498,11 +497,6 @@
   12.12      | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
   12.13      | _ => raise UNDEF));
   12.14  
   12.15 -val present_proof = present_transaction (fn _ =>
   12.16 -  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
   12.17 -    | skip as Skipped_Proof _ => skip
   12.18 -    | _ => raise UNDEF));
   12.19 -
   12.20  fun proofs' f = transaction (fn int =>
   12.21    (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
   12.22      | skip as Skipped_Proof _ => skip
    13.1 --- a/src/Pure/Pure.thy	Thu Nov 13 17:28:11 2014 +0100
    13.2 +++ b/src/Pure/Pure.thy	Thu Nov 13 23:45:15 2014 +0100
    13.3 @@ -12,8 +12,8 @@
    13.4      "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    13.5      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
    13.6      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
    13.7 -  and "text" "text_raw" :: thy_decl
    13.8 -  and "txt" "txt_raw" :: prf_decl % "proof"
    13.9 +  and "text" "txt" :: document_body
   13.10 +  and "text_raw" :: document_raw
   13.11    and "default_sort" :: thy_decl == ""
   13.12    and "typedecl" "type_synonym" "nonterminal" "judgment"
   13.13      "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
    14.1 --- a/src/Pure/System/options.scala	Thu Nov 13 17:28:11 2014 +0100
    14.2 +++ b/src/Pure/System/options.scala	Thu Nov 13 23:45:15 2014 +0100
    14.3 @@ -76,7 +76,7 @@
    14.4  
    14.5    lazy val options_syntax =
    14.6      Outer_Syntax.init() + ":" + "=" + "--" +
    14.7 -      (SECTION, Keyword.HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
    14.8 +      (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
    14.9  
   14.10    lazy val prefs_syntax = Outer_Syntax.init() + "="
   14.11  
    15.1 --- a/src/Pure/Thy/thy_header.ML	Thu Nov 13 17:28:11 2014 +0100
    15.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Nov 13 23:45:15 2014 +0100
    15.3 @@ -46,6 +46,9 @@
    15.4  val sectionN = "section";
    15.5  val subsectionN = "subsection";
    15.6  val subsubsectionN = "subsubsection";
    15.7 +val textN = "text";
    15.8 +val txtN = "txt";
    15.9 +val text_rawN = "text_raw";
   15.10  
   15.11  val theoryN = "theory";
   15.12  val importsN = "imports";
   15.13 @@ -65,11 +68,14 @@
   15.14       (beginN, NONE),
   15.15       (importsN, NONE),
   15.16       (keywordsN, NONE),
   15.17 -     (headerN, SOME ((Keyword.heading, []), [])),
   15.18 -     (chapterN, SOME ((Keyword.heading, []), [])),
   15.19 -     (sectionN, SOME ((Keyword.heading, []), [])),
   15.20 -     (subsectionN, SOME ((Keyword.heading, []), [])),
   15.21 -     (subsubsectionN, SOME ((Keyword.heading, []), [])),
   15.22 +     (headerN, SOME ((Keyword.document_heading, []), [])),
   15.23 +     (chapterN, SOME ((Keyword.document_heading, []), [])),
   15.24 +     (sectionN, SOME ((Keyword.document_heading, []), [])),
   15.25 +     (subsectionN, SOME ((Keyword.document_heading, []), [])),
   15.26 +     (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
   15.27 +     (textN, SOME ((Keyword.document_body, []), [])),
   15.28 +     (txtN, SOME ((Keyword.document_body, []), [])),
   15.29 +     (text_rawN, SOME ((Keyword.document_raw, []), [])),
   15.30       (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
   15.31       ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
   15.32  
   15.33 @@ -138,7 +144,10 @@
   15.34      Parse.command chapterN ||
   15.35      Parse.command sectionN ||
   15.36      Parse.command subsectionN ||
   15.37 -    Parse.command subsubsectionN) --
   15.38 +    Parse.command subsubsectionN ||
   15.39 +    Parse.command textN ||
   15.40 +    Parse.command txtN ||
   15.41 +    Parse.command text_rawN) --
   15.42    Parse.tags -- Parse.!!! Parse.document_source;
   15.43  
   15.44  val header =
    16.1 --- a/src/Pure/Thy/thy_header.scala	Thu Nov 13 17:28:11 2014 +0100
    16.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Nov 13 23:45:15 2014 +0100
    16.3 @@ -24,6 +24,9 @@
    16.4    val SECTION = "section"
    16.5    val SUBSECTION = "subsection"
    16.6    val SUBSUBSECTION = "subsubsection"
    16.7 +  val TEXT = "text"
    16.8 +  val TXT = "txt"
    16.9 +  val TEXT_RAW = "text_raw"
   16.10  
   16.11    val THEORY = "theory"
   16.12    val IMPORTS = "imports"
   16.13 @@ -43,11 +46,14 @@
   16.14        (BEGIN, None, None),
   16.15        (IMPORTS, None, None),
   16.16        (KEYWORDS, None, None),
   16.17 -      (HEADER, Some(((Keyword.HEADING, Nil), Nil)), None),
   16.18 -      (CHAPTER, Some(((Keyword.HEADING, Nil), Nil)), None),
   16.19 -      (SECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
   16.20 -      (SUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
   16.21 -      (SUBSUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
   16.22 +      (HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   16.23 +      (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   16.24 +      (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   16.25 +      (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   16.26 +      (SUBSUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   16.27 +      (TEXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
   16.28 +      (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
   16.29 +      (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
   16.30        (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
   16.31        ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
   16.32  
   16.33 @@ -110,7 +116,10 @@
   16.34          command(CHAPTER) |
   16.35          command(SECTION) |
   16.36          command(SUBSECTION) |
   16.37 -        command(SUBSUBSECTION)) ~
   16.38 +        command(SUBSUBSECTION) |
   16.39 +        command(TEXT) |
   16.40 +        command(TXT) |
   16.41 +        command(TEXT_RAW)) ~
   16.42        tags ~! document_source
   16.43  
   16.44      (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    17.1 --- a/src/Pure/Thy/thy_output.ML	Thu Nov 13 17:28:11 2014 +0100
    17.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Nov 13 23:45:15 2014 +0100
    17.3 @@ -33,11 +33,8 @@
    17.4      Token.src -> 'a list -> Pretty.T list
    17.5    val output: Proof.context -> Pretty.T list -> string
    17.6    val verbatim_text: Proof.context -> string -> string
    17.7 -  val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
    17.8 -    Toplevel.transition -> Toplevel.transition
    17.9 -  val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   17.10 -  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   17.11 -  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
   17.12 +  val old_header_command: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   17.13 +  val document_command: (xstring * Position.T) option * Symbol_Pos.source ->
   17.14      Toplevel.transition -> Toplevel.transition
   17.15  end;
   17.16  
   17.17 @@ -285,22 +282,30 @@
   17.18      val (tag, tags) = tag_stack;
   17.19      val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
   17.20  
   17.21 +    val nesting = Toplevel.level state' - Toplevel.level state;
   17.22 +
   17.23      val active_tag' =
   17.24        if is_some tag' then tag'
   17.25        else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
   17.26 -      else try hd (Keyword.command_tags keywords cmd_name);
   17.27 +      else
   17.28 +        (case Keyword.command_tags keywords cmd_name of
   17.29 +          default_tag :: _ => SOME default_tag
   17.30 +        | [] =>
   17.31 +            if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
   17.32 +            then active_tag
   17.33 +            else NONE);
   17.34 +
   17.35      val edge = (active_tag, active_tag');
   17.36  
   17.37      val newline' =
   17.38        if is_none active_tag' then span_newline else newline;
   17.39  
   17.40 -    val nesting = Toplevel.level state' - Toplevel.level state;
   17.41      val tag_stack' =
   17.42        if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
   17.43        else if nesting >= 0 then (tag', replicate nesting tag @ tags)
   17.44        else
   17.45          (case drop (~ nesting - 1) tags of
   17.46 -          tgs :: tgss => (tgs, tgss)
   17.47 +          tg :: tgs => (tg, tgs)
   17.48          | [] => err_bad_nesting (Position.here cmd_pos));
   17.49  
   17.50      val buffer' =
   17.51 @@ -359,7 +364,6 @@
   17.52  fun present_thy thy command_results toks =
   17.53    let
   17.54      val keywords = Thy_Header.get_keywords thy;
   17.55 -    val is_markup = Outer_Syntax.is_markup thy;
   17.56  
   17.57  
   17.58      (* tokens *)
   17.59 @@ -367,9 +371,10 @@
   17.60      val ignored = Scan.state --| ignore
   17.61        >> (fn d => (NONE, (NoToken, ("", d))));
   17.62  
   17.63 -    fun markup mark mk flag = Scan.peek (fn d =>
   17.64 +    fun markup pred mk flag = Scan.peek (fn d =>
   17.65        improper |--
   17.66 -        Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
   17.67 +        Parse.position (Scan.one (fn tok =>
   17.68 +          Token.is_command tok andalso pred keywords (Token.content_of tok))) --
   17.69        Scan.repeat tag --
   17.70        Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
   17.71        >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) =>
   17.72 @@ -392,9 +397,9 @@
   17.73  
   17.74      val token =
   17.75        ignored ||
   17.76 -      markup Outer_Syntax.Markup MarkupToken Latex.markup_true ||
   17.77 -      markup Outer_Syntax.Markup_Env MarkupEnvToken Latex.markup_true ||
   17.78 -      markup Outer_Syntax.Verbatim (VerbatimToken o #2) "" ||
   17.79 +      markup Keyword.is_document_heading MarkupToken Latex.markup_true ||
   17.80 +      markup Keyword.is_document_body MarkupEnvToken Latex.markup_true ||
   17.81 +      markup Keyword.is_document_raw (VerbatimToken o #2) "" ||
   17.82        command || cmt || other;
   17.83  
   17.84  
   17.85 @@ -702,27 +707,21 @@
   17.86  
   17.87  
   17.88  
   17.89 -(** markup commands **)
   17.90 -
   17.91 -fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
   17.92 -val proof_markup = Toplevel.present_proof o check_text;
   17.93 +(** document commands **)
   17.94  
   17.95 -fun reject_target NONE = ()
   17.96 -  | reject_target (SOME (_, pos)) =
   17.97 -      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
   17.98 -
   17.99 -fun header_markup txt =
  17.100 +fun old_header_command txt =
  17.101    Toplevel.keep (fn state =>
  17.102      if Toplevel.is_toplevel state then
  17.103       (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
  17.104        check_text txt state)
  17.105      else raise Toplevel.UNDEF);
  17.106  
  17.107 -fun heading_markup (loc, txt) =
  17.108 +fun document_command (loc, txt) =
  17.109    Toplevel.keep (fn state =>
  17.110 -    if Toplevel.is_toplevel state then (reject_target loc; check_text txt state)
  17.111 -    else raise Toplevel.UNDEF) o
  17.112 -  local_theory_markup (loc, txt) o
  17.113 -  Toplevel.present_proof (fn state => (reject_target loc; check_text txt state));
  17.114 +    (case loc of
  17.115 +      NONE => check_text txt state
  17.116 +    | SOME (_, pos) =>
  17.117 +        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
  17.118 +  Toplevel.present_local_theory loc (check_text txt);
  17.119  
  17.120  end;
    18.1 --- a/src/Pure/pure_syn.ML	Thu Nov 13 17:28:11 2014 +0100
    18.2 +++ b/src/Pure/pure_syn.ML	Thu Nov 13 23:45:15 2014 +0100
    18.3 @@ -8,24 +8,36 @@
    18.4  struct
    18.5  
    18.6  val _ =
    18.7 -  Outer_Syntax.markup_command Outer_Syntax.Markup ("header", @{here}) "theory header"
    18.8 -    (Parse.document_source >> Thy_Output.header_markup);
    18.9 +  Outer_Syntax.command ("header", @{here}) "theory header"
   18.10 +    (Parse.document_source >> Thy_Output.old_header_command);
   18.11  
   18.12  val _ =
   18.13 -  Outer_Syntax.markup_command Outer_Syntax.Markup ("chapter", @{here}) "chapter heading"
   18.14 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   18.15 +  Outer_Syntax.command ("chapter", @{here}) "chapter heading"
   18.16 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
   18.17 +
   18.18 +val _ =
   18.19 +  Outer_Syntax.command ("section", @{here}) "section heading"
   18.20 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
   18.21  
   18.22  val _ =
   18.23 -  Outer_Syntax.markup_command Outer_Syntax.Markup ("section", @{here}) "section heading"
   18.24 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   18.25 +  Outer_Syntax.command ("subsection", @{here}) "subsection heading"
   18.26 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
   18.27 +
   18.28 +val _ =
   18.29 +  Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
   18.30 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
   18.31  
   18.32  val _ =
   18.33 -  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsection", @{here}) "subsection heading"
   18.34 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   18.35 +  Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
   18.36 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
   18.37  
   18.38  val _ =
   18.39 -  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsubsection", @{here}) "subsubsection heading"
   18.40 -    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
   18.41 +  Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
   18.42 +    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
   18.43 +
   18.44 +val _ =
   18.45 +  Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
   18.46 +    (Parse.document_source >> K (Toplevel.imperative I));
   18.47  
   18.48  val _ =
   18.49    Outer_Syntax.command ("theory", @{here}) "begin theory"