# HG changeset patch
# User wenzelm
# Date 1726487623 -7200
# Node ID 7631de7518fc3459952482f09f1a97b3bd16cc4d
# Parent  2cdb00f797b1fbd4ae347cebe018ed9ae515234e
obsolete (see also b93cc7d73431);

diff -r 2cdb00f797b1 -r 7631de7518fc etc/build.props
--- a/etc/build.props	Sun Sep 15 16:45:13 2024 +0200
+++ b/etc/build.props	Mon Sep 16 13:53:43 2024 +0200
@@ -233,7 +233,6 @@
   src/Pure/Tools/task_statistics.scala \
   src/Pure/Tools/update_cartouches.scala \
   src/Pure/Tools/update_comments.scala \
-  src/Pure/Tools/update_header.scala \
   src/Pure/Tools/update_then.scala \
   src/Pure/Tools/update_theorems.scala \
   src/Pure/Tools/update_tool.scala \
diff -r 2cdb00f797b1 -r 7631de7518fc src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Sun Sep 15 16:45:13 2024 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Mon Sep 16 13:53:43 2024 +0200
@@ -157,7 +157,6 @@
   Sync.isabelle_tool,
   Update_Cartouches.isabelle_tool,
   Update_Comments.isabelle_tool,
-  Update_Header.isabelle_tool,
   Update_Then.isabelle_tool,
   Update_Theorems.isabelle_tool,
   Update_Tool.isabelle_tool,
diff -r 2cdb00f797b1 -r 7631de7518fc src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Sun Sep 15 16:45:13 2024 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-/*  Title:      Pure/Tools/update_header.scala
-    Author:     Makarius
-
-Replace theory header command.
-*/
-
-package isabelle
-
-
-object Update_Header {
-  def update_header(section: String, path: Path): Unit = {
-    val text0 = File.read(path)
-    val text1 =
-      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
-        yield { if (tok.source == "header") section else tok.source }).mkString
-
-    if (text0 != text1) {
-      Output.writeln("changing " + path)
-      File.write_backup2(path, text1)
-    }
-  }
-
-
-  /* Isabelle tool wrapper */
-
-  private val headings =
-    Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
-
-  val isabelle_tool =
-    Isabelle_Tool("update_header", "replace obsolete theory header command",
-      Scala_Project.here,
-      { args =>
-        var section = "section"
-
-        val getopts = Getopts("""
-Usage: isabelle update_header [FILES|DIRS...]
-
-  Options are:
-    -s COMMAND   alternative heading command (default 'section')
-
-  Recursively find .thy files and replace obsolete theory header commands
-  by 'chapter', 'section' (default), 'subsection', 'subsubsection',
-  'paragraph', 'subparagraph'.
-
-  Old versions of files are preserved by appending "~~".
-""",
-          "s:" -> (arg => section = arg))
-
-        val specs = getopts(args)
-        if (specs.isEmpty) getopts.usage()
-
-        if (!headings.contains(section))
-          error("Bad heading command: " + quote(section))
-
-        for {
-          spec <- specs
-          file <- File.find_files(Path.explode(spec).file, file => File.is_thy(file.getName))
-        } update_header(section, File.path(file))
-      })
-}