src/Pure/Tools/update_cartouches.scala
author wenzelm
Sun Feb 28 15:00:17 2016 +0100 (2016-02-28)
changeset 62445 91902961184c
parent 61579 634cd44bb1d3
child 62454 38c89353b349
permissions -rw-r--r--
moved getopts to Scala;
wenzelm@58610
     1
/*  Title:      Pure/Tools/update_cartouches.scala
wenzelm@58610
     2
    Author:     Makarius
wenzelm@58610
     3
wenzelm@61579
     4
Update theory syntax to use cartouches etc.
wenzelm@58610
     5
*/
wenzelm@58610
     6
wenzelm@58610
     7
package isabelle
wenzelm@58610
     8
wenzelm@58610
     9
wenzelm@58610
    10
object Update_Cartouches
wenzelm@58610
    11
{
wenzelm@58610
    12
  /* update cartouches */
wenzelm@58610
    13
wenzelm@58610
    14
  private def cartouche(s: String): String =
wenzelm@58610
    15
    Symbol.open + s + Symbol.close
wenzelm@58610
    16
wenzelm@58610
    17
  private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
wenzelm@58610
    18
wenzelm@61492
    19
  val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
wenzelm@61492
    20
wenzelm@61492
    21
  def update_text(content: String): String =
wenzelm@61492
    22
  {
wenzelm@61492
    23
    (try { Some(Antiquote.read(content)) } catch { case ERROR(_) => None }) match {
wenzelm@61492
    24
      case Some(ants) =>
wenzelm@61492
    25
        val ants1: List[Antiquote.Antiquote] =
wenzelm@61492
    26
          ants.map(ant =>
wenzelm@61492
    27
            ant match {
wenzelm@61492
    28
              case Antiquote.Antiq(Text_Antiq(body)) =>
wenzelm@61492
    29
                Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match {
wenzelm@61492
    30
                  case List(tok) => Antiquote.Control(cartouche(tok.content))
wenzelm@61492
    31
                  case _ => ant
wenzelm@61492
    32
                }
wenzelm@61492
    33
              case _ => ant
wenzelm@61492
    34
            })
wenzelm@61492
    35
        if (ants == ants1) content else ants1.map(_.source).mkString
wenzelm@61492
    36
      case None => content
wenzelm@61492
    37
    }
wenzelm@61492
    38
  }
wenzelm@61492
    39
wenzelm@61579
    40
  def update_cartouches(replace_comment: Boolean, replace_text: Boolean, path: Path)
wenzelm@58610
    41
  {
wenzelm@58610
    42
    val text0 = File.read(path)
wenzelm@61492
    43
wenzelm@61579
    44
    // outer syntax cartouches and comment markers
wenzelm@58610
    45
    val text1 =
wenzelm@59083
    46
      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
wenzelm@58610
    47
        yield {
wenzelm@58610
    48
          if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
wenzelm@58610
    49
          else if (tok.kind == Token.Kind.VERBATIM) {
wenzelm@58610
    50
            tok.content match {
wenzelm@58610
    51
              case Verbatim_Body(s) => cartouche(s)
wenzelm@58610
    52
              case s => tok.source
wenzelm@58610
    53
            }
wenzelm@58610
    54
          }
wenzelm@61579
    55
          else if (replace_comment && tok.source == "--") Symbol.comment
wenzelm@58610
    56
          else tok.source
wenzelm@58610
    57
        }
wenzelm@58610
    58
      ).mkString
wenzelm@58610
    59
wenzelm@61492
    60
    // cartouches within presumed text tokens
wenzelm@61492
    61
    val text2 =
wenzelm@61492
    62
      if (replace_text) {
wenzelm@61492
    63
        (for (tok <- Token.explode(Keyword.Keywords.empty, text1).iterator)
wenzelm@61492
    64
          yield {
wenzelm@61492
    65
            if (tok.kind == Token.Kind.STRING || tok.kind == Token.Kind.CARTOUCHE) {
wenzelm@61492
    66
              val content = tok.content
wenzelm@61492
    67
              val content1 = update_text(content)
wenzelm@61492
    68
wenzelm@61492
    69
              if (content == content1) tok.source
wenzelm@61492
    70
              else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1)
wenzelm@61492
    71
              else cartouche(content1)
wenzelm@61492
    72
            }
wenzelm@61492
    73
            else tok.source
wenzelm@61492
    74
          }).mkString
wenzelm@61492
    75
      }
wenzelm@61492
    76
      else text1
wenzelm@61492
    77
wenzelm@61492
    78
    if (text0 != text2) {
wenzelm@58610
    79
      Output.writeln("changing " + path)
wenzelm@61492
    80
      File.write_backup2(path, text2)
wenzelm@58610
    81
    }
wenzelm@58610
    82
  }
wenzelm@58610
    83
wenzelm@58610
    84
wenzelm@58610
    85
  /* command line entry point */
wenzelm@58610
    86
wenzelm@58610
    87
  def main(args: Array[String])
wenzelm@58610
    88
  {
wenzelm@58610
    89
    Command_Line.tool0 {
wenzelm@62445
    90
      var replace_comment = false
wenzelm@62445
    91
      var replace_text = false
wenzelm@62445
    92
wenzelm@62445
    93
      val getopts = Getopts(() => """
wenzelm@62445
    94
Usage: isabelle update_cartouches [FILES|DIRS...]
wenzelm@62445
    95
wenzelm@62445
    96
  Options are:
wenzelm@62445
    97
    -c           replace comment marker "--" by symbol "\<comment>"
wenzelm@62445
    98
    -t           replace @{text} antiquotations within text tokens
wenzelm@62445
    99
wenzelm@62445
   100
  Recursively find .thy files and update theory syntax to use cartouches
wenzelm@62445
   101
  instead of old-style {* verbatim *} or `alt_string` tokens.
wenzelm@62445
   102
wenzelm@62445
   103
  Old versions of files are preserved by appending "~~".
wenzelm@62445
   104
""",
wenzelm@62445
   105
        "c" -> (_ => replace_comment = true),
wenzelm@62445
   106
        "t" -> (_ => replace_text = true))
wenzelm@62445
   107
wenzelm@62445
   108
      val specs = getopts(args)
wenzelm@62445
   109
      if (specs.isEmpty) getopts.usage()
wenzelm@62445
   110
wenzelm@62445
   111
      for {
wenzelm@62445
   112
        spec <- specs
wenzelm@62445
   113
        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
wenzelm@62445
   114
      } update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
wenzelm@58610
   115
    }
wenzelm@58610
   116
  }
wenzelm@58610
   117
}