# HG changeset patch
# User wenzelm
# Date 1459717299 -7200
# Node ID 98dbed6cfa44d74f845935904751961ddd0798eb
# Parent  1a9ce1b13b20467d2050126dd193bd6e23667e15
prefer internal tool;

diff -r 1a9ce1b13b20 -r 98dbed6cfa44 lib/Tools/update_cartouches
--- 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 "$@"
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 lib/Tools/update_header
--- 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 "$@"
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 lib/Tools/update_then
--- 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 "$@"
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 lib/Tools/update_theorems
--- 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 "$@"
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 src/Pure/System/isabelle_tool.scala
--- 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 */
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 src/Pure/Tools/update_cartouches.scala
--- 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)))
-    }
-  }
+    })
 }
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 src/Pure/Tools/update_header.scala
--- 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)))
-    }
-  }
+    })
 }
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 src/Pure/Tools/update_then.scala
--- 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)))
-    }
-  }
+    })
 }
diff -r 1a9ce1b13b20 -r 98dbed6cfa44 src/Pure/Tools/update_theorems.scala
--- 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)))
+  })
 }