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