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;

--- a/NEWS	Thu Nov 13 17:28:11 2014 +0100
+++ b/NEWS	Thu Nov 13 23:45:15 2014 +0100
@@ -180,13 +180,20 @@
 
 *** Document preparation ***
 
-* Document headings work uniformly via the commands 'chapter',
-'section', 'subsection', 'subsubsection' -- in any context, even
-before the initial 'theory' command.  Obsolete proof commands 'sect',
-'subsect', 'subsubsect' have been discontinued.  The Obsolete 'header'
-command is still retained for some time, but should be replaced by
-'chapter', 'section' etc. (using "isabelle update_header"). Minor
-INCOMPATIBILITY.
+* Document markup commands 'chapter', 'section', 'subsection',
+'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
+context, even before the initial 'theory' command. Obsolete proof
+commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been
+discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'
+instead. The old 'header' command is still retained for some time, but
+should be replaced by 'chapter', 'section' etc. (using "isabelle
+update_header"). Minor INCOMPATIBILITY.
+
+* Diagnostic commands and document markup commands within a proof do not
+affect the command tag for output. Thus commands like 'thm' are subject
+to proof document structure, and no longer "stick out" accidentally.
+Commands 'text' and 'txt' merely differ in the LaTeX style, not their
+tags. Potential INCOMPATIBILITY in exotic situations.
 
 * Official support for "tt" style variants, via \isatt{...} or
 \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or

--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Nov 13 23:45:15 2014 +0100
@@ -26,10 +26,9 @@
     @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\
     @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\
     @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\
-    @{command_def "text"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "text_raw"} & : & @{text "local_theory \<rightarrow> local_theory"} \\[0.5ex]
-    @{command_def "txt"} & : & @{text "proof \<rightarrow> proof"} \\
-    @{command_def "txt_raw"} & : & @{text "proof \<rightarrow> proof"} \\
+    @{command_def "text"} & : & @{text "any \<rightarrow> any"} \\
+    @{command_def "txt"} & : & @{text "any \<rightarrow> any"} \\
+    @{command_def "text_raw"} & : & @{text "any \<rightarrow> any"} \\
   \end{matharray}
 
   Markup commands provide a structured way to insert text into the
@@ -45,9 +44,10 @@
 
   @{rail \<open>
     (@@{command chapter} | @@{command section} | @@{command subsection} |
-      @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text}
+      @@{command subsubsection} | @@{command text} | @@{command txt})
+      @{syntax target}? @{syntax text}
     ;
-    (@@{command text_raw} | @@{command txt} | @@{command txt_raw}) @{syntax text}
+    @@{command text_raw} @{syntax text}
   \<close>}
 
   \begin{description}
@@ -59,22 +59,22 @@
   @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},
   @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}.
 
-  \item @{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.
+  \item @{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.
 
-  \item @{command text_raw} and @{command txt_raw} insert {\LaTeX}
-  source into the output, without additional markup.  Thus the full
-  range of document manipulations becomes available, at the risk of
-  messing up document output.
+  \item @{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.
 
   \end{description}
 
-  Except for @{command "text_raw"} and @{command "txt_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, or the named @{text "target"}.
+  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, or the named @{text "target"}.
 
   \medskip The proof markup commands closely resemble those for theory
   specifications, but have a different formal status and produce

--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Thu Nov 13 23:45:15 2014 +0100
@@ -414,7 +414,7 @@
 proof -
 (*>*)
 
-  txt_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "A \<longrightarrow> B"
   proof
@@ -422,12 +422,12 @@
     show B sorry %noproof
   qed
 
-  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "A \<longrightarrow> B" and A sorry %noproof
   then have B ..
 
-  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have A sorry %noproof
   then have "A \<or> B" ..
@@ -435,7 +435,7 @@
   have B sorry %noproof
   then have "A \<or> B" ..
 
-  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "A \<or> B" sorry %noproof
   then have C
@@ -447,26 +447,26 @@
     then show C sorry %noproof
   qed
 
-  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have A and B sorry %noproof
   then have "A \<and> B" ..
 
-  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "A \<and> B" sorry %noproof
   then obtain A and B ..
 
-  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<bottom>" sorry %noproof
   then have A ..
 
-  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<top>" ..
 
-  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<not> A"
   proof
@@ -474,12 +474,12 @@
     then show "\<bottom>" sorry %noproof
   qed
 
-  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<not> A" and A sorry %noproof
   then have B ..
 
-  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<forall>x. B x"
   proof
@@ -487,24 +487,24 @@
     show "B x" sorry %noproof
   qed
 
-  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<forall>x. B x" sorry %noproof
   then have "B a" ..
 
-  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<exists>x. B x"
   proof
     show "B a" sorry %noproof
   qed
 
-  txt_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*)
 
   have "\<exists>x. B x" sorry %noproof
   then obtain a where "B a" ..
 
-  txt_raw \<open>\end{minipage}\<close>
+  text_raw \<open>\end{minipage}\<close>
 
 (*<*)
 qed

--- a/src/Doc/Isar_Ref/Framework.thy	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy	Thu Nov 13 23:45:15 2014 +0100
@@ -654,31 +654,31 @@
 theorem True
 proof
 (*>*)
-  txt_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
+  text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close>
   {
     fix x
     have "B x" sorry %noproof
   }
   note \<open>\<And>x. B x\<close>
-  txt_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
   {
     assume A
     have B sorry %noproof
   }
   note \<open>A \<Longrightarrow> B\<close>
-  txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
   {
     def x \<equiv> a
     have "B x" sorry %noproof
   }
   note \<open>B a\<close>
-  txt_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
+  text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*)
   {
     obtain x where "A x" sorry %noproof
     have B sorry %noproof
   }
   note \<open>B\<close>
-  txt_raw \<open>\end{minipage}\<close>
+  text_raw \<open>\end{minipage}\<close>
 (*<*)
 qed
 (*>*)
@@ -819,14 +819,14 @@
 text_raw \<open>\begingroup\footnotesize\<close>
 (*<*)notepad begin
 (*>*)
-  txt_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>
+  text_raw \<open>\begin{minipage}[t]{0.18\textwidth}\<close>
   have "A \<longrightarrow> B"
   proof
     assume A
     show B
       sorry %noproof
   qed
-  txt_raw \<open>\end{minipage}\quad
+  text_raw \<open>\end{minipage}\quad
 \begin{minipage}[t]{0.06\textwidth}
 @{text "begin"} \\
 \\
@@ -886,7 +886,7 @@
     show "C x y" sorry %noproof
   qed
 
-txt_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
+text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
 
 (*<*)
 next
@@ -898,7 +898,7 @@
     show "C x y" sorry %noproof
   qed
 
-txt_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
+text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close>
 
 (*<*)
 next
@@ -910,7 +910,7 @@
     show "C x y" sorry
   qed
 
-txt_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
+text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close>
 (*<*)
 next
 (*>*)

--- a/src/Doc/Prog_Prove/Isar.thy	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy	Thu Nov 13 23:45:15 2014 +0100
@@ -240,12 +240,12 @@
 show "R"
 proof cases
   assume "P"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 next
   assume "\<not> P"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)oops(*>*)
 text_raw {* }
 \end{minipage}\index{cases@@{text cases}}
@@ -254,16 +254,16 @@
 \isa{%
 *}
 (*<*)lemma "R" proof-(*>*)
-have "P \<or> Q" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+have "P \<or> Q" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 then show "R"
 proof
   assume "P"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 next
   assume "Q"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)oops(*>*)
 
 text_raw {* }
@@ -279,12 +279,12 @@
 show "P \<longleftrightarrow> Q"
 proof
   assume "P"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "Q" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "Q" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
 next
   assume "Q"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "P" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "P" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
 qed(*<*)qed(*>*)
 text_raw {* }
 \medskip
@@ -299,8 +299,8 @@
 show "\<not> P"
 proof
   assume "P"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)oops(*>*)
 
 text_raw {* }
@@ -313,8 +313,8 @@
 show "P"
 proof (rule ccontr)
   assume "\<not>P"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)oops(*>*)
 
 text_raw {* }
@@ -332,8 +332,8 @@
 show "\<forall>x. P(x)"
 proof
   fix x
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "P(x)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "P(x)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)oops(*>*)
 
 text_raw {* }
@@ -345,8 +345,8 @@
 (*<*)lemma "EX x. P(x)" proof-(*>*)
 show "\<exists>x. P(x)"
 proof
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "P(witness)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "P(witness)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed
 (*<*)oops(*>*)
 
@@ -367,7 +367,7 @@
 \end{isamarkuptext}%
 *}
 (*<*)lemma True proof- assume 1: "EX x. P x"(*>*)
-have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)txt_raw{*\ $\dots$\\*}
+have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)text_raw{*\ $\dots$\\*}
 then obtain x where p: "P(x)" by blast
 (*<*)oops(*>*)
 text{*
@@ -401,9 +401,9 @@
 (*<*)lemma "A = (B::'a set)" proof-(*>*)
 show "A = B"
 proof
-  show "A \<subseteq> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  show "A \<subseteq> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 next
-  show "B \<subseteq> A" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  show "B \<subseteq> A" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)qed(*>*)
 
 text_raw {* }
@@ -417,8 +417,8 @@
 proof
   fix x
   assume "x \<in> A"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "x \<in> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "x \<in> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)qed(*>*)
 
 text_raw {* }
@@ -444,12 +444,12 @@
 show "formula\<^sub>1 \<longleftrightarrow> formula\<^sub>2" (is "?L \<longleftrightarrow> ?R")
 proof
   assume "?L"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "?R" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "?R" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
 next
   assume "?R"
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show "?L" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show "?L" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
 qed(*<*)qed(*>*)
 
 text{* Instead of duplicating @{text"formula\<^sub>i"} in the text, we introduce
@@ -462,8 +462,8 @@
 
 lemma "formula"
 proof -
-  txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
-  show ?thesis (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
+  show ?thesis (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
 qed
 
 text{* 
@@ -511,12 +511,12 @@
 \isa{%
 *}
 (*<*)lemma "P" proof-(*>*)
-have "P\<^sub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
-moreover have "P\<^sub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+have "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+moreover have "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 moreover
-txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*)
-moreover have "P\<^sub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
-ultimately have "P"  (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*)
+moreover have "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ultimately have "P"  (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 (*<*)oops(*>*)
 
 text_raw {* }
@@ -527,12 +527,12 @@
 \isa{%
 *}
 (*<*)lemma "P" proof-(*>*)
-have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
-have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$*}
-txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*}
-have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
-from lab\<^sub>1 lab\<^sub>2 txt_raw{*\ $\dots$\\*}
-have "P"  (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$*}
+text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}
+have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+from lab\<^sub>1 lab\<^sub>2 text_raw{*\ $\dots$\\*}
+have "P"  (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 (*<*)oops(*>*)
 
 text_raw {* }
@@ -733,12 +733,12 @@
 show "P(n)"
 proof (induction n)
   case 0
-  txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
-  show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
+  show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
 next
   case (Suc n)
-  txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
-  show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}
+  text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
+  show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
 qed(*<*)qed(*>*)
 
 text_raw {* }
@@ -904,18 +904,18 @@
 show "I x \<Longrightarrow> P x"
 proof(induction rule: I.induct)
   case rule\<^sub>1
-  txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
-  show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
+  show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 next
-  txt_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
+  text_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
 (*<*)
   case rule\<^sub>2
   show ?case sorry
 (*>*)
 next
   case rule\<^sub>n
-  txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
-  show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}
+  text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
+  show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
 qed(*<*)qed(*>*)
 
 text{*

--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Thu Nov 13 23:45:15 2014 +0100
@@ -121,7 +121,7 @@
           unfolding H'_def sum_def lin_def by blast
         
         have ya: "y1 + y2 = y \<and> a1 + a2 = a" using E HE _ y x0
-        proof (rule decomp_H') txt_raw \<open>\label{decomp-H-use}\<close>
+        proof (rule decomp_H') text_raw \<open>\label{decomp-H-use}\<close>
           from HE y1 y2 show "y1 + y2 \<in> H"
             by (rule subspace.add_closed)
           from x0 and HE y y1 y2

--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Nov 13 23:45:15 2014 +0100
@@ -179,7 +179,7 @@
 ML {*
   Outer_Syntax.command
     @{command_spec "text_cartouche"} ""
-    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.local_theory_markup)
+    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.document_command)
 *}
 
 text_cartouche

--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -7,30 +7,6 @@
 structure Isar_Syn: sig end =
 struct
 
-(** markup commands **)
-
-val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup_Env
-    @{command_spec "text"} "formal comment (theory)"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup);
-
-val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Verbatim
-    @{command_spec "text_raw"} "raw document preparation text"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.local_theory_markup);
-
-val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup_Env
-    @{command_spec "txt"} "formal comment (proof)"
-    (Parse.document_source >> Thy_Output.proof_markup);
-
-val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Verbatim
-    @{command_spec "txt_raw"} "raw document preparation text (proof)"
-    (Parse.document_source >> Thy_Output.proof_markup);
-
-
-
 (** theory commands **)
 
 (* sorts *)

--- a/src/Pure/Isar/keyword.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -7,7 +7,9 @@
 signature KEYWORD =
 sig
   val diag: string
-  val heading: string
+  val document_heading: string
+  val document_body: string
+  val document_raw: string
   val thy_begin: string
   val thy_end: string
   val thy_decl: string
@@ -41,8 +43,11 @@
   val is_literal: keywords -> string -> bool
   val command_files: keywords -> string -> Path.T -> Path.T list
   val command_tags: keywords -> string -> string list
+  val is_vacuous: keywords -> string -> bool
   val is_diag: keywords -> string -> bool
-  val is_heading: keywords -> string -> bool
+  val is_document_heading: keywords -> string -> bool
+  val is_document_body: keywords -> string -> bool
+  val is_document_raw: keywords -> string -> bool
   val is_theory_begin: keywords -> string -> bool
   val is_theory_load: keywords -> string -> bool
   val is_theory: keywords -> string -> bool
@@ -64,7 +69,9 @@
 (* kinds *)
 
 val diag = "diag";
-val heading = "heading";
+val document_heading = "document_heading";
+val document_body = "document_body";
+val document_raw = "document_raw";
 val thy_begin = "thy_begin";
 val thy_end = "thy_end";
 val thy_decl = "thy_decl";
@@ -87,9 +94,9 @@
 val prf_script = "prf_script";
 
 val kinds =
-  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
-    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+  [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
+    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open,
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 
 (* specifications *)
@@ -196,9 +203,14 @@
       | SOME {kind, ...} => Symtab.defined tab kind);
   in pred end;
 
+val is_vacuous = command_category [diag, document_heading, document_body, document_raw];
+
 val is_diag = command_category [diag];
 
-val is_heading = command_category [heading];
+val is_document_heading = command_category [document_heading];
+val is_document_body = command_category [document_body];
+val is_document_raw = command_category [document_raw];
+val is_document = command_category [document_heading, document_body, document_raw];
 
 val is_theory_begin = command_category [thy_begin];
 
@@ -215,8 +227,8 @@
     prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_proof_body = command_category
-  [diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm,
-    prf_asm_goal, prf_asm_goal_script, prf_script];
+  [diag, document_heading, document_body, document_raw, prf_block, prf_open, prf_close,
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];

--- a/src/Pure/Isar/keyword.scala	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Thu Nov 13 23:45:15 2014 +0100
@@ -14,7 +14,9 @@
   /* kinds */
 
   val DIAG = "diag"
-  val HEADING = "heading"
+  val DOCUMENT_HEADING = "document_heading"
+  val DOCUMENT_BODY = "document_body"
+  val DOCUMENT_RAW = "document_raw"
   val THY_BEGIN = "thy_begin"
   val THY_END = "thy_end"
   val THY_DECL = "thy_decl"
@@ -39,9 +41,14 @@
 
   /* categories */
 
+  val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
+
   val diag = Set(DIAG)
 
-  val heading = Set(HEADING)
+  val document_heading = Set(DOCUMENT_HEADING)
+  val document_body = Set(DOCUMENT_BODY)
+  val document_raw = Set(DOCUMENT_RAW)
+  val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
 
   val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
 
@@ -54,8 +61,8 @@
       PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
 
   val proof_body =
-    Set(DIAG, HEADING, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM,
-      PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
+      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
 
   val theory_goal = Set(THY_GOAL)
   val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)

--- a/src/Pure/Isar/outer_syntax.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -6,15 +6,11 @@
 
 signature OUTER_SYNTAX =
 sig
-  datatype markup = Markup | Markup_Env | Verbatim
-  val is_markup: theory -> markup -> string -> bool
   val help: theory -> string list -> unit
   val print_commands: theory -> unit
   type command_spec = string * Position.T
   val command: command_spec -> string ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
-  val markup_command: markup -> command_spec -> string ->
-    (Toplevel.transition -> Toplevel.transition) parser -> unit
   val local_theory': command_spec -> string ->
     (bool -> local_theory -> local_theory) parser -> unit
   val local_theory: command_spec -> string ->
@@ -47,19 +43,16 @@
 
 (* command parsers *)
 
-datatype markup = Markup | Markup_Env | Verbatim;
-
 datatype command = Command of
  {comment: string,
-  markup: markup option,
   parse: (Toplevel.transition -> Toplevel.transition) parser,
   pos: Position.T,
   id: serial};
 
 fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2;
 
-fun new_command comment markup parse pos =
-  Command {comment = comment, markup = markup, parse = parse, pos = pos, id = serial ()};
+fun new_command comment parse pos =
+  Command {comment = comment, parse = parse, pos = pos, id = serial ()};
 
 fun command_pos (Command {pos, ...}) = pos;
 
@@ -74,45 +67,22 @@
         command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
 
 
-(* type syntax *)
-
-datatype syntax = Syntax of
- {commands: command Symtab.table,
-  markups: (string * markup) list};
-
-fun make_syntax (commands, markups) =
-  Syntax {commands = commands, markups = markups};
+(* theory data *)
 
 structure Data = Theory_Data
 (
-  type T = syntax;
-  val empty = make_syntax (Symtab.empty, []);
+  type T = command Symtab.table;
+  val empty = Symtab.empty;
   val extend = I;
-  fun merge (Syntax {commands = commands1, markups = markups1},
-      Syntax {commands = commands2, markups = markups2}) =
-    let
-      val commands' = (commands1, commands2)
-        |> Symtab.join (fn name => fn (cmd1, cmd2) =>
-          if eq_command (cmd1, cmd2) then raise Symtab.SAME
-          else err_dup_command name [command_pos cmd1, command_pos cmd2]);
-      val markups' = AList.merge (op =) (K true) (markups1, markups2);
-    in make_syntax (commands', markups') end;
+  fun merge data : T =
+    data |> Symtab.join (fn name => fn (cmd1, cmd2) =>
+      if eq_command (cmd1, cmd2) then raise Symtab.SAME
+      else err_dup_command name [command_pos cmd1, command_pos cmd2]);
 );
 
-
-(* inspect syntax *)
-
-val get_syntax = Data.get;
-
-val dest_commands =
-  get_syntax #> (fn Syntax {commands, ...} => commands |> Symtab.dest |> sort_wrt #1);
-
-val lookup_commands =
-  get_syntax #> (fn Syntax {commands, ...} => Symtab.lookup commands);
-
-val is_markup =
-  get_syntax #> (fn Syntax {markups, ...} => fn kind => fn name =>
-    AList.lookup (op =) markups name = SOME kind);
+val get_commands = Data.get;
+val dest_commands = get_commands #> Symtab.dest #> sort_wrt #1;
+val lookup_commands = Symtab.lookup o get_commands;
 
 fun help thy pats =
   dest_commands thy
@@ -132,36 +102,28 @@
   end;
 
 
-(* build syntax *)
+(* maintain commands *)
 
-fun add_command name cmd thy = thy |> Data.map (fn Syntax {commands, ...} =>
+fun add_command name cmd thy =
   let
-    val keywords = Thy_Header.get_keywords thy;
     val _ =
-      Keyword.is_command keywords name orelse
+      Keyword.is_command (Thy_Header.get_keywords thy) name orelse
         err_command "Undeclared outer syntax command " name [command_pos cmd];
-
     val _ =
-      (case Symtab.lookup commands name of
+      (case lookup_commands thy name of
         NONE => ()
       | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
-
     val _ =
       Context_Position.report_generic (ML_Context.the_generic_context ())
         (command_pos cmd) (command_markup true (name, cmd));
-
-    val commands' = Symtab.update (name, cmd) commands;
-    val markups' =
-      Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
-        commands' [];
-  in make_syntax (commands', markups') end);
+  in Data.map (Symtab.update (name, cmd)) thy end;
 
 val _ = Theory.setup (Theory.at_end (fn thy =>
   let
-    val keywords = Thy_Header.get_keywords thy;
-    val major = Keyword.major_keywords keywords;
+    val command_keywords =
+      Scan.dest_lexicon (Keyword.major_keywords (Thy_Header.get_keywords thy));
     val _ =
-      (case subtract (op =) (map #1 (dest_commands thy)) (Scan.dest_lexicon major) of
+      (case subtract (op =) (map #1 (dest_commands thy)) command_keywords of
         [] => ()
       | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
   in NONE end));
@@ -172,10 +134,7 @@
 type command_spec = string * Position.T;
 
 fun command (name, pos) comment parse =
-  Theory.setup (add_command name (new_command comment NONE parse pos));
-
-fun markup_command markup (name, pos) comment parse =
-  Theory.setup (add_command name (new_command comment (SOME markup) parse pos));
+  Theory.setup (add_command name (new_command comment parse pos));
 
 fun local_theory_command trans command_spec comment parse =
   command command_spec comment (Parse.opt_target -- parse >> (fn (loc, f) => trans loc f));

--- a/src/Pure/Isar/toplevel.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -65,7 +65,6 @@
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
   val forget_proof: bool -> transition -> transition
-  val present_proof: (state -> unit) -> transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
@@ -498,11 +497,6 @@
     | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | _ => raise UNDEF));
 
-val present_proof = present_transaction (fn _ =>
-  (fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x)
-    | skip as Skipped_Proof _ => skip
-    | _ => raise UNDEF));
-
 fun proofs' f = transaction (fn int =>
   (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
     | skip as Skipped_Proof _ => skip

--- a/src/Pure/Pure.thy	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Pure.thy	Thu Nov 13 23:45:15 2014 +0100
@@ -12,8 +12,8 @@
     "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
-  and "text" "text_raw" :: thy_decl
-  and "txt" "txt_raw" :: prf_decl % "proof"
+  and "text" "txt" :: document_body
+  and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""
   and "typedecl" "type_synonym" "nonterminal" "judgment"
     "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"

--- a/src/Pure/System/options.scala	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/System/options.scala	Thu Nov 13 23:45:15 2014 +0100
@@ -76,7 +76,7 @@
 
   lazy val options_syntax =
     Outer_Syntax.init() + ":" + "=" + "--" +
-      (SECTION, Keyword.HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
+      (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
 
   lazy val prefs_syntax = Outer_Syntax.init() + "="
 

--- a/src/Pure/Thy/thy_header.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -46,6 +46,9 @@
 val sectionN = "section";
 val subsectionN = "subsection";
 val subsubsectionN = "subsubsection";
+val textN = "text";
+val txtN = "txt";
+val text_rawN = "text_raw";
 
 val theoryN = "theory";
 val importsN = "imports";
@@ -65,11 +68,14 @@
      (beginN, NONE),
      (importsN, NONE),
      (keywordsN, NONE),
-     (headerN, SOME ((Keyword.heading, []), [])),
-     (chapterN, SOME ((Keyword.heading, []), [])),
-     (sectionN, SOME ((Keyword.heading, []), [])),
-     (subsectionN, SOME ((Keyword.heading, []), [])),
-     (subsubsectionN, SOME ((Keyword.heading, []), [])),
+     (headerN, SOME ((Keyword.document_heading, []), [])),
+     (chapterN, SOME ((Keyword.document_heading, []), [])),
+     (sectionN, SOME ((Keyword.document_heading, []), [])),
+     (subsectionN, SOME ((Keyword.document_heading, []), [])),
+     (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
+     (textN, SOME ((Keyword.document_body, []), [])),
+     (txtN, SOME ((Keyword.document_body, []), [])),
+     (text_rawN, SOME ((Keyword.document_raw, []), [])),
      (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
      ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
 
@@ -138,7 +144,10 @@
     Parse.command chapterN ||
     Parse.command sectionN ||
     Parse.command subsectionN ||
-    Parse.command subsubsectionN) --
+    Parse.command subsubsectionN ||
+    Parse.command textN ||
+    Parse.command txtN ||
+    Parse.command text_rawN) --
   Parse.tags -- Parse.!!! Parse.document_source;
 
 val header =

--- a/src/Pure/Thy/thy_header.scala	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Nov 13 23:45:15 2014 +0100
@@ -24,6 +24,9 @@
   val SECTION = "section"
   val SUBSECTION = "subsection"
   val SUBSUBSECTION = "subsubsection"
+  val TEXT = "text"
+  val TXT = "txt"
+  val TEXT_RAW = "text_raw"
 
   val THEORY = "theory"
   val IMPORTS = "imports"
@@ -43,11 +46,14 @@
       (BEGIN, None, None),
       (IMPORTS, None, None),
       (KEYWORDS, None, None),
-      (HEADER, Some(((Keyword.HEADING, Nil), Nil)), None),
-      (CHAPTER, Some(((Keyword.HEADING, Nil), Nil)), None),
-      (SECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
-      (SUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
-      (SUBSUBSECTION, Some(((Keyword.HEADING, Nil), Nil)), None),
+      (HEADER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+      (CHAPTER, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+      (SECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+      (SUBSECTION, Some(((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
+      (SUBSUBSECTION, 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),
       (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
       ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
 
@@ -110,7 +116,10 @@
         command(CHAPTER) |
         command(SECTION) |
         command(SUBSECTION) |
-        command(SUBSUBSECTION)) ~
+        command(SUBSUBSECTION) |
+        command(TEXT) |
+        command(TXT) |
+        command(TEXT_RAW)) ~
       tags ~! document_source
 
     (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }

--- a/src/Pure/Thy/thy_output.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -33,11 +33,8 @@
     Token.src -> 'a list -> Pretty.T list
   val output: Proof.context -> Pretty.T list -> string
   val verbatim_text: Proof.context -> string -> string
-  val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
-    Toplevel.transition -> Toplevel.transition
-  val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
-  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
-  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
+  val old_header_command: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
+  val document_command: (xstring * Position.T) option * Symbol_Pos.source ->
     Toplevel.transition -> Toplevel.transition
 end;
 
@@ -285,22 +282,30 @@
     val (tag, tags) = tag_stack;
     val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
 
+    val nesting = Toplevel.level state' - Toplevel.level state;
+
     val active_tag' =
       if is_some tag' then tag'
       else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
-      else try hd (Keyword.command_tags keywords cmd_name);
+      else
+        (case Keyword.command_tags keywords cmd_name of
+          default_tag :: _ => SOME default_tag
+        | [] =>
+            if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
+            then active_tag
+            else NONE);
+
     val edge = (active_tag, active_tag');
 
     val newline' =
       if is_none active_tag' then span_newline else newline;
 
-    val nesting = Toplevel.level state' - Toplevel.level state;
     val tag_stack' =
       if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
       else if nesting >= 0 then (tag', replicate nesting tag @ tags)
       else
         (case drop (~ nesting - 1) tags of
-          tgs :: tgss => (tgs, tgss)
+          tg :: tgs => (tg, tgs)
         | [] => err_bad_nesting (Position.here cmd_pos));
 
     val buffer' =
@@ -359,7 +364,6 @@
 fun present_thy thy command_results toks =
   let
     val keywords = Thy_Header.get_keywords thy;
-    val is_markup = Outer_Syntax.is_markup thy;
 
 
     (* tokens *)
@@ -367,9 +371,10 @@
     val ignored = Scan.state --| ignore
       >> (fn d => (NONE, (NoToken, ("", d))));
 
-    fun markup mark mk flag = Scan.peek (fn d =>
+    fun markup pred mk flag = Scan.peek (fn d =>
       improper |--
-        Parse.position (Scan.one (Token.is_command andf is_markup mark o Token.content_of)) --
+        Parse.position (Scan.one (fn tok =>
+          Token.is_command tok andalso pred keywords (Token.content_of tok))) --
       Scan.repeat tag --
       Parse.!!!! ((improper -- locale -- improper) |-- Parse.document_source --| improper_end)
       >> (fn (((tok, pos'), tags), {text, range = (pos, _), ...}) =>
@@ -392,9 +397,9 @@
 
     val token =
       ignored ||
-      markup Outer_Syntax.Markup MarkupToken Latex.markup_true ||
-      markup Outer_Syntax.Markup_Env MarkupEnvToken Latex.markup_true ||
-      markup Outer_Syntax.Verbatim (VerbatimToken o #2) "" ||
+      markup Keyword.is_document_heading MarkupToken Latex.markup_true ||
+      markup Keyword.is_document_body MarkupEnvToken Latex.markup_true ||
+      markup Keyword.is_document_raw (VerbatimToken o #2) "" ||
       command || cmt || other;
 
 
@@ -702,27 +707,21 @@
 
 
 
-(** markup commands **)
-
-fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
-val proof_markup = Toplevel.present_proof o check_text;
+(** document commands **)
 
-fun reject_target NONE = ()
-  | reject_target (SOME (_, pos)) =
-      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
-
-fun header_markup txt =
+fun old_header_command txt =
   Toplevel.keep (fn state =>
     if Toplevel.is_toplevel state then
      (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
       check_text txt state)
     else raise Toplevel.UNDEF);
 
-fun heading_markup (loc, txt) =
+fun document_command (loc, txt) =
   Toplevel.keep (fn state =>
-    if Toplevel.is_toplevel state then (reject_target loc; check_text txt state)
-    else raise Toplevel.UNDEF) o
-  local_theory_markup (loc, txt) o
-  Toplevel.present_proof (fn state => (reject_target loc; check_text txt state));
+    (case loc of
+      NONE => check_text txt state
+    | SOME (_, pos) =>
+        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
+  Toplevel.present_local_theory loc (check_text txt);
 
 end;

--- a/src/Pure/pure_syn.ML	Thu Nov 13 17:28:11 2014 +0100
+++ b/src/Pure/pure_syn.ML	Thu Nov 13 23:45:15 2014 +0100
@@ -8,24 +8,36 @@
 struct
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("header", @{here}) "theory header"
-    (Parse.document_source >> Thy_Output.header_markup);
+  Outer_Syntax.command ("header", @{here}) "theory header"
+    (Parse.document_source >> Thy_Output.old_header_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("chapter", @{here}) "chapter heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("chapter", @{here}) "chapter heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+
+val _ =
+  Outer_Syntax.command ("section", @{here}) "section heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("section", @{here}) "section heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("subsection", @{here}) "subsection heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+
+val _ =
+  Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsection", @{here}) "subsection heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
 
 val _ =
-  Outer_Syntax.markup_command Outer_Syntax.Markup ("subsubsection", @{here}) "subsubsection heading"
-    (Parse.opt_target -- Parse.document_source >> Thy_Output.heading_markup);
+  Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command);
+
+val _ =
+  Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
+    (Parse.document_source >> K (Toplevel.imperative I));
 
 val _ =
   Outer_Syntax.command ("theory", @{here}) "begin theory"