added update_header tool;
authorwenzelm
Sun Nov 02 16:47:45 2014 +0100 (2014-11-02)
changeset 58872f0f623005324
parent 58871 c399ae4b836f
child 58873 db866dc081f8
added update_header tool;
NEWS
lib/Tools/update_header
src/Pure/Tools/update_header.scala
src/Pure/build-jars
     1.1 --- a/NEWS	Sun Nov 02 16:39:54 2014 +0100
     1.2 +++ b/NEWS	Sun Nov 02 16:47:45 2014 +0100
     1.3 @@ -172,7 +172,8 @@
     1.4  before the initial 'theory' command.  Obsolete proof commands 'sect',
     1.5  'subsect', 'subsubsect' have been discontinued.  The Obsolete 'header'
     1.6  command is still retained for some time, but should be replaced by
     1.7 -'chapter', 'section' etc. Minor INCOMPATIBILITY.
     1.8 +'chapter', 'section' etc. (using "isabelle update_header"). Minor
     1.9 +INCOMPATIBILITY.
    1.10  
    1.11  * Official support for "tt" style variants, via \isatt{...} or
    1.12  \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/update_header	Sun Nov 02 16:47:45 2014 +0100
     2.3 @@ -0,0 +1,60 @@
     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 +
    2.11 +## diagnostics
    2.12 +
    2.13 +PRG="$(basename "$0")"
    2.14 +
    2.15 +function usage()
    2.16 +{
    2.17 +  echo
    2.18 +  echo "Usage: isabelle $PRG [FILES|DIRS...]"
    2.19 +  echo
    2.20 +  echo "  Options are:"
    2.21 +  echo "    -s COMMAND   alternative heading command (default 'section')"
    2.22 +  echo
    2.23 +  echo "  Recursively find .thy files and replace obsolete theory header commands"
    2.24 +  echo "  by 'section' (default), or 'chapter', 'subsection', 'subsubsection'."
    2.25 +  echo
    2.26 +  echo "  Old versions of files are preserved by appending \"~~\"."
    2.27 +  echo
    2.28 +  exit 1
    2.29 +}
    2.30 +
    2.31 +
    2.32 +## process command line
    2.33 +
    2.34 +#options
    2.35 +
    2.36 +SECTION="section"
    2.37 +
    2.38 +while getopts "s:" OPT
    2.39 +do
    2.40 +  case "$OPT" in
    2.41 +    s)
    2.42 +      SECTION="$OPTARG"
    2.43 +      ;;
    2.44 +    \?)
    2.45 +      usage
    2.46 +      ;;
    2.47 +  esac
    2.48 +done
    2.49 +
    2.50 +shift $(($OPTIND - 1))
    2.51 +
    2.52 +
    2.53 +# args
    2.54 +
    2.55 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    2.56 +
    2.57 +SPECS="$@"; shift "$#"
    2.58 +
    2.59 +
    2.60 +## main
    2.61 +
    2.62 +find $SPECS -name \*.thy -print0 | \
    2.63 +  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Header "$SECTION"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/update_header.scala	Sun Nov 02 16:47:45 2014 +0100
     3.3 @@ -0,0 +1,40 @@
     3.4 +/*  Title:      Pure/Tools/update_header.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Replace theory header command.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Update_Header
    3.14 +{
    3.15 +  def update_header(section: String, path: Path)
    3.16 +  {
    3.17 +    val text0 = File.read(path)
    3.18 +    val text1 =
    3.19 +      (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
    3.20 +        yield { if (tok.source == "header") section else tok.source }).mkString
    3.21 +
    3.22 +    if (text0 != text1) {
    3.23 +      Output.writeln("changing " + path)
    3.24 +      File.write_backup2(path, text1)
    3.25 +    }
    3.26 +  }
    3.27 +
    3.28 +
    3.29 +  /* command line entry point */
    3.30 +
    3.31 +  def main(args: Array[String])
    3.32 +  {
    3.33 +    Command_Line.tool0 {
    3.34 +      args.toList match {
    3.35 +        case section :: files =>
    3.36 +          if (!Set("chapter", "section", "subsection", "subsubsection").contains(section))
    3.37 +            error("Bad heading command: " + quote(section))
    3.38 +          files.foreach(file => update_header(section, Path.explode(file)))
    3.39 +        case _ => error("Bad arguments:\n" + cat_lines(args))
    3.40 +      }
    3.41 +    }
    3.42 +  }
    3.43 +}
     4.1 --- a/src/Pure/build-jars	Sun Nov 02 16:39:54 2014 +0100
     4.2 +++ b/src/Pure/build-jars	Sun Nov 02 16:47:45 2014 +0100
     4.3 @@ -96,6 +96,7 @@
     4.4    Tools/simplifier_trace.scala
     4.5    Tools/task_statistics.scala
     4.6    Tools/update_cartouches.scala
     4.7 +  Tools/update_header.scala
     4.8    Tools/update_semicolons.scala
     4.9    library.scala
    4.10    term.scala