src/Pure/Tools/update_theorems.scala
changeset 61337 4645502c3c64
child 62450 2154f709fc25
equal deleted inserted replaced
61336:fa4ebbd350ae 61337:4645502c3c64
       
     1 /*  Title:      Pure/Tools/update_theorems.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Update toplevel theorem keywords.
       
     5 */
       
     6 
       
     7 package isabelle
       
     8 
       
     9 
       
    10 object Update_Theorems
       
    11 {
       
    12   def update_theorems(path: Path)
       
    13   {
       
    14     val text0 = File.read(path)
       
    15     val text1 =
       
    16       (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
       
    17         yield {
       
    18           tok.source match {
       
    19             case "theorems" => "lemmas"
       
    20             case "schematic_theorem" | "schematic_lemma" | "schematic_corollary" =>
       
    21               "schematic_goal"
       
    22             case s => s
       
    23         } }).mkString
       
    24 
       
    25     if (text0 != text1) {
       
    26       Output.writeln("changing " + path)
       
    27       File.write_backup2(path, text1)
       
    28     }
       
    29   }
       
    30 
       
    31 
       
    32   /* command line entry point */
       
    33 
       
    34   def main(args: Array[String])
       
    35   {
       
    36     Command_Line.tool0 {
       
    37       args.foreach(arg => update_theorems(Path.explode(arg)))
       
    38     }
       
    39   }
       
    40 }