# HG changeset patch
# User wenzelm
# Date 1412686431 -7200
# Node ID fffdbce036dbe3d66b03a6015670c1ac92e99156
# Parent  d0cb70d66bc1d46f25a262758d38388bddadead7
added update_cartouches tool;

diff -r d0cb70d66bc1 -r fffdbce036db NEWS
--- 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)
 ---------------------------------
diff -r d0cb70d66bc1 -r fffdbce036db lib/Tools/update_cartouches
--- /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
diff -r d0cb70d66bc1 -r fffdbce036db src/Pure/General/file.scala
--- 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 */
 
diff -r d0cb70d66bc1 -r fffdbce036db src/Pure/General/path.scala
--- 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) =
diff -r d0cb70d66bc1 -r fffdbce036db src/Pure/Tools/update_cartouches.scala
--- /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)))
+    }
+  }
+}
diff -r d0cb70d66bc1 -r fffdbce036db src/Pure/build-jars
--- 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