# 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 \<circle>, 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});