equal
deleted
inserted
replaced
148 |
148 |
149 /* administrative update_keywords */ |
149 /* administrative update_keywords */ |
150 |
150 |
151 def update_keywords(options: Options) |
151 def update_keywords(options: Options) |
152 { |
152 { |
153 val tree = Build.find_sessions(options, Nil) |
153 val tree = Build.find_sessions(options) |
154 |
154 |
155 def chapter(ch: String): List[String] = |
155 def chapter(ch: String): List[String] = |
156 for ((name, info) <- tree.topological_order if info.chapter == ch) yield name |
156 for ((name, info) <- tree.topological_order if info.chapter == ch) yield name |
157 |
157 |
158 keywords(options, sessions = chapter("HOL")) |
158 keywords(options, sessions = chapter("HOL")) |