--- 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
--- 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"
--- 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
--- 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))
+ }
}
}
}