src/Pure/Tools/update_theorems.scala
author wenzelm
Wed, 10 Feb 2016 14:14:43 +0100
changeset 62278 c04e97be39d3
parent 61337 4645502c3c64
child 62450 2154f709fc25
permissions -rw-r--r--
misc tuning and updates;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/update_theorems.scala
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     3
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     4
Update toplevel theorem keywords.
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     5
*/
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     6
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     7
package isabelle
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     8
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
     9
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    10
object Update_Theorems
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    11
{
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    12
  def update_theorems(path: Path)
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    13
  {
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    14
    val text0 = File.read(path)
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    15
    val text1 =
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    16
      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    17
        yield {
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    18
          tok.source match {
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    19
            case "theorems" => "lemmas"
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    20
            case "schematic_theorem" | "schematic_lemma" | "schematic_corollary" =>
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    21
              "schematic_goal"
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    22
            case s => s
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    23
        } }).mkString
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    24
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    25
    if (text0 != text1) {
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    26
      Output.writeln("changing " + path)
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    27
      File.write_backup2(path, text1)
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    28
    }
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    29
  }
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    30
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    31
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    32
  /* command line entry point */
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    33
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    34
  def main(args: Array[String])
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    35
  {
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    36
    Command_Line.tool0 {
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    37
      args.foreach(arg => update_theorems(Path.explode(arg)))
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    38
    }
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    39
  }
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents:
diff changeset
    40
}