equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Update_Header |
10 object Update_Header { |
11 { |
11 def update_header(section: String, path: Path): Unit = { |
12 def update_header(section: String, path: Path): Unit = |
|
13 { |
|
14 val text0 = File.read(path) |
12 val text0 = File.read(path) |
15 val text1 = |
13 val text1 = |
16 (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) |
14 (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) |
17 yield { if (tok.source == "header") section else tok.source }).mkString |
15 yield { if (tok.source == "header") section else tok.source }).mkString |
18 |
16 |
28 private val headings = |
26 private val headings = |
29 Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph") |
27 Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph") |
30 |
28 |
31 val isabelle_tool = |
29 val isabelle_tool = |
32 Isabelle_Tool("update_header", "replace obsolete theory header command", |
30 Isabelle_Tool("update_header", "replace obsolete theory header command", |
33 Scala_Project.here, args => |
31 Scala_Project.here, |
34 { |
32 args => { |
35 var section = "section" |
33 var section = "section" |
36 |
34 |
37 val getopts = Getopts(""" |
35 val getopts = Getopts(""" |
38 Usage: isabelle update_header [FILES|DIRS...] |
36 Usage: isabelle update_header [FILES|DIRS...] |
39 |
37 |