prefer internal tool;
authorwenzelm
Sun Apr 03 23:01:39 2016 +0200 (2016-04-03)
changeset 6283698dbed6cfa44
parent 62835 1a9ce1b13b20
child 62837 237ef2bab6c7
prefer internal tool;
lib/Tools/update_cartouches
lib/Tools/update_header
lib/Tools/update_then
lib/Tools/update_theorems
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/update_cartouches.scala
src/Pure/Tools/update_header.scala
src/Pure/Tools/update_then.scala
src/Pure/Tools/update_theorems.scala
     1.1 --- a/lib/Tools/update_cartouches	Sun Apr 03 22:54:31 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,9 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# DESCRIPTION: update theory syntax to use cartouches
     1.9 -
    1.10 -isabelle_admin_build jars || exit $?
    1.11 -
    1.12 -exec isabelle java isabelle.Update_Cartouches "$@"
     2.1 --- a/lib/Tools/update_header	Sun Apr 03 22:54:31 2016 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,9 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Makarius
     2.7 -#
     2.8 -# DESCRIPTION: replace obsolete theory header command
     2.9 -
    2.10 -isabelle_admin_build jars || exit $?
    2.11 -
    2.12 -exec isabelle java isabelle.Update_Header "$@"
     3.1 --- a/lib/Tools/update_then	Sun Apr 03 22:54:31 2016 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,9 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# Author: Makarius
     3.7 -#
     3.8 -# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
     3.9 -
    3.10 -isabelle_admin_build jars || exit $?
    3.11 -
    3.12 -exec isabelle java isabelle.Update_Then "$@"
     4.1 --- a/lib/Tools/update_theorems	Sun Apr 03 22:54:31 2016 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,9 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Author: Makarius
     4.7 -#
     4.8 -# DESCRIPTION: update toplevel theorem keywords
     4.9 -
    4.10 -isabelle_admin_build jars || exit $?
    4.11 -
    4.12 -exec isabelle java isabelle.Update_Theorems "$@"
     5.1 --- a/src/Pure/System/isabelle_tool.scala	Sun Apr 03 22:54:31 2016 +0200
     5.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Apr 03 23:01:39 2016 +0200
     5.3 @@ -73,6 +73,10 @@
     5.4    register(Doc.isabelle_tool)
     5.5    register(ML_Process.isabelle_tool)
     5.6    register(Options.isabelle_tool)
     5.7 +  register(Update_Cartouches.isabelle_tool)
     5.8 +  register(Update_Header.isabelle_tool)
     5.9 +  register(Update_Then.isabelle_tool)
    5.10 +  register(Update_Theorems.isabelle_tool)
    5.11  
    5.12  
    5.13    /* command line entry point */
     6.1 --- a/src/Pure/Tools/update_cartouches.scala	Sun Apr 03 22:54:31 2016 +0200
     6.2 +++ b/src/Pure/Tools/update_cartouches.scala	Sun Apr 03 23:01:39 2016 +0200
     6.3 @@ -82,11 +82,11 @@
     6.4    }
     6.5  
     6.6  
     6.7 -  /* command line entry point */
     6.8 +  /* Isabelle tool wrapper */
     6.9  
    6.10 -  def main(args: Array[String])
    6.11 -  {
    6.12 -    Command_Line.tool0 {
    6.13 +  val isabelle_tool =
    6.14 +    Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
    6.15 +    {
    6.16        var replace_comment = false
    6.17        var replace_text = false
    6.18  
    6.19 @@ -112,6 +112,5 @@
    6.20          spec <- specs
    6.21          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    6.22        } update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
    6.23 -    }
    6.24 -  }
    6.25 +    })
    6.26  }
     7.1 --- a/src/Pure/Tools/update_header.scala	Sun Apr 03 22:54:31 2016 +0200
     7.2 +++ b/src/Pure/Tools/update_header.scala	Sun Apr 03 23:01:39 2016 +0200
     7.3 @@ -23,14 +23,14 @@
     7.4    }
     7.5  
     7.6  
     7.7 -  /* command line entry point */
     7.8 +  /* Isabelle tool wrapper */
     7.9  
    7.10    private val headings =
    7.11      Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
    7.12  
    7.13 -  def main(args: Array[String])
    7.14 -  {
    7.15 -    Command_Line.tool0 {
    7.16 +  val isabelle_tool =
    7.17 +    Isabelle_Tool("update_header", "replace obsolete theory header command", args =>
    7.18 +    {
    7.19        var section = "section"
    7.20  
    7.21        val getopts = Getopts("""
    7.22 @@ -57,6 +57,5 @@
    7.23          spec <- specs
    7.24          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    7.25        } update_header(section, Path.explode(File.standard_path(file)))
    7.26 -    }
    7.27 -  }
    7.28 +    })
    7.29  }
     8.1 --- a/src/Pure/Tools/update_then.scala	Sun Apr 03 22:54:31 2016 +0200
     8.2 +++ b/src/Pure/Tools/update_then.scala	Sun Apr 03 23:01:39 2016 +0200
     8.3 @@ -28,11 +28,11 @@
     8.4    }
     8.5  
     8.6  
     8.7 -  /* command line entry point */
     8.8 +  /* Isabelle tool wrapper */
     8.9  
    8.10 -  def main(args: Array[String])
    8.11 -  {
    8.12 -    Command_Line.tool0 {
    8.13 +  val isabelle_tool =
    8.14 +    Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'", args =>
    8.15 +    {
    8.16        val getopts = Getopts("""
    8.17  Usage: isabelle update_then [FILES|DIRS...]
    8.18  
    8.19 @@ -51,6 +51,5 @@
    8.20          spec <- specs
    8.21          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    8.22        } update_then(Path.explode(File.standard_path(file)))
    8.23 -    }
    8.24 -  }
    8.25 +    })
    8.26  }
     9.1 --- a/src/Pure/Tools/update_theorems.scala	Sun Apr 03 22:54:31 2016 +0200
     9.2 +++ b/src/Pure/Tools/update_theorems.scala	Sun Apr 03 23:01:39 2016 +0200
     9.3 @@ -29,12 +29,11 @@
     9.4    }
     9.5  
     9.6  
     9.7 -  /* command line entry point */
     9.8 +  /* Isabelle tool wrapper */
     9.9  
    9.10 -  def main(args: Array[String])
    9.11 +  val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
    9.12    {
    9.13 -    Command_Line.tool0 {
    9.14 -      val getopts = Getopts("""
    9.15 +    val getopts = Getopts("""
    9.16  Usage: isabelle update_theorems [FILES|DIRS...]
    9.17  
    9.18    Recursively find .thy files and update toplevel theorem keywords:
    9.19 @@ -47,13 +46,12 @@
    9.20    Old versions of files are preserved by appending "~~".
    9.21  """)
    9.22  
    9.23 -      val specs = getopts(args)
    9.24 -      if (specs.isEmpty) getopts.usage()
    9.25 +    val specs = getopts(args)
    9.26 +    if (specs.isEmpty) getopts.usage()
    9.27  
    9.28 -      for {
    9.29 -        spec <- specs
    9.30 -        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    9.31 -      } update_theorems(Path.explode(File.standard_path(file)))
    9.32 -    }
    9.33 -  }
    9.34 +    for {
    9.35 +      spec <- specs
    9.36 +      file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    9.37 +    } update_theorems(Path.explode(File.standard_path(file)))
    9.38 +  })
    9.39  }