# HG changeset patch # User wenzelm # Date 1415918715 -3600 # Node ID ed09ae4ea2d8cdfe5ca33e63acb7ad4271da97ea # Parent 6237574c705b3c7d3978763fe8ff15517657b870 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; diff -r 6237574c705b -r ed09ae4ea2d8 NEWS --- 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 diff -r 6237574c705b -r ed09ae4ea2d8 src/Doc/Isar_Ref/Document_Preparation.thy --- 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 \ any"} \\ @{command_def "subsection"} & : & @{text "any \ any"} \\ @{command_def "subsubsection"} & : & @{text "any \ any"} \\ - @{command_def "text"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "text_raw"} & : & @{text "local_theory \ local_theory"} \\[0.5ex] - @{command_def "txt"} & : & @{text "proof \ proof"} \\ - @{command_def "txt_raw"} & : & @{text "proof \ proof"} \\ + @{command_def "text"} & : & @{text "any \ any"} \\ + @{command_def "txt"} & : & @{text "any \ any"} \\ + @{command_def "text_raw"} & : & @{text "any \ any"} \\ \end{matharray} Markup commands provide a structured way to insert text into the @@ -45,9 +44,10 @@ @{rail \ (@@{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} \} \begin{description} @@ -59,22 +59,22 @@ @{verbatim \\isamarkupchapter\}, @{verbatim \\isamarkupsection\}, @{verbatim \\isamarkupsubsection\}, @{verbatim \\isamarkupsubsubsection\}. - \item @{command text} and @{command txt} specify paragraphs of plain - text. This corresponds to a {\LaTeX} environment @{verbatim - \\begin{isamarkuptext}\} @{text "\"} @{verbatim \\end{isamarkuptext}\} etc. + \item @{command text} and @{command txt} specify paragraphs of plain text. + This corresponds to a {\LaTeX} environment @{verbatim + \\begin{isamarkuptext}\} @{text "\"} @{verbatim \\end{isamarkuptext}\} + 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 diff -r 6237574c705b -r ed09ae4ea2d8 src/Doc/Isar_Ref/First_Order_Logic.thy --- 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 \\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "A \ B" proof @@ -422,12 +422,12 @@ show B sorry %noproof qed - txt_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "A \ B" and A sorry %noproof then have B .. - txt_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have A sorry %noproof then have "A \ B" .. @@ -435,7 +435,7 @@ have B sorry %noproof then have "A \ B" .. - txt_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "A \ B" sorry %noproof then have C @@ -447,26 +447,26 @@ then show C sorry %noproof qed - txt_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have A and B sorry %noproof then have "A \ B" .. - txt_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "A \ B" sorry %noproof then obtain A and B .. - txt_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\" sorry %noproof then have A .. - txt_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\" .. - txt_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\ A" proof @@ -474,12 +474,12 @@ then show "\" sorry %noproof qed - txt_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\ A" and A sorry %noproof then have B .. - txt_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\x. B x" proof @@ -487,24 +487,24 @@ show "B x" sorry %noproof qed - txt_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\x. B x" sorry %noproof then have "B a" .. - txt_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\x. B x" proof show "B a" sorry %noproof qed - txt_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\(*<*)next(*>*) have "\x. B x" sorry %noproof then obtain a where "B a" .. - txt_raw \\end{minipage}\ + text_raw \\end{minipage}\ (*<*) qed diff -r 6237574c705b -r ed09ae4ea2d8 src/Doc/Isar_Ref/Framework.thy --- 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 \\begin{minipage}[t]{0.45\textwidth}\ + text_raw \\begin{minipage}[t]{0.45\textwidth}\ { fix x have "B x" sorry %noproof } note \\x. B x\ - txt_raw \\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) { assume A have B sorry %noproof } note \A \ B\ - txt_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) { def x \ a have "B x" sorry %noproof } note \B a\ - txt_raw \\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) + text_raw \\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\(*<*)next(*>*) { obtain x where "A x" sorry %noproof have B sorry %noproof } note \B\ - txt_raw \\end{minipage}\ + text_raw \\end{minipage}\ (*<*) qed (*>*) @@ -819,14 +819,14 @@ text_raw \\begingroup\footnotesize\ (*<*)notepad begin (*>*) - txt_raw \\begin{minipage}[t]{0.18\textwidth}\ + text_raw \\begin{minipage}[t]{0.18\textwidth}\ have "A \ B" proof assume A show B sorry %noproof qed - txt_raw \\end{minipage}\quad + text_raw \\end{minipage}\quad \begin{minipage}[t]{0.06\textwidth} @{text "begin"} \\ \\ @@ -886,7 +886,7 @@ show "C x y" sorry %noproof qed -txt_raw \\end{minipage}\begin{minipage}{0.5\textwidth}\ +text_raw \\end{minipage}\begin{minipage}{0.5\textwidth}\ (*<*) next @@ -898,7 +898,7 @@ show "C x y" sorry %noproof qed -txt_raw \\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\ +text_raw \\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\ (*<*) next @@ -910,7 +910,7 @@ show "C x y" sorry qed -txt_raw \\end{minipage}\begin{minipage}{0.5\textwidth}\ +text_raw \\end{minipage}\begin{minipage}{0.5\textwidth}\ (*<*) next (*>*) diff -r 6237574c705b -r ed09ae4ea2d8 src/Doc/Prog_Prove/Isar.thy --- 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 "\ 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 \ Q" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +have "P \ 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 \ 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 "\ 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 "\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 "\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 "\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 "\x. P(x)" (*<*)by(rule 1)(*>*)txt_raw{*\ $\dots$\\*} +have "\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 \ B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} + show "A \ B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} next - show "B \ A" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} + show "B \ A" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} qed(*<*)qed(*>*) text_raw {* } @@ -417,8 +417,8 @@ proof fix x assume "x \ A" - txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} - show "x \ B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} + text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "x \ B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} qed(*<*)qed(*>*) text_raw {* } @@ -444,12 +444,12 @@ show "formula\<^sub>1 \ formula\<^sub>2" (is "?L \ ?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 \ 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{* diff -r 6237574c705b -r ed09ae4ea2d8 src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy --- 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 \ a1 + a2 = a" using E HE _ y x0 - proof (rule decomp_H') txt_raw \\label{decomp-H-use}\ + proof (rule decomp_H') text_raw \\label{decomp-H-use}\ from HE y1 y2 show "y1 + y2 \ H" by (rule subspace.add_closed) from x0 and HE y y1 y2 diff -r 6237574c705b -r ed09ae4ea2d8 src/HOL/ex/Cartouche_Examples.thy --- 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 diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Isar/isar_syn.ML --- 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 *) diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Isar/keyword.ML --- 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]; diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Isar/keyword.scala --- 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) diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Isar/outer_syntax.ML --- 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)); diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Isar/toplevel.ML --- 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 diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Pure.thy --- 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" diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/System/options.scala --- 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() + "=" diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Thy/thy_header.ML --- 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 = diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Thy/thy_header.scala --- 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 } diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/Thy/thy_output.ML --- 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; diff -r 6237574c705b -r ed09ae4ea2d8 src/Pure/pure_syn.ML --- 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"