equal
deleted
inserted
replaced
23 } |
23 } |
24 |
24 |
25 |
25 |
26 /* command line entry point */ |
26 /* command line entry point */ |
27 |
27 |
|
28 private val headings = |
|
29 Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph") |
|
30 |
28 def main(args: Array[String]) |
31 def main(args: Array[String]) |
29 { |
32 { |
30 Command_Line.tool0 { |
33 Command_Line.tool0 { |
31 args.toList match { |
34 args.toList match { |
32 case section :: files => |
35 case section :: files => |
33 if (!Set("chapter", "section", "subsection", "subsubsection").contains(section)) |
36 if (!headings.contains(section)) |
34 error("Bad heading command: " + quote(section)) |
37 error("Bad heading command: " + quote(section)) |
35 files.foreach(file => update_header(section, Path.explode(file))) |
38 files.foreach(file => update_header(section, Path.explode(file))) |
36 case _ => error("Bad arguments:\n" + cat_lines(args)) |
39 case _ => |
|
40 error("Bad arguments:\n" + cat_lines(args)) |
37 } |
41 } |
38 } |
42 } |
39 } |
43 } |
40 } |
44 } |