--- 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 ***
--- 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)
--- 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 ||
--- 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) |
--- 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 =>
--- 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});