added update_cartouches tool;
authorwenzelm
Tue Oct 07 14:53:51 2014 +0200 (2014-10-07)
changeset 58610fffdbce036db
parent 58609 d0cb70d66bc1
child 58611 d49f3181030e
added update_cartouches tool;
NEWS
lib/Tools/update_cartouches
src/Pure/General/file.scala
src/Pure/General/path.scala
src/Pure/Tools/update_cartouches.scala
src/Pure/build-jars
     1.1 --- a/NEWS	Tue Oct 07 11:44:25 2014 +0200
     1.2 +++ b/NEWS	Tue Oct 07 14:53:51 2014 +0200
     1.3 @@ -129,6 +129,12 @@
     1.4  PARALLEL_GOALS.
     1.5  
     1.6  
     1.7 +*** System ***
     1.8 +
     1.9 +* The Isabelle tool "update_cartouches" changes theory files to use
    1.10 +cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
    1.11 +
    1.12 +
    1.13  
    1.14  New in Isabelle2014 (August 2014)
    1.15  ---------------------------------
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/Tools/update_cartouches	Tue Oct 07 14:53:51 2014 +0200
     2.3 @@ -0,0 +1,36 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Author: Makarius
     2.7 +#
     2.8 +# DESCRIPTION: update theory syntax to use cartouches
     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 update theory syntax to use cartouches"
    2.21 +  echo "  instead of old-style {* verbatim *} or \`alt_string\` tokens."
    2.22 +  echo
    2.23 +  echo "  Old versions of files are preserved by appending \"~~\"."
    2.24 +  echo
    2.25 +  exit 1
    2.26 +}
    2.27 +
    2.28 +
    2.29 +## process command line
    2.30 +
    2.31 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    2.32 +
    2.33 +SPECS="$@"; shift "$#"
    2.34 +
    2.35 +
    2.36 +## main
    2.37 +
    2.38 +find $SPECS -name \*.thy -print0 | \
    2.39 +  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches
     3.1 --- a/src/Pure/General/file.scala	Tue Oct 07 11:44:25 2014 +0200
     3.2 +++ b/src/Pure/General/file.scala	Tue Oct 07 14:53:51 2014 +0200
     3.3 @@ -116,6 +116,12 @@
     3.4      File.write(path, text)
     3.5    }
     3.6  
     3.7 +  def write_backup2(path: Path, text: CharSequence)
     3.8 +  {
     3.9 +    path.file renameTo path.backup2.file
    3.10 +    File.write(path, text)
    3.11 +  }
    3.12 +
    3.13  
    3.14    /* copy */
    3.15  
     4.1 --- a/src/Pure/General/path.scala	Tue Oct 07 11:44:25 2014 +0200
     4.2 +++ b/src/Pure/General/path.scala	Tue Oct 07 14:53:51 2014 +0200
     4.3 @@ -162,6 +162,12 @@
     4.4      prfx + Path.basic(s + "~")
     4.5    }
     4.6  
     4.7 +  def backup2: Path =
     4.8 +  {
     4.9 +    val (prfx, s) = split_path
    4.10 +    prfx + Path.basic(s + "~~")
    4.11 +  }
    4.12 +
    4.13    private val Ext = new Regex("(.*)\\.([^.]*)")
    4.14  
    4.15    def split_ext: (Path, String) =
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/Tools/update_cartouches.scala	Tue Oct 07 14:53:51 2014 +0200
     5.3 @@ -0,0 +1,51 @@
     5.4 +/*  Title:      Pure/Tools/update_cartouches.scala
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Update theory syntax to use cartouches.
     5.8 +*/
     5.9 +
    5.10 +package isabelle
    5.11 +
    5.12 +
    5.13 +object Update_Cartouches
    5.14 +{
    5.15 +  /* update cartouches */
    5.16 +
    5.17 +  private def cartouche(s: String): String =
    5.18 +    Symbol.open + s + Symbol.close
    5.19 +
    5.20 +  private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
    5.21 +
    5.22 +  def update_cartouches(path: Path)
    5.23 +  {
    5.24 +    val text0 = File.read(path)
    5.25 +    val text1 =
    5.26 +      (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
    5.27 +        yield {
    5.28 +          if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
    5.29 +          else if (tok.kind == Token.Kind.VERBATIM) {
    5.30 +            tok.content match {
    5.31 +              case Verbatim_Body(s) => cartouche(s)
    5.32 +              case s => tok.source
    5.33 +            }
    5.34 +          }
    5.35 +          else tok.source
    5.36 +        }
    5.37 +      ).mkString
    5.38 +
    5.39 +    if (text0 != text1) {
    5.40 +      Output.writeln("changing " + path)
    5.41 +      File.write_backup2(path, text1)
    5.42 +    }
    5.43 +  }
    5.44 +
    5.45 +
    5.46 +  /* command line entry point */
    5.47 +
    5.48 +  def main(args: Array[String])
    5.49 +  {
    5.50 +    Command_Line.tool0 {
    5.51 +      args.foreach(arg => update_cartouches(Path.explode(arg)))
    5.52 +    }
    5.53 +  }
    5.54 +}
     6.1 --- a/src/Pure/build-jars	Tue Oct 07 11:44:25 2014 +0200
     6.2 +++ b/src/Pure/build-jars	Tue Oct 07 14:53:51 2014 +0200
     6.3 @@ -97,6 +97,7 @@
     6.4    Tools/print_operation.scala
     6.5    Tools/simplifier_trace.scala
     6.6    Tools/task_statistics.scala
     6.7 +  Tools/update_cartouches.scala
     6.8    library.scala
     6.9    term.scala
    6.10    term_xml.scala