src/Pure/Tools/update_semicolons.scala
author wenzelm
Fri, 21 Nov 2014 18:14:39 +0100
changeset 59026 30b8a5825a9c
parent 58861 5ff61774df11
child 59083 88b0b1f28adc
permissions -rw-r--r--
removed some add-ons from modules that are relevant for the inference kernel;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58861
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/update_semicolons.scala
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     3
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     4
Remove obsolete semicolons from theory sources.
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     5
*/
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     6
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     7
package isabelle
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     8
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
     9
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    10
object Update_Semicolons
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    11
{
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    12
  def update_semicolons(path: Path)
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    13
  {
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    14
    val text0 = File.read(path)
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    15
    val text1 =
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    16
      (for (tok <- Outer_Syntax.empty.scan(text0).iterator if tok.source != ";")
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    17
        yield tok.source).mkString
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    18
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    19
    if (text0 != text1) {
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    20
      Output.writeln("changing " + path)
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    21
      File.write_backup2(path, text1)
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    22
    }
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    23
  }
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    24
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    25
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    26
  /* command line entry point */
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    27
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    28
  def main(args: Array[String])
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    29
  {
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    30
    Command_Line.tool0 {
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    31
      args.foreach(arg => update_semicolons(Path.explode(arg)))
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    32
    }
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    33
  }
5ff61774df11 command-line terminator ";" is no longer accepted;
wenzelm
parents:
diff changeset
    34
}