added isabelle update_then;
authorwenzelm
Mon Sep 21 17:42:31 2015 +0200 (2015-09-21)
changeset 612164ca490f09ec6
parent 61215 652611b34c2c
child 61217 566f256f59bb
added isabelle update_then;
NEWS
lib/Tools/update_then
src/Pure/Tools/update_then.scala
src/Pure/build-jars
     1.1 --- a/NEWS	Mon Sep 21 17:01:33 2015 +0200
     1.2 +++ b/NEWS	Mon Sep 21 17:42:31 2015 +0200
     1.3 @@ -368,6 +368,15 @@
     1.4  running Isabelle/jEdit process. This achieves the effect of
     1.5  single-instance applications seen on common GUI desktops.
     1.6  
     1.7 +* Command-line tool "isabelle update_then" expands old Isar command
     1.8 +conflations:
     1.9 +
    1.10 +    hence  ~>  then have
    1.11 +    thus   ~>  then show
    1.12 +
    1.13 +This syntax is more orthogonal and improves readability and
    1.14 +maintainability of proofs.
    1.15 +
    1.16  * Poly/ML default platform architecture may be changed from 32bit to
    1.17  64bit via system option ML_system_64. A system restart (and rebuild)
    1.18  is required after change.
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/update_then	Mon Sep 21 17:42:31 2015 +0200
     2.3 @@ -0,0 +1,38 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Author: Makarius
     2.7 +#
     2.8 +# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
     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 "  Recursively find .thy files and expand old Isar command conflations:"
    2.21 +  echo
    2.22 +  echo "    hence  ~>  then have"
    2.23 +  echo "    thus   ~>  then show"
    2.24 +  echo
    2.25 +  echo "  Old versions of files are preserved by appending \"~~\"."
    2.26 +  echo
    2.27 +  exit 1
    2.28 +}
    2.29 +
    2.30 +
    2.31 +## process command line
    2.32 +
    2.33 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    2.34 +
    2.35 +SPECS="$@"; shift "$#"
    2.36 +
    2.37 +
    2.38 +## main
    2.39 +
    2.40 +find $SPECS -name \*.thy -print0 | \
    2.41 +  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Then
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/update_then.scala	Mon Sep 21 17:42:31 2015 +0200
     3.3 @@ -0,0 +1,39 @@
     3.4 +/*  Title:      Pure/Tools/update_then.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Expand old Isar command conflations 'hence' and 'thus'.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Update_Then
    3.14 +{
    3.15 +  def update_then(path: Path)
    3.16 +  {
    3.17 +    val text0 = File.read(path)
    3.18 +    val text1 =
    3.19 +      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
    3.20 +        yield {
    3.21 +          tok.source match {
    3.22 +            case "hence" => "then have"
    3.23 +            case "thus" => "then show"
    3.24 +            case s => s
    3.25 +        } }).mkString
    3.26 +
    3.27 +    if (text0 != text1) {
    3.28 +      Output.writeln("changing " + path)
    3.29 +      File.write_backup2(path, text1)
    3.30 +    }
    3.31 +  }
    3.32 +
    3.33 +
    3.34 +  /* command line entry point */
    3.35 +
    3.36 +  def main(args: Array[String])
    3.37 +  {
    3.38 +    Command_Line.tool0 {
    3.39 +      args.foreach(arg => update_then(Path.explode(arg)))
    3.40 +    }
    3.41 +  }
    3.42 +}
     4.1 --- a/src/Pure/build-jars	Mon Sep 21 17:01:33 2015 +0200
     4.2 +++ b/src/Pure/build-jars	Mon Sep 21 17:42:31 2015 +0200
     4.3 @@ -105,6 +105,7 @@
     4.4    Tools/update_cartouches.scala
     4.5    Tools/update_header.scala
     4.6    Tools/update_semicolons.scala
     4.7 +  Tools/update_then.scala
     4.8    library.scala
     4.9    term.scala
    4.10    term_xml.scala