src/Pure/Tools/update_cartouches.scala
author wenzelm
Wed, 03 Dec 2014 14:04:38 +0100
changeset 59083 88b0b1f28adc
parent 58610 fffdbce036db
child 61492 3480725c71d2
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58610
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/update_cartouches.scala
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     3
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     4
Update theory syntax to use cartouches.
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     5
*/
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     6
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     7
package isabelle
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     8
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
     9
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    10
object Update_Cartouches
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    11
{
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    12
  /* update cartouches */
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    13
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    14
  private def cartouche(s: String): String =
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    15
    Symbol.open + s + Symbol.close
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    16
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    17
  private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    18
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    19
  def update_cartouches(path: Path)
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    20
  {
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    21
    val text0 = File.read(path)
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    22
    val text1 =
59083
88b0b1f28adc tuned signature;
wenzelm
parents: 58610
diff changeset
    23
      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
58610
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    24
        yield {
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    25
          if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    26
          else if (tok.kind == Token.Kind.VERBATIM) {
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    27
            tok.content match {
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    28
              case Verbatim_Body(s) => cartouche(s)
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    29
              case s => tok.source
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    30
            }
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    31
          }
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    32
          else tok.source
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    33
        }
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    34
      ).mkString
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    35
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    36
    if (text0 != text1) {
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    37
      Output.writeln("changing " + path)
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    38
      File.write_backup2(path, text1)
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    39
    }
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    40
  }
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    41
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    42
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    43
  /* command line entry point */
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    44
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    45
  def main(args: Array[String])
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    46
  {
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    47
    Command_Line.tool0 {
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    48
      args.foreach(arg => update_cartouches(Path.explode(arg)))
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    49
    }
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    50
  }
fffdbce036db added update_cartouches tool;
wenzelm
parents:
diff changeset
    51
}