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