added isabelle update_cartouches option -t;
authorwenzelm
Tue Oct 20 23:03:46 2015 +0200 (2015-10-20)
changeset 614923480725c71d2
parent 61491 97261e6c1d42
child 61493 0debd22f0c0e
added isabelle update_cartouches option -t;
NEWS
lib/Tools/update_cartouches
src/Pure/General/antiquote.scala
src/Pure/Tools/update_cartouches.scala
     1.1 --- a/NEWS	Tue Oct 20 20:45:33 2015 +0200
     1.2 +++ b/NEWS	Tue Oct 20 23:03:46 2015 +0200
     1.3 @@ -66,7 +66,9 @@
     1.4  
     1.5  * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
     1.6  Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
     1.7 -text.
     1.8 +text. Command-line tool "isabelle update_cartouches -t" helps to update
     1.9 +old sources, by approximative patching of the content of string and
    1.10 +cartouche tokens seen in theory sources.
    1.11  
    1.12  * The @{text} antiquotation now ignores the antiquotation option
    1.13  "source". The given text content is output unconditionally, without any
     2.1 --- a/lib/Tools/update_cartouches	Tue Oct 20 20:45:33 2015 +0200
     2.2 +++ b/lib/Tools/update_cartouches	Tue Oct 20 23:03:46 2015 +0200
     2.3 @@ -14,6 +14,9 @@
     2.4    echo
     2.5    echo "Usage: isabelle $PRG [FILES|DIRS...]"
     2.6    echo
     2.7 +  echo "  Options are:"
     2.8 +  echo "    -t           replace @{text} antiquotations within text tokens"
     2.9 +  echo
    2.10    echo "  Recursively find .thy files and update theory syntax to use cartouches"
    2.11    echo "  instead of old-style {* verbatim *} or \`alt_string\` tokens."
    2.12    echo
    2.13 @@ -25,6 +28,27 @@
    2.14  
    2.15  ## process command line
    2.16  
    2.17 +# options
    2.18 +
    2.19 +TEXT="false"
    2.20 +
    2.21 +while getopts "t" OPT
    2.22 +do
    2.23 +  case "$OPT" in
    2.24 +    t)
    2.25 +      TEXT="true"
    2.26 +      ;;
    2.27 +    \?)
    2.28 +      usage
    2.29 +      ;;
    2.30 +  esac
    2.31 +done
    2.32 +
    2.33 +shift $(($OPTIND - 1))
    2.34 +
    2.35 +
    2.36 +# args
    2.37 +
    2.38  [ "$#" -eq 0 -o "$1" = "-?" ] && usage
    2.39  
    2.40  SPECS="$@"; shift "$#"
    2.41 @@ -33,4 +57,4 @@
    2.42  ## main
    2.43  
    2.44  find $SPECS -name \*.thy -print0 | \
    2.45 -  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches
    2.46 +  xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Cartouches "$TEXT"
     3.1 --- a/src/Pure/General/antiquote.scala	Tue Oct 20 20:45:33 2015 +0200
     3.2 +++ b/src/Pure/General/antiquote.scala	Tue Oct 20 23:03:46 2015 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  
     3.5  object Antiquote
     3.6  {
     3.7 -  sealed abstract class Antiquote
     3.8 +  sealed abstract class Antiquote { def source: String }
     3.9    case class Text(source: String) extends Antiquote
    3.10    case class Control(source: String) extends Antiquote
    3.11    case class Antiq(source: String) extends Antiquote
     4.1 --- a/src/Pure/Tools/update_cartouches.scala	Tue Oct 20 20:45:33 2015 +0200
     4.2 +++ b/src/Pure/Tools/update_cartouches.scala	Tue Oct 20 23:03:46 2015 +0200
     4.3 @@ -16,9 +16,32 @@
     4.4  
     4.5    private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
     4.6  
     4.7 -  def update_cartouches(path: Path)
     4.8 +  val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
     4.9 +
    4.10 +  def update_text(content: String): String =
    4.11 +  {
    4.12 +    (try { Some(Antiquote.read(content)) } catch { case ERROR(_) => None }) match {
    4.13 +      case Some(ants) =>
    4.14 +        val ants1: List[Antiquote.Antiquote] =
    4.15 +          ants.map(ant =>
    4.16 +            ant match {
    4.17 +              case Antiquote.Antiq(Text_Antiq(body)) =>
    4.18 +                Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match {
    4.19 +                  case List(tok) => Antiquote.Control(cartouche(tok.content))
    4.20 +                  case _ => ant
    4.21 +                }
    4.22 +              case _ => ant
    4.23 +            })
    4.24 +        if (ants == ants1) content else ants1.map(_.source).mkString
    4.25 +      case None => content
    4.26 +    }
    4.27 +  }
    4.28 +
    4.29 +  def update_cartouches(replace_text: Boolean, path: Path)
    4.30    {
    4.31      val text0 = File.read(path)
    4.32 +
    4.33 +    // outer syntax cartouches
    4.34      val text1 =
    4.35        (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
    4.36          yield {
    4.37 @@ -33,9 +56,27 @@
    4.38          }
    4.39        ).mkString
    4.40  
    4.41 -    if (text0 != text1) {
    4.42 +    // cartouches within presumed text tokens
    4.43 +    val text2 =
    4.44 +      if (replace_text) {
    4.45 +        (for (tok <- Token.explode(Keyword.Keywords.empty, text1).iterator)
    4.46 +          yield {
    4.47 +            if (tok.kind == Token.Kind.STRING || tok.kind == Token.Kind.CARTOUCHE) {
    4.48 +              val content = tok.content
    4.49 +              val content1 = update_text(content)
    4.50 +
    4.51 +              if (content == content1) tok.source
    4.52 +              else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1)
    4.53 +              else cartouche(content1)
    4.54 +            }
    4.55 +            else tok.source
    4.56 +          }).mkString
    4.57 +      }
    4.58 +      else text1
    4.59 +
    4.60 +    if (text0 != text2) {
    4.61        Output.writeln("changing " + path)
    4.62 -      File.write_backup2(path, text1)
    4.63 +      File.write_backup2(path, text2)
    4.64      }
    4.65    }
    4.66  
    4.67 @@ -45,7 +86,11 @@
    4.68    def main(args: Array[String])
    4.69    {
    4.70      Command_Line.tool0 {
    4.71 -      args.foreach(arg => update_cartouches(Path.explode(arg)))
    4.72 +      args.toList match {
    4.73 +        case Properties.Value.Boolean(replace_text) :: files =>
    4.74 +          files.foreach(file => update_cartouches(replace_text, Path.explode(file)))
    4.75 +        case _ => error("Bad arguments:\n" + cat_lines(args))
    4.76 +      }
    4.77      }
    4.78    }
    4.79  }