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