uniform heading commands work in any context, even in theory header;
authorwenzelm
Sun Nov 02 15:27:37 2014 +0100 (2014-11-02 ago)
changeset 58868c5e1cce7ace3
parent 58867 911addd19e9f
child 58869 963fd2084e8f
uniform heading commands work in any context, even in theory header;
discontinued obsolete 'sect', 'subsect', 'subsubsect';
marked obsolete 'header' as legacy;
NEWS
lib/texinputs/isabelle.sty
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Tutorial/Documents/Documents.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Pure.thy
src/Pure/System/options.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/NEWS	Sun Nov 02 13:26:20 2014 +0100
     1.2 +++ b/NEWS	Sun Nov 02 15:27:37 2014 +0100
     1.3 @@ -167,6 +167,13 @@
     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. Minor INCOMPATIBILITY.
    1.13 +
    1.14  * Official support for "tt" style variants, via \isatt{...} or
    1.15  \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
    1.16  verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
     2.1 --- a/lib/texinputs/isabelle.sty	Sun Nov 02 13:26:20 2014 +0100
     2.2 +++ b/lib/texinputs/isabelle.sty	Sun Nov 02 15:27:37 2014 +0100
     2.3 @@ -127,9 +127,6 @@
     2.4  \newcommand{\isamarkupsection}[1]{\section{#1}}
     2.5  \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
     2.6  \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
     2.7 -\newcommand{\isamarkupsect}[1]{\section{#1}}
     2.8 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
     2.9 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
    2.10  
    2.11  \newif\ifisamarkup
    2.12  \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
     3.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Nov 02 13:26:20 2014 +0100
     3.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Nov 02 15:27:37 2014 +0100
     3.3 @@ -22,16 +22,12 @@
     3.4  
     3.5  text \<open>
     3.6    \begin{matharray}{rcl}
     3.7 -    @{command_def "header"} & : & @{text "toplevel \<rightarrow> toplevel"} \\[0.5ex]
     3.8 -    @{command_def "chapter"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     3.9 -    @{command_def "section"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    3.10 -    @{command_def "subsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    3.11 -    @{command_def "subsubsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    3.12 +    @{command_def "chapter"} & : & @{text "any \<rightarrow> any"} \\
    3.13 +    @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\
    3.14 +    @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\
    3.15 +    @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\
    3.16      @{command_def "text"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    3.17      @{command_def "text_raw"} & : & @{text "local_theory \<rightarrow> local_theory"} \\[0.5ex]
    3.18 -    @{command_def "sect"} & : & @{text "proof \<rightarrow> proof"} \\
    3.19 -    @{command_def "subsect"} & : & @{text "proof \<rightarrow> proof"} \\
    3.20 -    @{command_def "subsubsect"} & : & @{text "proof \<rightarrow> proof"} \\
    3.21      @{command_def "txt"} & : & @{text "proof \<rightarrow> proof"} \\
    3.22      @{command_def "txt_raw"} & : & @{text "proof \<rightarrow> proof"} \\
    3.23    \end{matharray}
    3.24 @@ -51,26 +47,17 @@
    3.25      (@@{command chapter} | @@{command section} | @@{command subsection} |
    3.26        @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text}
    3.27      ;
    3.28 -    (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} |
    3.29 -      @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text}
    3.30 +    (@@{command text_raw} | @@{command txt} | @@{command txt_raw}) @{syntax text}
    3.31    \<close>}
    3.32  
    3.33    \begin{description}
    3.34  
    3.35 -  \item @{command header} provides plain text markup just preceding
    3.36 -  the formal beginning of a theory.  The corresponding {\LaTeX} macro
    3.37 -  is @{verbatim \<open>\isamarkupheader\<close>}, which acts like @{command
    3.38 -  section} by default.
    3.39 -  
    3.40 -  \item @{command chapter}, @{command section}, @{command subsection},
    3.41 -  and @{command subsubsection} mark chapter and section headings
    3.42 -  within the main theory body or local theory targets.  The
    3.43 -  corresponding {\LaTeX} macros are @{verbatim \<open>\isamarkupchapter\<close>},
    3.44 -  @{verbatim \<open>\isamarkupsection\<close>}, @{verbatim \<open>\isamarkupsubsection\<close>} etc.
    3.45 -
    3.46 -  \item @{command sect}, @{command subsect}, and @{command subsubsect}
    3.47 -  mark section headings within proofs.  The corresponding {\LaTeX}
    3.48 -  macros are @{verbatim \<open>\isamarkupsect\<close>}, @{verbatim \<open>\isamarkupsubsect\<close>} etc.
    3.49 +  \item @{command chapter}, @{command section}, @{command subsection}, and
    3.50 +  @{command subsubsection} mark chapter and section headings within the
    3.51 +  theory source; this works in any context, even before the initial
    3.52 +  @{command theory} command. The corresponding {\LaTeX} macros are
    3.53 +  @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},
    3.54 +  @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}.
    3.55  
    3.56    \item @{command text} and @{command txt} specify paragraphs of plain
    3.57    text.  This corresponds to a {\LaTeX} environment @{verbatim
    3.58 @@ -91,8 +78,7 @@
    3.59  
    3.60    \medskip The proof markup commands closely resemble those for theory
    3.61    specifications, but have a different formal status and produce
    3.62 -  different {\LaTeX} macros.  The default definitions coincide for
    3.63 -  analogous commands such as @{command section} and @{command sect}.
    3.64 +  different {\LaTeX} macros.
    3.65  \<close>
    3.66  
    3.67  
     4.1 --- a/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 02 13:26:20 2014 +0100
     4.2 +++ b/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 02 15:27:37 2014 +0100
     4.3 @@ -424,24 +424,6 @@
     4.4    do not affect the formal meaning of a theory (or proof), but result
     4.5    in corresponding {\LaTeX} elements.
     4.6  
     4.7 -  There are separate markup commands depending on the textual context:
     4.8 -  in header position (just before \isakeyword{theory}), within the
     4.9 -  theory body, or within a proof.  The header needs to be treated
    4.10 -  specially here, since ordinary theory and proof commands may only
    4.11 -  occur \emph{after} the initial \isakeyword{theory} specification.
    4.12 -
    4.13 -  \medskip
    4.14 -
    4.15 -  \begin{tabular}{llll}
    4.16 -  header & theory & proof & default meaning \\\hline
    4.17 -    & \commdx{chapter} & & \verb,\chapter, \\
    4.18 -  \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
    4.19 -    & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
    4.20 -    & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
    4.21 -  \end{tabular}
    4.22 -
    4.23 -  \medskip
    4.24 -
    4.25    From the Isabelle perspective, each markup command takes a single
    4.26    $text$ argument (delimited by \verb,",~@{text \<dots>}~\verb,", or
    4.27    \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,},).  After stripping any
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 13:26:20 2014 +0100
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 15:27:37 2014 +0100
     5.3 @@ -48,10 +48,11 @@
     5.4    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
     5.5    val print_type: (string list * (string * string option)) ->
     5.6      Toplevel.transition -> Toplevel.transition
     5.7 -  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
     5.8 -  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) ->
     5.9 +  val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
    5.10      Toplevel.transition -> Toplevel.transition
    5.11    val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    5.12 +  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
    5.13 +    Toplevel.transition -> Toplevel.transition
    5.14  end;
    5.15  
    5.16  structure Isar_Cmd: ISAR_CMD =
    5.17 @@ -377,11 +378,21 @@
    5.18  
    5.19  (* markup commands *)
    5.20  
    5.21 -fun header_markup txt = Toplevel.keep (fn state =>
    5.22 -  if Toplevel.is_toplevel state then Thy_Output.check_text txt state
    5.23 -  else raise Toplevel.UNDEF);
    5.24 -
    5.25  fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
    5.26  val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
    5.27  
    5.28 +fun reject_target NONE = ()
    5.29 +  | reject_target (SOME (_, pos)) =
    5.30 +      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
    5.31 +
    5.32 +fun heading_markup (loc, txt) =
    5.33 +  Toplevel.keep (fn state =>
    5.34 +    if Toplevel.is_toplevel state then
    5.35 +     (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
    5.36 +      reject_target loc;
    5.37 +      Thy_Output.check_text txt state)
    5.38 +    else raise Toplevel.UNDEF) o
    5.39 +  local_theory_markup (loc, txt) o
    5.40 +  Toplevel.present_proof (fn state => (reject_target loc; Thy_Output.check_text txt state));
    5.41 +
    5.42  end;
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Nov 02 13:26:20 2014 +0100
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 02 15:27:37 2014 +0100
     6.3 @@ -12,27 +12,27 @@
     6.4  val _ =
     6.5    Outer_Syntax.markup_command Thy_Output.Markup
     6.6      @{command_spec "header"} "theory header"
     6.7 -    (Parse.document_source >> Isar_Cmd.header_markup);
     6.8 +    (Parse.document_source >> (fn s => Isar_Cmd.heading_markup (NONE, s)));
     6.9  
    6.10  val _ =
    6.11    Outer_Syntax.markup_command Thy_Output.Markup
    6.12      @{command_spec "chapter"} "chapter heading"
    6.13 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
    6.14 +    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
    6.15  
    6.16  val _ =
    6.17    Outer_Syntax.markup_command Thy_Output.Markup
    6.18      @{command_spec "section"} "section heading"
    6.19 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
    6.20 +    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
    6.21  
    6.22  val _ =
    6.23    Outer_Syntax.markup_command Thy_Output.Markup
    6.24      @{command_spec "subsection"} "subsection heading"
    6.25 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
    6.26 +    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
    6.27  
    6.28  val _ =
    6.29    Outer_Syntax.markup_command Thy_Output.Markup
    6.30      @{command_spec "subsubsection"} "subsubsection heading"
    6.31 -    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
    6.32 +    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
    6.33  
    6.34  val _ =
    6.35    Outer_Syntax.markup_command Thy_Output.MarkupEnv
    6.36 @@ -45,21 +45,6 @@
    6.37      (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
    6.38  
    6.39  val _ =
    6.40 -  Outer_Syntax.markup_command Thy_Output.Markup
    6.41 -    @{command_spec "sect"} "formal comment (proof)"
    6.42 -    (Parse.document_source >> Isar_Cmd.proof_markup);
    6.43 -
    6.44 -val _ =
    6.45 -  Outer_Syntax.markup_command Thy_Output.Markup
    6.46 -    @{command_spec "subsect"} "formal comment (proof)"
    6.47 -    (Parse.document_source >> Isar_Cmd.proof_markup);
    6.48 -
    6.49 -val _ =
    6.50 -  Outer_Syntax.markup_command Thy_Output.Markup
    6.51 -    @{command_spec "subsubsect"} "formal comment (proof)"
    6.52 -    (Parse.document_source >> Isar_Cmd.proof_markup);
    6.53 -
    6.54 -val _ =
    6.55    Outer_Syntax.markup_command Thy_Output.MarkupEnv
    6.56      @{command_spec "txt"} "formal comment (proof)"
    6.57      (Parse.document_source >> Isar_Cmd.proof_markup);
     7.1 --- a/src/Pure/Isar/keyword.ML	Sun Nov 02 13:26:20 2014 +0100
     7.2 +++ b/src/Pure/Isar/keyword.ML	Sun Nov 02 15:27:37 2014 +0100
     7.3 @@ -10,12 +10,9 @@
     7.4    val kind_of: T -> string
     7.5    val kind_files_of: T -> string * string list
     7.6    val diag: T
     7.7 +  val heading: T
     7.8    val thy_begin: T
     7.9    val thy_end: T
    7.10 -  val thy_heading1: T
    7.11 -  val thy_heading2: T
    7.12 -  val thy_heading3: T
    7.13 -  val thy_heading4: T
    7.14    val thy_decl: T
    7.15    val thy_decl_block: T
    7.16    val thy_load: T
    7.17 @@ -25,9 +22,6 @@
    7.18    val qed_script: T
    7.19    val qed_block: T
    7.20    val qed_global: T
    7.21 -  val prf_heading2: T
    7.22 -  val prf_heading3: T
    7.23 -  val prf_heading4: T
    7.24    val prf_goal: T
    7.25    val prf_block: T
    7.26    val prf_open: T
    7.27 @@ -90,12 +84,9 @@
    7.28  (* kinds *)
    7.29  
    7.30  val diag = kind "diag";
    7.31 +val heading = kind "heading";
    7.32  val thy_begin = kind "thy_begin";
    7.33  val thy_end = kind "thy_end";
    7.34 -val thy_heading1 = kind "thy_heading1";
    7.35 -val thy_heading2 = kind "thy_heading2";
    7.36 -val thy_heading3 = kind "thy_heading3";
    7.37 -val thy_heading4 = kind "thy_heading4";
    7.38  val thy_decl = kind "thy_decl";
    7.39  val thy_decl_block = kind "thy_decl_block";
    7.40  val thy_load = kind "thy_load";
    7.41 @@ -105,9 +96,6 @@
    7.42  val qed_script = kind "qed_script";
    7.43  val qed_block = kind "qed_block";
    7.44  val qed_global = kind "qed_global";
    7.45 -val prf_heading2 = kind "prf_heading2";
    7.46 -val prf_heading3 = kind "prf_heading3";
    7.47 -val prf_heading4 = kind "prf_heading4";
    7.48  val prf_goal = kind "prf_goal";
    7.49  val prf_block = kind "prf_block";
    7.50  val prf_open = kind "prf_open";
    7.51 @@ -120,10 +108,9 @@
    7.52  val prf_script = kind "prf_script";
    7.53  
    7.54  val kinds =
    7.55 -  [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    7.56 -    thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global,
    7.57 -    prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
    7.58 -    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    7.59 +  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
    7.60 +    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
    7.61 +    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    7.62  
    7.63  
    7.64  (* tags *)
    7.65 @@ -235,30 +222,25 @@
    7.66  
    7.67  val is_diag = command_category [diag];
    7.68  
    7.69 -val is_heading =
    7.70 -  command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    7.71 -    prf_heading2, prf_heading3, prf_heading4];
    7.72 +val is_heading = command_category [heading];
    7.73  
    7.74  val is_theory_begin = command_category [thy_begin];
    7.75  
    7.76  val is_theory_load = command_category [thy_load];
    7.77  
    7.78  val is_theory = command_category
    7.79 -  [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    7.80 -    thy_load, thy_decl, thy_decl_block, thy_goal];
    7.81 +  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];
    7.82  
    7.83  val is_theory_body = command_category
    7.84 -  [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    7.85 -    thy_load, thy_decl, thy_decl_block, thy_goal];
    7.86 +  [thy_load, thy_decl, thy_decl_block, thy_goal];
    7.87  
    7.88  val is_proof = command_category
    7.89 -  [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
    7.90 -    prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
    7.91 -    prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    7.92 +  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
    7.93 +    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    7.94  
    7.95  val is_proof_body = command_category
    7.96 -  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain,
    7.97 -    prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    7.98 +  [diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm,
    7.99 +    prf_asm_goal, prf_asm_goal_script, prf_script];
   7.100  
   7.101  val is_theory_goal = command_category [thy_goal];
   7.102  val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
     8.1 --- a/src/Pure/Isar/keyword.scala	Sun Nov 02 13:26:20 2014 +0100
     8.2 +++ b/src/Pure/Isar/keyword.scala	Sun Nov 02 15:27:37 2014 +0100
     8.3 @@ -13,12 +13,9 @@
     8.4  
     8.5    val MINOR = "minor"
     8.6    val DIAG = "diag"
     8.7 +  val HEADING = "heading"
     8.8    val THY_BEGIN = "thy_begin"
     8.9    val THY_END = "thy_end"
    8.10 -  val THY_HEADING1 = "thy_heading1"
    8.11 -  val THY_HEADING2 = "thy_heading2"
    8.12 -  val THY_HEADING3 = "thy_heading3"
    8.13 -  val THY_HEADING4 = "thy_heading4"
    8.14    val THY_DECL = "thy_decl"
    8.15    val THY_DECL_BLOCK = "thy_decl_block"
    8.16    val THY_LOAD = "thy_load"
    8.17 @@ -27,9 +24,6 @@
    8.18    val QED_SCRIPT = "qed_script"
    8.19    val QED_BLOCK = "qed_block"
    8.20    val QED_GLOBAL = "qed_global"
    8.21 -  val PRF_HEADING2 = "prf_heading2"
    8.22 -  val PRF_HEADING3 = "prf_heading3"
    8.23 -  val PRF_HEADING4 = "prf_heading4"
    8.24    val PRF_GOAL = "prf_goal"
    8.25    val PRF_BLOCK = "prf_block"
    8.26    val PRF_OPEN = "prf_open"
    8.27 @@ -46,26 +40,21 @@
    8.28  
    8.29    val diag = Set(DIAG)
    8.30  
    8.31 -  val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
    8.32 -    PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
    8.33 +  val heading = Set(HEADING)
    8.34  
    8.35 -  val theory =
    8.36 -    Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
    8.37 -      THY_LOAD, THY_DECL, THY_GOAL)
    8.38 +  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
    8.39  
    8.40    val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
    8.41  
    8.42 -  val theory_body =
    8.43 -    Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL)
    8.44 +  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
    8.45  
    8.46    val proof =
    8.47 -    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
    8.48 -      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL,
    8.49 -      PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    8.50 +    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
    8.51 +      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    8.52  
    8.53    val proof_body =
    8.54 -    Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN,
    8.55 -      PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    8.56 +    Set(DIAG, HEADING, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM,
    8.57 +      PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
    8.58  
    8.59    val theory_goal = Set(THY_GOAL)
    8.60    val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
     9.1 --- a/src/Pure/Isar/outer_syntax.scala	Sun Nov 02 13:26:20 2014 +0100
     9.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Nov 02 15:27:37 2014 +0100
     9.3 @@ -277,14 +277,16 @@
     9.4  
     9.5    def heading_level(command: Command): Option[Int] =
     9.6    {
     9.7 -    keyword_kind(command.name) match {
     9.8 -      case _ if command.name == "header" => Some(0)
     9.9 -      case Some(Keyword.THY_HEADING1) => Some(1)
    9.10 -      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
    9.11 -      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
    9.12 -      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
    9.13 -      case Some(kind) if Keyword.theory(kind) => Some(5)
    9.14 -      case _ => None
    9.15 +    command.name match {
    9.16 +      case "chapter" => Some(0)
    9.17 +      case "section" | "header" => Some(1)
    9.18 +      case "subsection" => Some(2)
    9.19 +      case "subsubsection" => Some(3)
    9.20 +      case _ =>
    9.21 +        keyword_kind(command.name) match {
    9.22 +          case Some(kind) if Keyword.theory(kind) => Some(4)
    9.23 +          case _ => None
    9.24 +        }
    9.25      }
    9.26    }
    9.27  
    10.1 --- a/src/Pure/Pure.thy	Sun Nov 02 13:26:20 2014 +0100
    10.2 +++ b/src/Pure/Pure.thy	Sun Nov 02 15:27:37 2014 +0100
    10.3 @@ -14,15 +14,12 @@
    10.4      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
    10.5      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
    10.6    and "theory" :: thy_begin % "theory"
    10.7 -  and "header" :: diag
    10.8 -  and "chapter" :: thy_heading1
    10.9 -  and "section" :: thy_heading2
   10.10 -  and "subsection" :: thy_heading3
   10.11 -  and "subsubsection" :: thy_heading4
   10.12 +  and "header" :: heading
   10.13 +  and "chapter" :: heading
   10.14 +  and "section" :: heading
   10.15 +  and "subsection" :: heading
   10.16 +  and "subsubsection" :: heading
   10.17    and "text" "text_raw" :: thy_decl
   10.18 -  and "sect" :: prf_heading2 % "proof"
   10.19 -  and "subsect" :: prf_heading3 % "proof"
   10.20 -  and "subsubsect" :: prf_heading4 % "proof"
   10.21    and "txt" "txt_raw" :: prf_decl % "proof"
   10.22    and "default_sort" :: thy_decl == ""
   10.23    and "typedecl" "type_synonym" "nonterminal" "judgment"
    11.1 --- a/src/Pure/System/options.scala	Sun Nov 02 13:26:20 2014 +0100
    11.2 +++ b/src/Pure/System/options.scala	Sun Nov 02 15:27:37 2014 +0100
    11.3 @@ -76,7 +76,7 @@
    11.4  
    11.5    lazy val options_syntax =
    11.6      Outer_Syntax.init() + ":" + "=" + "--" +
    11.7 -      (SECTION, Keyword.THY_HEADING2) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
    11.8 +      (SECTION, Keyword.HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
    11.9  
   11.10    lazy val prefs_syntax = Outer_Syntax.init() + "="
   11.11  
    12.1 --- a/src/Pure/Thy/thy_header.ML	Sun Nov 02 13:26:20 2014 +0100
    12.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Nov 02 15:27:37 2014 +0100
    12.3 @@ -67,6 +67,11 @@
    12.4  (* header keywords *)
    12.5  
    12.6  val headerN = "header";
    12.7 +val chapterN = "chapter";
    12.8 +val sectionN = "section";
    12.9 +val subsectionN = "subsection";
   12.10 +val subsubsectionN = "subsubsection";
   12.11 +
   12.12  val theoryN = "theory";
   12.13  val importsN = "imports";
   12.14  val keywordsN = "keywords";
   12.15 @@ -75,7 +80,7 @@
   12.16  val header_lexicons =
   12.17    pairself (Scan.make_lexicon o map Symbol.explode)
   12.18     (["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN],
   12.19 -    [headerN, theoryN]);
   12.20 +    [headerN, chapterN, sectionN, subsectionN, subsubsectionN, theoryN]);
   12.21  
   12.22  
   12.23  (* header args *)
   12.24 @@ -118,10 +123,16 @@
   12.25  
   12.26  (* read header *)
   12.27  
   12.28 +val heading =
   12.29 +  (Parse.command_name headerN ||
   12.30 +    Parse.command_name chapterN ||
   12.31 +    Parse.command_name sectionN ||
   12.32 +    Parse.command_name subsectionN ||
   12.33 +    Parse.command_name subsubsectionN) --
   12.34 +  Parse.tags -- Parse.!!! Parse.document_source;
   12.35 +
   12.36  val header =
   12.37 -  (Parse.command_name headerN -- Parse.tags) |--
   12.38 -    (Parse.!!! (Parse.document_source -- (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
   12.39 -  (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
   12.40 +  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
   12.41  
   12.42  fun token_source pos str =
   12.43    str
    13.1 --- a/src/Pure/Thy/thy_header.scala	Sun Nov 02 13:26:20 2014 +0100
    13.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Nov 02 15:27:37 2014 +0100
    13.3 @@ -16,6 +16,11 @@
    13.4  object Thy_Header extends Parse.Parser
    13.5  {
    13.6    val HEADER = "header"
    13.7 +  val CHAPTER = "chapter"
    13.8 +  val SECTION = "section"
    13.9 +  val SUBSECTION = "subsection"
   13.10 +  val SUBSUBSECTION = "subsubsection"
   13.11 +
   13.12    val THEORY = "theory"
   13.13    val IMPORTS = "imports"
   13.14    val KEYWORDS = "keywords"
   13.15 @@ -23,8 +28,8 @@
   13.16    val BEGIN = "begin"
   13.17  
   13.18    private val lexicon =
   13.19 -    Scan.Lexicon("%", "(", ")", ",", "::", "==",
   13.20 -      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
   13.21 +    Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN,
   13.22 +      HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY)
   13.23  
   13.24  
   13.25    /* theory file name */
   13.26 @@ -74,9 +79,15 @@
   13.27        keyword(BEGIN) ^^
   13.28        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
   13.29  
   13.30 -    (keyword(HEADER) ~ tags) ~!
   13.31 -      ((document_source ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
   13.32 -    (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   13.33 +    val heading =
   13.34 +      (keyword(HEADER) |
   13.35 +        keyword(CHAPTER) |
   13.36 +        keyword(SECTION) |
   13.37 +        keyword(SUBSECTION) |
   13.38 +        keyword(SUBSUBSECTION)) ~
   13.39 +      tags ~! document_source
   13.40 +
   13.41 +    (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   13.42    }
   13.43  
   13.44