equal
deleted
inserted
replaced
11 { |
11 { |
12 def update_header(section: String, path: Path) |
12 def update_header(section: String, path: Path) |
13 { |
13 { |
14 val text0 = File.read(path) |
14 val text0 = File.read(path) |
15 val text1 = |
15 val text1 = |
16 (for (tok <- Outer_Syntax.empty.scan(text0).iterator) |
16 (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) |
17 yield { if (tok.source == "header") section else tok.source }).mkString |
17 yield { if (tok.source == "header") section else tok.source }).mkString |
18 |
18 |
19 if (text0 != text1) { |
19 if (text0 != text1) { |
20 Output.writeln("changing " + path) |
20 Output.writeln("changing " + path) |
21 File.write_backup2(path, text1) |
21 File.write_backup2(path, text1) |