--- a/NEWS Tue Oct 07 11:44:25 2014 +0200
+++ b/NEWS Tue Oct 07 14:53:51 2014 +0200
@@ -129,6 +129,12 @@
PARALLEL_GOALS.
+*** System ***
+
+* The Isabelle tool "update_cartouches" changes theory files to use
+cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
+
+
New in Isabelle2014 (August 2014)
---------------------------------
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/update_cartouches Tue Oct 07 14:53:51 2014 +0200
@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: update theory syntax to use cartouches
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [FILES|DIRS...]"
+ echo
+ echo " Recursively find .thy files and update theory syntax to use cartouches"
+ echo " instead of old-style {* verbatim *} or \`alt_string\` tokens."
+ echo
+ echo " Old versions of files are preserved by appending \"~~\"."
+ echo
+ exit 1
+}
+
+
+## process command line
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SPECS="$@"; shift "$#"
+
+
+## main
+
+find $SPECS -name \*.thy -print0 | \
+ xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches
--- a/src/Pure/General/file.scala Tue Oct 07 11:44:25 2014 +0200
+++ b/src/Pure/General/file.scala Tue Oct 07 14:53:51 2014 +0200
@@ -116,6 +116,12 @@
File.write(path, text)
}
+ def write_backup2(path: Path, text: CharSequence)
+ {
+ path.file renameTo path.backup2.file
+ File.write(path, text)
+ }
+
/* copy */
--- a/src/Pure/General/path.scala Tue Oct 07 11:44:25 2014 +0200
+++ b/src/Pure/General/path.scala Tue Oct 07 14:53:51 2014 +0200
@@ -162,6 +162,12 @@
prfx + Path.basic(s + "~")
}
+ def backup2: Path =
+ {
+ val (prfx, s) = split_path
+ prfx + Path.basic(s + "~~")
+ }
+
private val Ext = new Regex("(.*)\\.([^.]*)")
def split_ext: (Path, String) =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update_cartouches.scala Tue Oct 07 14:53:51 2014 +0200
@@ -0,0 +1,51 @@
+/* Title: Pure/Tools/update_cartouches.scala
+ Author: Makarius
+
+Update theory syntax to use cartouches.
+*/
+
+package isabelle
+
+
+object Update_Cartouches
+{
+ /* update cartouches */
+
+ private def cartouche(s: String): String =
+ Symbol.open + s + Symbol.close
+
+ private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
+
+ def update_cartouches(path: Path)
+ {
+ val text0 = File.read(path)
+ val text1 =
+ (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
+ yield {
+ if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
+ else if (tok.kind == Token.Kind.VERBATIM) {
+ tok.content match {
+ case Verbatim_Body(s) => cartouche(s)
+ case s => tok.source
+ }
+ }
+ else tok.source
+ }
+ ).mkString
+
+ if (text0 != text1) {
+ Output.writeln("changing " + path)
+ File.write_backup2(path, text1)
+ }
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ args.foreach(arg => update_cartouches(Path.explode(arg)))
+ }
+ }
+}
--- a/src/Pure/build-jars Tue Oct 07 11:44:25 2014 +0200
+++ b/src/Pure/build-jars Tue Oct 07 14:53:51 2014 +0200
@@ -97,6 +97,7 @@
Tools/print_operation.scala
Tools/simplifier_trace.scala
Tools/task_statistics.scala
+ Tools/update_cartouches.scala
library.scala
term.scala
term_xml.scala