1/* Title: Pure/Tools/update_comments.scala 2 Author: Makarius 3 4Update formal comments in outer syntax: \<comment> \<open>...\<close> 5*/ 6 7package isabelle 8 9 10import scala.annotation.tailrec 11 12 13object Update_Comments 14{ 15 def update_comments(path: Path) 16 { 17 def make_comment(tok: Token): String = 18 Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content)) 19 20 @tailrec def update(toks: List[Token], result: List[String]): String = 21 { 22 toks match { 23 case tok :: rest 24 if tok.source == "--" || tok.source == Symbol.comment => 25 rest.dropWhile(_.is_space) match { 26 case tok1 :: rest1 if tok1.is_text => 27 update(rest1, make_comment(tok1) :: result) 28 case _ => update(rest, tok.source :: result) 29 } 30 case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) => 31 update(rest, make_comment(tok) :: result) 32 case tok :: rest => update(rest, tok.source :: result) 33 case Nil => result.reverse.mkString 34 } 35 } 36 37 val text0 = File.read(path) 38 val text1 = update(Token.explode(Keyword.Keywords.empty, text0), Nil) 39 40 if (text0 != text1) { 41 Output.writeln("changing " + path) 42 File.write_backup2(path, text1) 43 } 44 } 45 46 47 /* Isabelle tool wrapper */ 48 49 val isabelle_tool = 50 Isabelle_Tool("update_comments", "update formal comments in outer syntax", args => 51 { 52 val getopts = Getopts(""" 53Usage: isabelle update_comments [FILES|DIRS...] 54 55 Recursively find .thy files and update formal comments in outer syntax. 56 57 Old versions of files are preserved by appending "~~". 58""") 59 60 val specs = getopts(args) 61 if (specs.isEmpty) getopts.usage() 62 63 for { 64 spec <- specs 65 file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy")) 66 } update_comments(File.path(file)) 67 }) 68} 69