# HG changeset patch # User wenzelm # Date 1456677440 -3600 # Node ID b93cc7d734313727aa55c8eed15cab23981382a2 # Parent f25b67245699a1da4e0a8a4089f0301c84f03f53 discontinued old 'header'; diff -r f25b67245699 -r b93cc7d73431 NEWS --- a/NEWS Sun Feb 28 15:57:03 2016 +0100 +++ b/NEWS Sun Feb 28 17:37:20 2016 +0100 @@ -11,6 +11,9 @@ * New symbol \, e.g. for temporal operator. +* Old 'header' command is no longer supported (legacy since +Isabelle2015). + *** Isar *** diff -r f25b67245699 -r b93cc7d73431 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Sun Feb 28 15:57:03 2016 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Sun Feb 28 17:37:20 2016 +0100 @@ -237,7 +237,7 @@ val name = command.span.name name match { case Thy_Header.CHAPTER => Some(0) - case Thy_Header.SECTION | Thy_Header.HEADER => Some(1) + case Thy_Header.SECTION => Some(1) case Thy_Header.SUBSECTION => Some(2) case Thy_Header.SUBSUBSECTION => Some(3) case Thy_Header.PARAGRAPH => Some(4) diff -r f25b67245699 -r b93cc7d73431 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Sun Feb 28 15:57:03 2016 +0100 +++ b/src/Pure/Thy/thy_header.ML Sun Feb 28 17:37:20 2016 +0100 @@ -42,8 +42,6 @@ (* bootstrap keywords *) -val headerN = "header"; (* FIXME legacy *) - val chapterN = "chapter"; val sectionN = "section"; val subsectionN = "subsection"; @@ -72,7 +70,6 @@ ((beginN, @{here}), NONE), ((importsN, @{here}), NONE), ((keywordsN, @{here}), NONE), - ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])), ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])), ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])), ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])), @@ -147,8 +144,7 @@ (* read header *) val heading = - (Parse.command headerN || - Parse.command chapterN || + (Parse.command chapterN || Parse.command sectionN || Parse.command subsectionN || Parse.command subsubsectionN || diff -r f25b67245699 -r b93cc7d73431 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sun Feb 28 15:57:03 2016 +0100 +++ b/src/Pure/Thy/thy_header.scala Sun Feb 28 17:37:20 2016 +0100 @@ -19,8 +19,6 @@ type Keywords = List[(String, Option[Keyword.Spec], Option[String])] - val HEADER = "header" /* FIXME legacy */ - val CHAPTER = "chapter" val SECTION = "section" val SUBSECTION = "subsection" @@ -49,7 +47,6 @@ (BEGIN, None, None), (IMPORTS, None, None), (KEYWORDS, None, 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), @@ -115,8 +112,7 @@ { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } val heading = - (command(HEADER) | - command(CHAPTER) | + (command(CHAPTER) | command(SECTION) | command(SUBSECTION) | command(SUBSUBSECTION) | diff -r f25b67245699 -r b93cc7d73431 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sun Feb 28 15:57:03 2016 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Feb 28 17:37:20 2016 +0100 @@ -35,7 +35,6 @@ val string_of_margin: Proof.context -> Pretty.T -> string val output: Proof.context -> Pretty.T list -> string val verbatim_text: Proof.context -> string -> string - val old_header_command: Input.source -> Toplevel.transition -> Toplevel.transition val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition end; @@ -647,14 +646,7 @@ -(** document commands **) - -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"; - ignore (output_text state {markdown = false} txt)) - else raise Toplevel.UNDEF); +(** document command **) fun document_command markdown (loc, txt) = Toplevel.keep (fn state => diff -r f25b67245699 -r b93cc7d73431 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Sun Feb 28 15:57:03 2016 +0100 +++ b/src/Pure/pure_syn.ML Sun Feb 28 17:37:20 2016 +0100 @@ -14,10 +14,6 @@ struct val _ = - Outer_Syntax.command ("header", @{here}) "theory header" - (Parse.document_source >> Thy_Output.old_header_command); - -val _ = Outer_Syntax.command ("chapter", @{here}) "chapter heading" (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = false});