# HG changeset patch # User wenzelm # Date 1414938457 -3600 # Node ID c5e1cce7ace33dadd4e04ba52b2d2c32f181329a # Parent 911addd19e9fbe7cd4922c2cd18d103c44f8385d uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy; diff -r 911addd19e9f -r c5e1cce7ace3 NEWS --- a/NEWS Sun Nov 02 13:26:20 2014 +0100 +++ b/NEWS Sun Nov 02 15:27:37 2014 +0100 @@ -167,6 +167,13 @@ *** 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. Minor INCOMPATIBILITY. + * Official support for "tt" style variants, via \isatt{...} or \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or verbatim environment of LaTeX is no longer used. This allows @{ML} etc. diff -r 911addd19e9f -r c5e1cce7ace3 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Sun Nov 02 13:26:20 2014 +0100 +++ b/lib/texinputs/isabelle.sty Sun Nov 02 15:27:37 2014 +0100 @@ -127,9 +127,6 @@ \newcommand{\isamarkupsection}[1]{\section{#1}} \newcommand{\isamarkupsubsection}[1]{\subsection{#1}} \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} -\newcommand{\isamarkupsect}[1]{\section{#1}} -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}} -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} \newif\ifisamarkup \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} diff -r 911addd19e9f -r c5e1cce7ace3 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Nov 02 15:27:37 2014 +0100 @@ -22,16 +22,12 @@ text \ \begin{matharray}{rcl} - @{command_def "header"} & : & @{text "toplevel \ toplevel"} \\[0.5ex] - @{command_def "chapter"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "section"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "subsection"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "subsubsection"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "chapter"} & : & @{text "any \ any"} \\ + @{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 "sect"} & : & @{text "proof \ proof"} \\ - @{command_def "subsect"} & : & @{text "proof \ proof"} \\ - @{command_def "subsubsect"} & : & @{text "proof \ proof"} \\ @{command_def "txt"} & : & @{text "proof \ proof"} \\ @{command_def "txt_raw"} & : & @{text "proof \ proof"} \\ \end{matharray} @@ -51,26 +47,17 @@ (@@{command chapter} | @@{command section} | @@{command subsection} | @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text} ; - (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} | - @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text} + (@@{command text_raw} | @@{command txt} | @@{command txt_raw}) @{syntax text} \} \begin{description} - \item @{command header} provides plain text markup just preceding - the formal beginning of a theory. The corresponding {\LaTeX} macro - is @{verbatim \\isamarkupheader\}, which acts like @{command - section} by default. - - \item @{command chapter}, @{command section}, @{command subsection}, - and @{command subsubsection} mark chapter and section headings - within the main theory body or local theory targets. The - corresponding {\LaTeX} macros are @{verbatim \\isamarkupchapter\}, - @{verbatim \\isamarkupsection\}, @{verbatim \\isamarkupsubsection\} etc. - - \item @{command sect}, @{command subsect}, and @{command subsubsect} - mark section headings within proofs. The corresponding {\LaTeX} - macros are @{verbatim \\isamarkupsect\}, @{verbatim \\isamarkupsubsect\} etc. + \item @{command chapter}, @{command section}, @{command subsection}, and + @{command subsubsection} mark chapter and section headings within the + theory source; this works in any context, even before the initial + @{command theory} command. The corresponding {\LaTeX} macros are + @{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 @@ -91,8 +78,7 @@ \medskip The proof markup commands closely resemble those for theory specifications, but have a different formal status and produce - different {\LaTeX} macros. The default definitions coincide for - analogous commands such as @{command section} and @{command sect}. + different {\LaTeX} macros. \ diff -r 911addd19e9f -r c5e1cce7ace3 src/Doc/Tutorial/Documents/Documents.thy --- a/src/Doc/Tutorial/Documents/Documents.thy Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Doc/Tutorial/Documents/Documents.thy Sun Nov 02 15:27:37 2014 +0100 @@ -424,24 +424,6 @@ do not affect the formal meaning of a theory (or proof), but result in corresponding {\LaTeX} elements. - There are separate markup commands depending on the textual context: - in header position (just before \isakeyword{theory}), within the - theory body, or within a proof. The header needs to be treated - specially here, since ordinary theory and proof commands may only - occur \emph{after} the initial \isakeyword{theory} specification. - - \medskip - - \begin{tabular}{llll} - header & theory & proof & default meaning \\\hline - & \commdx{chapter} & & \verb,\chapter, \\ - \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\ - & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\ - & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\ - \end{tabular} - - \medskip - From the Isabelle perspective, each markup command takes a single $text$ argument (delimited by \verb,",~@{text \}~\verb,", or \verb,{,\verb,*,~@{text \}~\verb,*,\verb,},). After stripping any diff -r 911addd19e9f -r c5e1cce7ace3 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 02 15:27:37 2014 +0100 @@ -48,10 +48,11 @@ val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition val print_type: (string list * (string * string option)) -> Toplevel.transition -> Toplevel.transition - val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition - val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) -> + 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 heading_markup: (xstring * Position.T) option * Symbol_Pos.source -> + Toplevel.transition -> Toplevel.transition end; structure Isar_Cmd: ISAR_CMD = @@ -377,11 +378,21 @@ (* markup commands *) -fun header_markup txt = Toplevel.keep (fn state => - if Toplevel.is_toplevel state then Thy_Output.check_text txt state - else raise Toplevel.UNDEF); - fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt); val proof_markup = Toplevel.present_proof o Thy_Output.check_text; +fun reject_target NONE = () + | reject_target (SOME (_, pos)) = + error ("Illegal target specification -- not a theory context" ^ Position.here pos); + +fun heading_markup (loc, txt) = + Toplevel.keep (fn state => + if Toplevel.is_toplevel state then + (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead"; + reject_target loc; + Thy_Output.check_text txt state) + else raise Toplevel.UNDEF) o + local_theory_markup (loc, txt) o + Toplevel.present_proof (fn state => (reject_target loc; Thy_Output.check_text txt state)); + end; diff -r 911addd19e9f -r c5e1cce7ace3 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sun Nov 02 15:27:37 2014 +0100 @@ -12,27 +12,27 @@ val _ = Outer_Syntax.markup_command Thy_Output.Markup @{command_spec "header"} "theory header" - (Parse.document_source >> Isar_Cmd.header_markup); + (Parse.document_source >> (fn s => Isar_Cmd.heading_markup (NONE, s))); val _ = Outer_Syntax.markup_command Thy_Output.Markup @{command_spec "chapter"} "chapter heading" - (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup); + (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); val _ = Outer_Syntax.markup_command Thy_Output.Markup @{command_spec "section"} "section heading" - (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup); + (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); val _ = Outer_Syntax.markup_command Thy_Output.Markup @{command_spec "subsection"} "subsection heading" - (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup); + (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); val _ = Outer_Syntax.markup_command Thy_Output.Markup @{command_spec "subsubsection"} "subsubsection heading" - (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup); + (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup); val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv @@ -45,21 +45,6 @@ (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup); val _ = - Outer_Syntax.markup_command Thy_Output.Markup - @{command_spec "sect"} "formal comment (proof)" - (Parse.document_source >> Isar_Cmd.proof_markup); - -val _ = - Outer_Syntax.markup_command Thy_Output.Markup - @{command_spec "subsect"} "formal comment (proof)" - (Parse.document_source >> Isar_Cmd.proof_markup); - -val _ = - Outer_Syntax.markup_command Thy_Output.Markup - @{command_spec "subsubsect"} "formal comment (proof)" - (Parse.document_source >> Isar_Cmd.proof_markup); - -val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv @{command_spec "txt"} "formal comment (proof)" (Parse.document_source >> Isar_Cmd.proof_markup); diff -r 911addd19e9f -r c5e1cce7ace3 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Isar/keyword.ML Sun Nov 02 15:27:37 2014 +0100 @@ -10,12 +10,9 @@ val kind_of: T -> string val kind_files_of: T -> string * string list val diag: T + val heading: T val thy_begin: T val thy_end: T - val thy_heading1: T - val thy_heading2: T - val thy_heading3: T - val thy_heading4: T val thy_decl: T val thy_decl_block: T val thy_load: T @@ -25,9 +22,6 @@ val qed_script: T val qed_block: T val qed_global: T - val prf_heading2: T - val prf_heading3: T - val prf_heading4: T val prf_goal: T val prf_block: T val prf_open: T @@ -90,12 +84,9 @@ (* kinds *) val diag = kind "diag"; +val heading = kind "heading"; val thy_begin = kind "thy_begin"; val thy_end = kind "thy_end"; -val thy_heading1 = kind "thy_heading1"; -val thy_heading2 = kind "thy_heading2"; -val thy_heading3 = kind "thy_heading3"; -val thy_heading4 = kind "thy_heading4"; val thy_decl = kind "thy_decl"; val thy_decl_block = kind "thy_decl_block"; val thy_load = kind "thy_load"; @@ -105,9 +96,6 @@ val qed_script = kind "qed_script"; val qed_block = kind "qed_block"; val qed_global = kind "qed_global"; -val prf_heading2 = kind "prf_heading2"; -val prf_heading3 = kind "prf_heading3"; -val prf_heading4 = kind "prf_heading4"; val prf_goal = kind "prf_goal"; val prf_block = kind "prf_block"; val prf_open = kind "prf_open"; @@ -120,10 +108,9 @@ val prf_script = kind "prf_script"; val kinds = - [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4, - thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, - prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open, - prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]; + [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]; (* tags *) @@ -235,30 +222,25 @@ val is_diag = command_category [diag]; -val is_heading = - command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4, - prf_heading2, prf_heading3, prf_heading4]; +val is_heading = command_category [heading]; val is_theory_begin = command_category [thy_begin]; val is_theory_load = command_category [thy_load]; val is_theory = command_category - [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4, - thy_load, thy_decl, thy_decl_block, thy_goal]; + [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal]; val is_theory_body = command_category - [thy_heading1, thy_heading2, thy_heading3, thy_heading4, - thy_load, thy_decl, thy_decl_block, thy_goal]; + [thy_load, thy_decl, thy_decl_block, thy_goal]; val is_proof = command_category - [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4, - prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl, - prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]; + [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]; val is_proof_body = command_category - [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain, - prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]; + [diag, heading, 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 911addd19e9f -r c5e1cce7ace3 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Isar/keyword.scala Sun Nov 02 15:27:37 2014 +0100 @@ -13,12 +13,9 @@ val MINOR = "minor" val DIAG = "diag" + val HEADING = "heading" val THY_BEGIN = "thy_begin" val THY_END = "thy_end" - val THY_HEADING1 = "thy_heading1" - val THY_HEADING2 = "thy_heading2" - val THY_HEADING3 = "thy_heading3" - val THY_HEADING4 = "thy_heading4" val THY_DECL = "thy_decl" val THY_DECL_BLOCK = "thy_decl_block" val THY_LOAD = "thy_load" @@ -27,9 +24,6 @@ val QED_SCRIPT = "qed_script" val QED_BLOCK = "qed_block" val QED_GLOBAL = "qed_global" - val PRF_HEADING2 = "prf_heading2" - val PRF_HEADING3 = "prf_heading3" - val PRF_HEADING4 = "prf_heading4" val PRF_GOAL = "prf_goal" val PRF_BLOCK = "prf_block" val PRF_OPEN = "prf_open" @@ -46,26 +40,21 @@ val diag = Set(DIAG) - val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, - PRF_HEADING2, PRF_HEADING3, PRF_HEADING4) + val heading = Set(HEADING) - val theory = - Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, - THY_LOAD, THY_DECL, THY_GOAL) + val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK) - val theory_body = - Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL) + val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL) val proof = - Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, - PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL, - PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) + Set(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) val proof_body = - Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, - PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT) + Set(DIAG, HEADING, 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 911addd19e9f -r c5e1cce7ace3 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Sun Nov 02 15:27:37 2014 +0100 @@ -277,14 +277,16 @@ def heading_level(command: Command): Option[Int] = { - keyword_kind(command.name) match { - case _ if command.name == "header" => Some(0) - case Some(Keyword.THY_HEADING1) => Some(1) - case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2) - case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3) - case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4) - case Some(kind) if Keyword.theory(kind) => Some(5) - case _ => None + command.name match { + case "chapter" => Some(0) + case "section" | "header" => Some(1) + case "subsection" => Some(2) + case "subsubsection" => Some(3) + case _ => + keyword_kind(command.name) match { + case Some(kind) if Keyword.theory(kind) => Some(4) + case _ => None + } } } diff -r 911addd19e9f -r c5e1cce7ace3 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Pure.thy Sun Nov 02 15:27:37 2014 +0100 @@ -14,15 +14,12 @@ "infixr" "is" "keywords" "notes" "obtains" "open" "output" "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" and "theory" :: thy_begin % "theory" - and "header" :: diag - and "chapter" :: thy_heading1 - and "section" :: thy_heading2 - and "subsection" :: thy_heading3 - and "subsubsection" :: thy_heading4 + and "header" :: heading + and "chapter" :: heading + and "section" :: heading + and "subsection" :: heading + and "subsubsection" :: heading and "text" "text_raw" :: thy_decl - and "sect" :: prf_heading2 % "proof" - and "subsect" :: prf_heading3 % "proof" - and "subsubsect" :: prf_heading4 % "proof" and "txt" "txt_raw" :: prf_decl % "proof" and "default_sort" :: thy_decl == "" and "typedecl" "type_synonym" "nonterminal" "judgment" diff -r 911addd19e9f -r c5e1cce7ace3 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/System/options.scala Sun Nov 02 15:27:37 2014 +0100 @@ -76,7 +76,7 @@ lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + - (SECTION, Keyword.THY_HEADING2) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL) + (SECTION, Keyword.HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL) lazy val prefs_syntax = Outer_Syntax.init() + "=" diff -r 911addd19e9f -r c5e1cce7ace3 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Thy/thy_header.ML Sun Nov 02 15:27:37 2014 +0100 @@ -67,6 +67,11 @@ (* header keywords *) val headerN = "header"; +val chapterN = "chapter"; +val sectionN = "section"; +val subsectionN = "subsection"; +val subsubsectionN = "subsubsection"; + val theoryN = "theory"; val importsN = "imports"; val keywordsN = "keywords"; @@ -75,7 +80,7 @@ val header_lexicons = pairself (Scan.make_lexicon o map Symbol.explode) (["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN], - [headerN, theoryN]); + [headerN, chapterN, sectionN, subsectionN, subsubsectionN, theoryN]); (* header args *) @@ -118,10 +123,16 @@ (* read header *) +val heading = + (Parse.command_name headerN || + Parse.command_name chapterN || + Parse.command_name sectionN || + Parse.command_name subsectionN || + Parse.command_name subsubsectionN) -- + Parse.tags -- Parse.!!! Parse.document_source; + val header = - (Parse.command_name headerN -- Parse.tags) |-- - (Parse.!!! (Parse.document_source -- (Parse.command_name theoryN -- Parse.tags) |-- args)) || - (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args; + (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args; fun token_source pos str = str diff -r 911addd19e9f -r c5e1cce7ace3 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sun Nov 02 13:26:20 2014 +0100 +++ b/src/Pure/Thy/thy_header.scala Sun Nov 02 15:27:37 2014 +0100 @@ -16,6 +16,11 @@ object Thy_Header extends Parse.Parser { val HEADER = "header" + val CHAPTER = "chapter" + val SECTION = "section" + val SUBSECTION = "subsection" + val SUBSUBSECTION = "subsubsection" + val THEORY = "theory" val IMPORTS = "imports" val KEYWORDS = "keywords" @@ -23,8 +28,8 @@ val BEGIN = "begin" private val lexicon = - Scan.Lexicon("%", "(", ")", ",", "::", "==", - AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY) + Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN, + HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY) /* theory file name */ @@ -74,9 +79,15 @@ keyword(BEGIN) ^^ { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } - (keyword(HEADER) ~ tags) ~! - ((document_source ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | - (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } + val heading = + (keyword(HEADER) | + keyword(CHAPTER) | + keyword(SECTION) | + keyword(SUBSECTION) | + keyword(SUBSUBSECTION)) ~ + tags ~! document_source + + (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x } }