# HG changeset patch
# User wenzelm
# Date 1445375026 -7200
# Node ID 3480725c71d2ef0ba2cfad1a2ba94cd7e6f09031
# Parent  97261e6c1d423f5c9164fcf9c61e51b55db10c87
added isabelle update_cartouches option -t;

diff -r 97261e6c1d42 -r 3480725c71d2 NEWS
--- a/NEWS	Tue Oct 20 20:45:33 2015 +0200
+++ b/NEWS	Tue Oct 20 23:03:46 2015 +0200
@@ -66,7 +66,9 @@
 
 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
-text.
+text. Command-line tool "isabelle update_cartouches -t" helps to update
+old sources, by approximative patching of the content of string and
+cartouche tokens seen in theory sources.
 
 * The @{text} antiquotation now ignores the antiquotation option
 "source". The given text content is output unconditionally, without any
diff -r 97261e6c1d42 -r 3480725c71d2 lib/Tools/update_cartouches
--- a/lib/Tools/update_cartouches	Tue Oct 20 20:45:33 2015 +0200
+++ b/lib/Tools/update_cartouches	Tue Oct 20 23:03:46 2015 +0200
@@ -14,6 +14,9 @@
   echo
   echo "Usage: isabelle $PRG [FILES|DIRS...]"
   echo
+  echo "  Options are:"
+  echo "    -t           replace @{text} antiquotations within text tokens"
+  echo
   echo "  Recursively find .thy files and update theory syntax to use cartouches"
   echo "  instead of old-style {* verbatim *} or \`alt_string\` tokens."
   echo
@@ -25,6 +28,27 @@
 
 ## process command line
 
+# options
+
+TEXT="false"
+
+while getopts "t" OPT
+do
+  case "$OPT" in
+    t)
+      TEXT="true"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
 [ "$#" -eq 0 -o "$1" = "-?" ] && usage
 
 SPECS="$@"; shift "$#"
@@ -33,4 +57,4 @@
 ## main
 
 find $SPECS -name \*.thy -print0 | \
-  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches
+  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches "$TEXT"
diff -r 97261e6c1d42 -r 3480725c71d2 src/Pure/General/antiquote.scala
--- a/src/Pure/General/antiquote.scala	Tue Oct 20 20:45:33 2015 +0200
+++ b/src/Pure/General/antiquote.scala	Tue Oct 20 23:03:46 2015 +0200
@@ -12,7 +12,7 @@
 
 object Antiquote
 {
-  sealed abstract class Antiquote
+  sealed abstract class Antiquote { def source: String }
   case class Text(source: String) extends Antiquote
   case class Control(source: String) extends Antiquote
   case class Antiq(source: String) extends Antiquote
diff -r 97261e6c1d42 -r 3480725c71d2 src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Tue Oct 20 20:45:33 2015 +0200
+++ b/src/Pure/Tools/update_cartouches.scala	Tue Oct 20 23:03:46 2015 +0200
@@ -16,9 +16,32 @@
 
   private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
 
-  def update_cartouches(path: Path)
+  val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
+
+  def update_text(content: String): String =
+  {
+    (try { Some(Antiquote.read(content)) } catch { case ERROR(_) => None }) match {
+      case Some(ants) =>
+        val ants1: List[Antiquote.Antiquote] =
+          ants.map(ant =>
+            ant match {
+              case Antiquote.Antiq(Text_Antiq(body)) =>
+                Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match {
+                  case List(tok) => Antiquote.Control(cartouche(tok.content))
+                  case _ => ant
+                }
+              case _ => ant
+            })
+        if (ants == ants1) content else ants1.map(_.source).mkString
+      case None => content
+    }
+  }
+
+  def update_cartouches(replace_text: Boolean, path: Path)
   {
     val text0 = File.read(path)
+
+    // outer syntax cartouches
     val text1 =
       (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
         yield {
@@ -33,9 +56,27 @@
         }
       ).mkString
 
-    if (text0 != text1) {
+    // cartouches within presumed text tokens
+    val text2 =
+      if (replace_text) {
+        (for (tok <- Token.explode(Keyword.Keywords.empty, text1).iterator)
+          yield {
+            if (tok.kind == Token.Kind.STRING || tok.kind == Token.Kind.CARTOUCHE) {
+              val content = tok.content
+              val content1 = update_text(content)
+
+              if (content == content1) tok.source
+              else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1)
+              else cartouche(content1)
+            }
+            else tok.source
+          }).mkString
+      }
+      else text1
+
+    if (text0 != text2) {
       Output.writeln("changing " + path)
-      File.write_backup2(path, text1)
+      File.write_backup2(path, text2)
     }
   }
 
@@ -45,7 +86,11 @@
   def main(args: Array[String])
   {
     Command_Line.tool0 {
-      args.foreach(arg => update_cartouches(Path.explode(arg)))
+      args.toList match {
+        case Properties.Value.Boolean(replace_text) :: files =>
+          files.foreach(file => update_cartouches(replace_text, Path.explode(file)))
+        case _ => error("Bad arguments:\n" + cat_lines(args))
+      }
     }
   }
 }