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