1 /* Title: Pure/Tools/imports.scala |
|
2 Author: Makarius |
|
3 |
|
4 Maintain theory imports wrt. session structure. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.io.{File => JFile} |
|
11 |
|
12 |
|
13 object Imports |
|
14 { |
|
15 /* repository files */ |
|
16 |
|
17 def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true) |
|
18 : List[JFile] = |
|
19 Mercurial.find_repository(start) match { |
|
20 case None => |
|
21 progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)") |
|
22 Nil |
|
23 case Some(hg) => |
|
24 val start_path = start.canonical_file.toPath |
|
25 for { |
|
26 name <- hg.known_files() |
|
27 file = (hg.root + Path.explode(name)).file |
|
28 if pred(file) && File.canonical(file).toPath.startsWith(start_path) |
|
29 } yield file |
|
30 } |
|
31 |
|
32 |
|
33 /* report imports */ |
|
34 |
|
35 sealed case class Report( |
|
36 info: Sessions.Info, |
|
37 declared_imports: Set[String], |
|
38 potential_imports: Option[List[String]], |
|
39 actual_imports: Option[List[String]]) |
|
40 { |
|
41 def print(keywords: Keyword.Keywords, result: List[String]): String = |
|
42 { |
|
43 def print_name(name: String): String = Token.quote_name(keywords, name) |
|
44 |
|
45 " session " + print_name(info.name) + ": " + result.map(print_name(_)).mkString(" ") |
|
46 } |
|
47 } |
|
48 |
|
49 |
|
50 /* update imports */ |
|
51 |
|
52 sealed case class Update(range: Text.Range, old_text: String, new_text: String) |
|
53 { |
|
54 def edits: List[Text.Edit] = |
|
55 Text.Edit.replace(range.start, old_text, new_text) |
|
56 |
|
57 override def toString: String = |
|
58 range.toString + ": " + old_text + " -> " + new_text |
|
59 } |
|
60 |
|
61 def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String) |
|
62 : Option[(JFile, Update)] = |
|
63 { |
|
64 val file = |
|
65 pos match { |
|
66 case Position.File(file) => Path.explode(file).canonical_file |
|
67 case _ => error("Missing file in position" + Position.here(pos)) |
|
68 } |
|
69 |
|
70 val text = File.read(file) |
|
71 |
|
72 val range = |
|
73 pos match { |
|
74 case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range) |
|
75 case _ => error("Missing range in position" + Position.here(pos)) |
|
76 } |
|
77 |
|
78 Token.read_name(keywords, range.substring(text)) match { |
|
79 case Some(tok) => |
|
80 val s1 = tok.source |
|
81 val s2 = Token.quote_name(keywords, update(tok.content)) |
|
82 if (s1 == s2) None else Some((file, Update(range, s1, s2))) |
|
83 case None => error("Name token expected" + Position.here(pos)) |
|
84 } |
|
85 } |
|
86 |
|
87 |
|
88 /* collective operations */ |
|
89 |
|
90 def imports( |
|
91 options: Options, |
|
92 operation_imports: Boolean = false, |
|
93 operation_repository_files: Boolean = false, |
|
94 operation_update: Boolean = false, |
|
95 update_message: String = "", |
|
96 progress: Progress = No_Progress, |
|
97 selection: Sessions.Selection = Sessions.Selection.empty, |
|
98 dirs: List[Path] = Nil, |
|
99 select_dirs: List[Path] = Nil, |
|
100 verbose: Boolean = false) = |
|
101 { |
|
102 val sessions_structure = |
|
103 Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs) |
|
104 |
|
105 val deps = |
|
106 sessions_structure.selection_deps(options, selection, progress = progress, verbose = verbose). |
|
107 check_errors |
|
108 |
|
109 val root_keywords = Sessions.root_syntax.keywords |
|
110 |
|
111 if (operation_imports) { |
|
112 val report_imports: List[Report] = |
|
113 sessions_structure.build_topological_order.map((session_name: String) => |
|
114 { |
|
115 val info = sessions_structure(session_name) |
|
116 val session_base = deps(session_name) |
|
117 |
|
118 val declared_imports = |
|
119 sessions_structure.imports_requirements(List(session_name)).toSet |
|
120 |
|
121 val extra_imports = |
|
122 (for { |
|
123 a <- session_base.known.theory_names |
|
124 if session_base.theory_qualifier(a) == info.name |
|
125 b <- deps.all_known.get_file(a.path.file) |
|
126 qualifier = session_base.theory_qualifier(b) |
|
127 if !declared_imports.contains(qualifier) |
|
128 } yield qualifier).toSet |
|
129 |
|
130 val loaded_imports = |
|
131 sessions_structure.imports_requirements( |
|
132 session_base.loaded_theories.keys.map(a => |
|
133 session_base.theory_qualifier(session_base.known.theories(a).name))) |
|
134 .toSet - session_name |
|
135 |
|
136 val minimal_imports = |
|
137 loaded_imports.filter(s1 => |
|
138 !loaded_imports.exists(s2 => sessions_structure.imports_graph.is_edge(s1, s2))) |
|
139 |
|
140 def make_result(set: Set[String]): Option[List[String]] = |
|
141 if (set.isEmpty) None |
|
142 else Some(sessions_structure.imports_topological_order.filter(set)) |
|
143 |
|
144 Report(info, declared_imports, make_result(extra_imports), |
|
145 if (loaded_imports == declared_imports - session_name) None |
|
146 else make_result(minimal_imports)) |
|
147 }) |
|
148 |
|
149 progress.echo("\nPotential session imports:") |
|
150 for { |
|
151 report <- report_imports.sortBy(_.declared_imports.size) |
|
152 potential_imports <- report.potential_imports |
|
153 } progress.echo(report.print(root_keywords, potential_imports)) |
|
154 |
|
155 progress.echo("\nActual session imports:") |
|
156 for { |
|
157 report <- report_imports |
|
158 actual_imports <- report.actual_imports |
|
159 } progress.echo(report.print(root_keywords, actual_imports)) |
|
160 } |
|
161 |
|
162 if (operation_repository_files) { |
|
163 progress.echo("\nMercurial repository check:") |
|
164 val unused_files = |
|
165 for { |
|
166 (_, dir) <- Sessions.directories(dirs, select_dirs) |
|
167 file <- repository_files(progress, dir, file => file.getName.endsWith(".thy")) |
|
168 if deps.all_known.get_file(file).isEmpty |
|
169 } yield file |
|
170 unused_files.foreach(file => progress.echo("unused file " + quote(file.toString))) |
|
171 } |
|
172 |
|
173 if (operation_update) { |
|
174 progress.echo("\nUpdate theory imports" + update_message + ":") |
|
175 val updates = |
|
176 sessions_structure.build_topological_order.flatMap(session_name => |
|
177 { |
|
178 val info = sessions_structure(session_name) |
|
179 val session_base = deps(session_name) |
|
180 val session_resources = new Resources(sessions_structure, session_base) |
|
181 val imports_base = session_base.get_imports |
|
182 val imports_resources = new Resources(sessions_structure, imports_base) |
|
183 |
|
184 def standard_import(qualifier: String, dir: String, s: String): String = |
|
185 imports_resources.standard_import(session_base, qualifier, dir, s) |
|
186 |
|
187 val updates_root = |
|
188 for { |
|
189 (_, pos) <- info.theories.flatMap(_._2) |
|
190 upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _)) |
|
191 } yield upd |
|
192 |
|
193 val updates_theories = |
|
194 (for { |
|
195 name <- session_base.known.theories_local.iterator.map(p => p._2.name) |
|
196 if session_base.theory_qualifier(name) == info.name |
|
197 (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports_pos |
|
198 upd <- update_name(session_base.overall_syntax.keywords, pos, |
|
199 standard_import(session_base.theory_qualifier(name), name.master_dir, _)) |
|
200 } yield upd).toList |
|
201 |
|
202 updates_root ::: updates_theories |
|
203 }) |
|
204 |
|
205 val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _) |
|
206 val conflicts = |
|
207 file_updates.iterator_list.flatMap({ case (file, upds) => |
|
208 Library.duplicates(upds.sortBy(_.range.start), |
|
209 (x: Update, y: Update) => x.range overlaps y.range) match |
|
210 { |
|
211 case Nil => None |
|
212 case bad => Some((file, bad)) |
|
213 } |
|
214 }) |
|
215 if (conflicts.nonEmpty) |
|
216 error(cat_lines( |
|
217 conflicts.map({ case (file, bad) => |
|
218 "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") }))) |
|
219 |
|
220 for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) { |
|
221 progress.echo("file " + quote(file.toString)) |
|
222 val edits = |
|
223 upds.sortBy(upd => - upd.range.start).flatMap(upd => |
|
224 Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text)) |
|
225 val new_text = |
|
226 (File.read(file) /: edits)({ case (text, edit) => |
|
227 edit.edit(text, 0) match { |
|
228 case (None, text1) => text1 |
|
229 case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file) |
|
230 } |
|
231 }) |
|
232 File.write_backup2(Path.explode(File.standard_path(file)), new_text) |
|
233 } |
|
234 } |
|
235 } |
|
236 |
|
237 |
|
238 /* Isabelle tool wrapper */ |
|
239 |
|
240 val isabelle_tool = |
|
241 Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args => |
|
242 { |
|
243 var base_sessions: List[String] = Nil |
|
244 var select_dirs: List[Path] = Nil |
|
245 var operation_imports = false |
|
246 var operation_repository_files = false |
|
247 var requirements = false |
|
248 var operation_update = false |
|
249 var exclude_session_groups: List[String] = Nil |
|
250 var all_sessions = false |
|
251 var dirs: List[Path] = Nil |
|
252 var session_groups: List[String] = Nil |
|
253 var incremental_update = false |
|
254 var options = Options.init() |
|
255 var verbose = false |
|
256 var exclude_sessions: List[String] = Nil |
|
257 |
|
258 val getopts = Getopts(""" |
|
259 Usage: isabelle imports [OPTIONS] [SESSIONS ...] |
|
260 |
|
261 Options are: |
|
262 -B NAME include session NAME and all descendants |
|
263 -D DIR include session directory and select its sessions |
|
264 -I operation: report session imports |
|
265 -M operation: Mercurial repository check for theory files |
|
266 -R operate on requirements of selected sessions |
|
267 -U operation: update theory imports to use session qualifiers |
|
268 -X NAME exclude sessions from group NAME and all descendants |
|
269 -a select all sessions |
|
270 -d DIR include session directory |
|
271 -g NAME select session group NAME |
|
272 -i incremental update according to session graph structure |
|
273 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
274 -v verbose |
|
275 -x NAME exclude session NAME and all descendants |
|
276 |
|
277 Maintain theory imports wrt. session structure. At least one operation |
|
278 needs to be specified (see options -I -M -U). |
|
279 """, |
|
280 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
|
281 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
|
282 "I" -> (_ => operation_imports = true), |
|
283 "M" -> (_ => operation_repository_files = true), |
|
284 "R" -> (_ => requirements = true), |
|
285 "U" -> (_ => operation_update = true), |
|
286 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
|
287 "a" -> (_ => all_sessions = true), |
|
288 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
289 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
|
290 "i" -> (_ => incremental_update = true), |
|
291 "o:" -> (arg => options = options + arg), |
|
292 "v" -> (_ => verbose = true), |
|
293 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
|
294 |
|
295 val sessions = getopts(args) |
|
296 if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update)) |
|
297 getopts.usage() |
|
298 |
|
299 val selection = |
|
300 Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, |
|
301 exclude_sessions, session_groups, sessions) |
|
302 |
|
303 val progress = new Console_Progress(verbose = verbose) |
|
304 |
|
305 if (operation_imports || operation_repository_files || |
|
306 operation_update && !incremental_update) |
|
307 { |
|
308 imports(options, operation_imports = operation_imports, |
|
309 operation_repository_files = operation_repository_files, |
|
310 operation_update = operation_update, |
|
311 progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs, |
|
312 verbose = verbose) |
|
313 } |
|
314 else if (operation_update && incremental_update) { |
|
315 Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs). |
|
316 selection(selection).imports_topological_order.foreach(name => |
|
317 { |
|
318 imports(options, operation_update = operation_update, progress = progress, |
|
319 update_message = " for session " + quote(name), |
|
320 selection = Sessions.Selection(sessions = List(name)), |
|
321 dirs = dirs ::: select_dirs, verbose = verbose) |
|
322 }) |
|
323 } |
|
324 }) |
|
325 } |
|