src/Pure/Tools/update_theorems.scala
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 62836 98dbed6cfa44
child 68994 d961e11e0e87
permissions -rw-r--r--
tuned signature;
     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   /* Isabelle tool wrapper */
    33 
    34   val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
    35   {
    36     val getopts = Getopts("""
    37 Usage: isabelle update_theorems [FILES|DIRS...]
    38 
    39   Recursively find .thy files and update toplevel theorem keywords:
    40 
    41     theorems             ~>  lemmas
    42     schematic_theorem    ~>  schematic_goal
    43     schematic_lemma      ~>  schematic_goal
    44     schematic_corollary  ~>  schematic_goal
    45 
    46   Old versions of files are preserved by appending "~~".
    47 """)
    48 
    49     val specs = getopts(args)
    50     if (specs.isEmpty) getopts.usage()
    51 
    52     for {
    53       spec <- specs
    54       file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
    55     } update_theorems(Path.explode(File.standard_path(file)))
    56   })
    57 }