equal
deleted
inserted
replaced
|
1 /* Title: Pure/Tools/update_cartouches.scala |
|
2 Author: Makarius |
|
3 |
|
4 Update theory syntax to use cartouches. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Update_Cartouches |
|
11 { |
|
12 /* update cartouches */ |
|
13 |
|
14 private def cartouche(s: String): String = |
|
15 Symbol.open + s + Symbol.close |
|
16 |
|
17 private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r |
|
18 |
|
19 def update_cartouches(path: Path) |
|
20 { |
|
21 val text0 = File.read(path) |
|
22 val text1 = |
|
23 (for (tok <- Outer_Syntax.empty.scan(text0).iterator) |
|
24 yield { |
|
25 if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content) |
|
26 else if (tok.kind == Token.Kind.VERBATIM) { |
|
27 tok.content match { |
|
28 case Verbatim_Body(s) => cartouche(s) |
|
29 case s => tok.source |
|
30 } |
|
31 } |
|
32 else tok.source |
|
33 } |
|
34 ).mkString |
|
35 |
|
36 if (text0 != text1) { |
|
37 Output.writeln("changing " + path) |
|
38 File.write_backup2(path, text1) |
|
39 } |
|
40 } |
|
41 |
|
42 |
|
43 /* command line entry point */ |
|
44 |
|
45 def main(args: Array[String]) |
|
46 { |
|
47 Command_Line.tool0 { |
|
48 args.foreach(arg => update_cartouches(Path.explode(arg))) |
|
49 } |
|
50 } |
|
51 } |