1/* Title: Pure/Tools/imports.scala 2 Author: Makarius 3 4Maintain theory imports wrt. session structure. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11 12 13object 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 deps = 103 Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs). 104 selection_deps(selection, progress = progress, verbose = verbose).check_errors 105 106 val root_keywords = Sessions.root_syntax.keywords 107 108 if (operation_imports) { 109 val report_imports: List[Report] = 110 deps.sessions_structure.build_topological_order.map((session_name: String) => 111 { 112 val info = deps.sessions_structure(session_name) 113 val session_base = deps(session_name) 114 115 val declared_imports = 116 deps.sessions_structure.imports_requirements(List(session_name)).toSet 117 118 val extra_imports = 119 (for { 120 a <- session_base.known.theory_names 121 if session_base.theory_qualifier(a) == info.name 122 b <- deps.all_known.get_file(a.path.file) 123 qualifier = session_base.theory_qualifier(b) 124 if !declared_imports.contains(qualifier) 125 } yield qualifier).toSet 126 127 val loaded_imports = 128 deps.sessions_structure.imports_requirements( 129 session_base.loaded_theories.keys.map(a => 130 session_base.theory_qualifier(session_base.known.theories(a).name))) 131 .toSet - session_name 132 133 val minimal_imports = 134 loaded_imports.filter(s1 => 135 !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2))) 136 137 def make_result(set: Set[String]): Option[List[String]] = 138 if (set.isEmpty) None 139 else Some(deps.sessions_structure.imports_topological_order.filter(set)) 140 141 Report(info, declared_imports, make_result(extra_imports), 142 if (loaded_imports == declared_imports - session_name) None 143 else make_result(minimal_imports)) 144 }) 145 146 progress.echo("\nPotential session imports:") 147 for { 148 report <- report_imports.sortBy(_.declared_imports.size) 149 potential_imports <- report.potential_imports 150 } progress.echo(report.print(root_keywords, potential_imports)) 151 152 progress.echo("\nActual session imports:") 153 for { 154 report <- report_imports 155 actual_imports <- report.actual_imports 156 } progress.echo(report.print(root_keywords, actual_imports)) 157 } 158 159 if (operation_repository_files) { 160 progress.echo("\nMercurial repository check:") 161 val unused_files = 162 for { 163 (_, dir) <- Sessions.directories(dirs, select_dirs) 164 file <- repository_files(progress, dir, file => file.getName.endsWith(".thy")) 165 if deps.all_known.get_file(file).isEmpty 166 } yield file 167 unused_files.foreach(file => progress.echo("unused file " + quote(file.toString))) 168 } 169 170 if (operation_update) { 171 progress.echo("\nUpdate theory imports" + update_message + ":") 172 val updates = 173 deps.sessions_structure.build_topological_order.flatMap(session_name => 174 { 175 val info = deps.sessions_structure(session_name) 176 val session_base = deps(session_name) 177 val session_resources = new Resources(session_base) 178 val imports_base = session_base.get_imports 179 val imports_resources = new Resources(imports_base) 180 181 def standard_import(qualifier: String, dir: String, s: String): String = 182 imports_resources.standard_import(session_base, qualifier, dir, s) 183 184 val updates_root = 185 for { 186 (_, pos) <- info.theories.flatMap(_._2) 187 upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _)) 188 } yield upd 189 190 val updates_theories = 191 (for { 192 name <- session_base.known.theories_local.iterator.map(p => p._2.name) 193 if session_base.theory_qualifier(name) == info.name 194 (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports 195 upd <- update_name(session_base.overall_syntax.keywords, pos, 196 standard_import(session_base.theory_qualifier(name), name.master_dir, _)) 197 } yield upd).toList 198 199 updates_root ::: updates_theories 200 }) 201 202 val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _) 203 val conflicts = 204 file_updates.iterator_list.flatMap({ case (file, upds) => 205 Library.duplicates(upds.sortBy(_.range.start), 206 (x: Update, y: Update) => x.range overlaps y.range) match 207 { 208 case Nil => None 209 case bad => Some((file, bad)) 210 } 211 }) 212 if (conflicts.nonEmpty) 213 error(cat_lines( 214 conflicts.map({ case (file, bad) => 215 "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") }))) 216 217 for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) { 218 progress.echo("file " + quote(file.toString)) 219 val edits = 220 upds.sortBy(upd => - upd.range.start).flatMap(upd => 221 Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text)) 222 val new_text = 223 (File.read(file) /: edits)({ case (text, edit) => 224 edit.edit(text, 0) match { 225 case (None, text1) => text1 226 case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file) 227 } 228 }) 229 File.write_backup2(Path.explode(File.standard_path(file)), new_text) 230 } 231 } 232 } 233 234 235 /* Isabelle tool wrapper */ 236 237 val isabelle_tool = 238 Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args => 239 { 240 var base_sessions: List[String] = Nil 241 var select_dirs: List[Path] = Nil 242 var operation_imports = false 243 var operation_repository_files = false 244 var requirements = false 245 var operation_update = false 246 var exclude_session_groups: List[String] = Nil 247 var all_sessions = false 248 var dirs: List[Path] = Nil 249 var session_groups: List[String] = Nil 250 var incremental_update = false 251 var options = Options.init() 252 var verbose = false 253 var exclude_sessions: List[String] = Nil 254 255 val getopts = Getopts(""" 256Usage: isabelle imports [OPTIONS] [SESSIONS ...] 257 258 Options are: 259 -B NAME include session NAME and all descendants 260 -D DIR include session directory and select its sessions 261 -I operation: report session imports 262 -M operation: Mercurial repository check for theory files 263 -R operate on requirements of selected sessions 264 -U operation: update theory imports to use session qualifiers 265 -X NAME exclude sessions from group NAME and all descendants 266 -a select all sessions 267 -d DIR include session directory 268 -g NAME select session group NAME 269 -i incremental update according to session graph structure 270 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 271 -v verbose 272 -x NAME exclude session NAME and all descendants 273 274 Maintain theory imports wrt. session structure. At least one operation 275 needs to be specified (see options -I -M -U). 276""", 277 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), 278 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), 279 "I" -> (_ => operation_imports = true), 280 "M" -> (_ => operation_repository_files = true), 281 "R" -> (_ => requirements = true), 282 "U" -> (_ => operation_update = true), 283 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), 284 "a" -> (_ => all_sessions = true), 285 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), 286 "g:" -> (arg => session_groups = session_groups ::: List(arg)), 287 "i" -> (_ => incremental_update = true), 288 "o:" -> (arg => options = options + arg), 289 "v" -> (_ => verbose = true), 290 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) 291 292 val sessions = getopts(args) 293 if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update)) 294 getopts.usage() 295 296 val selection = 297 Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, 298 exclude_sessions, session_groups, sessions) 299 300 val progress = new Console_Progress(verbose = verbose) 301 302 if (operation_imports || operation_repository_files || 303 operation_update && !incremental_update) 304 { 305 imports(options, operation_imports = operation_imports, 306 operation_repository_files = operation_repository_files, 307 operation_update = operation_update, 308 progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs, 309 verbose = verbose) 310 } 311 else if (operation_update && incremental_update) { 312 Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs). 313 selection(selection).imports_topological_order.foreach(name => 314 { 315 imports(options, operation_update = operation_update, progress = progress, 316 update_message = " for session " + quote(name), 317 selection = Sessions.Selection(sessions = List(name)), 318 dirs = dirs ::: select_dirs, verbose = verbose) 319 }) 320 } 321 }) 322} 323