src/Pure/Tools/update_cartouches.scala

support for (single) primary key;
more operations;

/*  Title:      Pure/Tools/update_cartouches.scala
    Author:     Makarius

Update theory syntax to use cartouches etc.
*/

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

  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_comment: Boolean, replace_text: Boolean, path: Path)
  {
    val text0 = File.read(path)

    // outer syntax cartouches and comment markers
    val text1 =
      (for (tok <- Token.explode(Keyword.Keywords.empty, 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 if (replace_comment && tok.source == "--") Symbol.comment
          else tok.source
        }
      ).mkString

    // 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, text2)
    }
  }


  /* Isabelle tool wrapper */

  val isabelle_tool =
    Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
    {
      var replace_comment = false
      var replace_text = false

      val getopts = Getopts("""
Usage: isabelle update_cartouches [FILES|DIRS...]

  Options are:
    -c           replace comment marker "--" by symbol "\<comment>"
    -t           replace @{text} antiquotations within text tokens

  Recursively find .thy files and update theory syntax to use cartouches
  instead of old-style {* verbatim *} or `alt_string` tokens.

  Old versions of files are preserved by appending "~~".
""",
        "c" -> (_ => replace_comment = true),
        "t" -> (_ => replace_text = true))

      val specs = getopts(args)
      if (specs.isEmpty) getopts.usage()

      for {
        spec <- specs
        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
      } update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
    })
}