--- a/lib/Tools/update_cartouches Sun Apr 03 22:54:31 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update theory syntax to use cartouches
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Cartouches "$@"
--- a/lib/Tools/update_header Sun Apr 03 22:54:31 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: replace obsolete theory header command
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Header "$@"
--- a/lib/Tools/update_then Sun Apr 03 22:54:31 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Then "$@"
--- a/lib/Tools/update_theorems Sun Apr 03 22:54:31 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update toplevel theorem keywords
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Theorems "$@"
--- a/src/Pure/System/isabelle_tool.scala Sun Apr 03 22:54:31 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sun Apr 03 23:01:39 2016 +0200
@@ -73,6 +73,10 @@
register(Doc.isabelle_tool)
register(ML_Process.isabelle_tool)
register(Options.isabelle_tool)
+ register(Update_Cartouches.isabelle_tool)
+ register(Update_Header.isabelle_tool)
+ register(Update_Then.isabelle_tool)
+ register(Update_Theorems.isabelle_tool)
/* command line entry point */
--- a/src/Pure/Tools/update_cartouches.scala Sun Apr 03 22:54:31 2016 +0200
+++ b/src/Pure/Tools/update_cartouches.scala Sun Apr 03 23:01:39 2016 +0200
@@ -82,11 +82,11 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
- {
- Command_Line.tool0 {
+ val isabelle_tool =
+ Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
+ {
var replace_comment = false
var replace_text = false
@@ -112,6 +112,5 @@
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
} update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
- }
- }
+ })
}
--- a/src/Pure/Tools/update_header.scala Sun Apr 03 22:54:31 2016 +0200
+++ b/src/Pure/Tools/update_header.scala Sun Apr 03 23:01:39 2016 +0200
@@ -23,14 +23,14 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
private val headings =
Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
- def main(args: Array[String])
- {
- Command_Line.tool0 {
+ val isabelle_tool =
+ Isabelle_Tool("update_header", "replace obsolete theory header command", args =>
+ {
var section = "section"
val getopts = Getopts("""
@@ -57,6 +57,5 @@
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
} update_header(section, Path.explode(File.standard_path(file)))
- }
- }
+ })
}
--- a/src/Pure/Tools/update_then.scala Sun Apr 03 22:54:31 2016 +0200
+++ b/src/Pure/Tools/update_then.scala Sun Apr 03 23:01:39 2016 +0200
@@ -28,11 +28,11 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
- {
- Command_Line.tool0 {
+ val isabelle_tool =
+ Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'", args =>
+ {
val getopts = Getopts("""
Usage: isabelle update_then [FILES|DIRS...]
@@ -51,6 +51,5 @@
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
} update_then(Path.explode(File.standard_path(file)))
- }
- }
+ })
}
--- a/src/Pure/Tools/update_theorems.scala Sun Apr 03 22:54:31 2016 +0200
+++ b/src/Pure/Tools/update_theorems.scala Sun Apr 03 23:01:39 2016 +0200
@@ -29,12 +29,11 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
{
- Command_Line.tool0 {
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle update_theorems [FILES|DIRS...]
Recursively find .thy files and update toplevel theorem keywords:
@@ -47,13 +46,12 @@
Old versions of files are preserved by appending "~~".
""")
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
- for {
- spec <- specs
- file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_theorems(Path.explode(File.standard_path(file)))
- }
- }
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_theorems(Path.explode(File.standard_path(file)))
+ })
}