1/*  Title:      Pure/Tools/update_cartouches.scala
2    Author:     Makarius
3
4Update theory syntax to use cartouches etc.
5*/
6
7package isabelle
8
9
10object Update_Cartouches
11{
12  /* update cartouches */
13
14  private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
15
16  val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
17
18  def update_text(content: String): String =
19  {
20    (try { Some(Antiquote.read(content)) } catch { case ERROR(_) => None }) match {
21      case Some(ants) =>
22        val ants1: List[Antiquote.Antiquote] =
23          ants.map(ant =>
24            ant match {
25              case Antiquote.Antiq(Text_Antiq(body)) =>
26                Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match {
27                  case List(tok) => Antiquote.Control(Symbol.cartouche(tok.content))
28                  case _ => ant
29                }
30              case _ => ant
31            })
32        if (ants == ants1) content else ants1.map(_.source).mkString
33      case None => content
34    }
35  }
36
37  def update_cartouches(replace_text: Boolean, path: Path)
38  {
39    val text0 = File.read(path)
40
41    // outer syntax cartouches
42    val text1 =
43      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
44        yield {
45          if (tok.kind == Token.Kind.ALT_STRING) Symbol.cartouche(tok.content)
46          else if (tok.kind == Token.Kind.VERBATIM) {
47            tok.content match {
48              case Verbatim_Body(s) => Symbol.cartouche(s)
49              case s => tok.source
50            }
51          }
52          else tok.source
53        }
54      ).mkString
55
56    // cartouches within presumed text tokens
57    val text2 =
58      if (replace_text) {
59        (for (tok <- Token.explode(Keyword.Keywords.empty, text1).iterator)
60          yield {
61            if (tok.kind == Token.Kind.STRING || tok.kind == Token.Kind.CARTOUCHE) {
62              val content = tok.content
63              val content1 = update_text(content)
64
65              if (content == content1) tok.source
66              else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1)
67              else Symbol.cartouche(content1)
68            }
69            else tok.source
70          }).mkString
71      }
72      else text1
73
74    if (text0 != text2) {
75      Output.writeln("changing " + path)
76      File.write_backup2(path, text2)
77    }
78  }
79
80
81  /* Isabelle tool wrapper */
82
83  val isabelle_tool =
84    Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
85    {
86      var replace_text = false
87
88      val getopts = Getopts("""
89Usage: isabelle update_cartouches [FILES|DIRS...]
90
91  Options are:
92    -t           replace @{text} antiquotations within text tokens
93
94  Recursively find .thy or ROOT files and update theory syntax to use
95  cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
96
97  Old versions of files are preserved by appending "~~".
98""",
99        "t" -> (_ => replace_text = true))
100
101      val specs = getopts(args)
102      if (specs.isEmpty) getopts.usage()
103
104      for {
105        spec <- specs
106        file <- File.find_files(Path.explode(spec).file,
107          file => file.getName.endsWith(".thy") || file.getName == "ROOT")
108      } update_cartouches(replace_text, File.path(file))
109    })
110}
111