# HG changeset patch # User wenzelm # Date 1492955991 -7200 # Node ID 29c69a599743cbba3646ed29686a46f7ebd0e9a5 # Parent a04afc400156c3d68a91aeeeae51426ad7da25b0 clarified tool name -- more official status; diff -r a04afc400156 -r 29c69a599743 NEWS --- a/NEWS Sun Apr 23 14:27:22 2017 +0200 +++ b/NEWS Sun Apr 23 15:59:51 2017 +0200 @@ -201,6 +201,9 @@ a negative value means the current state in the ML heap image remains unchanged. +* Command-line tool "isabelle imports" helps to maintain theory imports +wrt. session structure. + New in Isabelle2016-1 (December 2016) diff -r a04afc400156 -r 29c69a599743 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Sun Apr 23 14:27:22 2017 +0200 +++ b/src/Pure/System/isabelle_tool.scala Sun Apr 23 15:59:51 2017 +0200 @@ -108,6 +108,7 @@ Build_Stats.isabelle_tool, Check_Sources.isabelle_tool, Doc.isabelle_tool, + Imports.isabelle_tool, ML_Process.isabelle_tool, NEWS.isabelle_tool, Options.isabelle_tool, @@ -115,7 +116,6 @@ Remote_DMG.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Header.isabelle_tool, - Update_Imports.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool, diff -r a04afc400156 -r 29c69a599743 src/Pure/Tools/imports.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/imports.scala Sun Apr 23 15:59:51 2017 +0200 @@ -0,0 +1,206 @@ +/* Title: Pure/Tools/imports.scala + Author: Makarius + +Maintain theory imports wrt. session structure. +*/ + +package isabelle + + +import java.io.{File => JFile} + + +object Imports +{ + /* update imports */ + + sealed case class Update(range: Text.Range, old_text: String, new_text: String) + { + def edits: List[Text.Edit] = + Text.Edit.replace(range.start, old_text, new_text) + + override def toString: String = + range.toString + ": " + old_text + " -> " + new_text + } + + def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String) + : Option[(JFile, Update)] = + { + val file = + pos match { + case Position.File(file) => Path.explode(file).file.getCanonicalFile + case _ => error("Missing file in position" + Position.here(pos)) + } + + val text = File.read(file) + + val range = + pos match { + case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range) + case _ => error("Missing range in position" + Position.here(pos)) + } + + Token.read_name(keywords, range.substring(text)) match { + case Some(tok) => + val s1 = tok.source + val s2 = Token.quote_name(keywords, update(tok.content)) + if (s1 == s2) None else Some((file, Update(range, s1, s2))) + case None => error("Name token expected" + Position.here(pos)) + } + } + + def update_imports( + options: Options, + progress: Progress = No_Progress, + selection: Sessions.Selection = Sessions.Selection.empty, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, + verbose: Boolean = false): List[(JFile, Update)] = + { + val full_sessions = Sessions.load(options, dirs, select_dirs) + val (selected, selected_sessions) = full_sessions.selection(selection) + + val deps = + Sessions.deps(selected_sessions, progress = progress, verbose = verbose, + global_theories = full_sessions.global_theories) + + selected.flatMap(session_name => + { + val info = full_sessions(session_name) + val session_base = deps(session_name) + val session_resources = new Resources(session_base) + val imports_resources = new Resources(session_base.get_imports) + + val local_theories = + (for { + (_, name) <- session_base.known.theories_local.iterator + if session_resources.theory_qualifier(name) == info.theory_qualifier + } yield name).toSet + + def standard_import(qualifier: String, dir: String, s: String): String = + { + val name = imports_resources.import_name(qualifier, dir, s) + val file = Path.explode(name.node).file + val s1 = + imports_resources.session_base.known.get_file(file) match { + case Some(name1) if session_resources.theory_qualifier(name1) != qualifier => + name1.theory + case Some(name1) if Thy_Header.is_base_name(s) => + name1.theory_base_name + case _ => s + } + val name2 = imports_resources.import_name(qualifier, dir, s1) + if (name.node == name2.node) s1 else s + } + + val updates_root = + for { + (_, pos) <- info.theories.flatMap(_._2) + upd <- update_name(Sessions.root_syntax.keywords, pos, + standard_import(info.theory_qualifier, info.dir.implode, _)) + } yield upd + + val updates_theories = + for { + (_, name) <- session_base.known.theories_local.toList + (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports + upd <- update_name(session_base.syntax.keywords, pos, + standard_import(session_resources.theory_qualifier(name), name.master_dir, _)) + } yield upd + + updates_root ::: updates_theories + }) + } + + def apply_updates(updates: List[(JFile, Update)]) + { + val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _) + val conflicts = + file_updates.iterator_list.flatMap({ case (file, upds) => + Library.duplicates(upds.sortBy(_.range.start), + (x: Update, y: Update) => x.range overlaps y.range) match + { + case Nil => None + case bad => Some((file, bad)) + } + }) + if (conflicts.nonEmpty) + error(cat_lines( + conflicts.map({ case (file, bad) => + "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") }))) + + for ((file, upds) <- file_updates.iterator_list) { + val edits = + upds.sortBy(upd => - upd.range.start).flatMap(upd => + Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text)) + val new_text = + (File.read(file) /: edits)({ case (text, edit) => + edit.edit(text, 0) match { + case (None, text1) => text1 + case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file) + } + }) + File.write_backup2(Path.explode(File.standard_path(file)), new_text) + } + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args => + { + var select_dirs: List[Path] = Nil + var requirements = false + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var options = Options.init() + var verbose = false + var exclude_sessions: List[String] = Nil + + val getopts = Getopts(""" +Usage: isabelle imports [OPTIONS] [SESSIONS ...] + + Options are: + -D DIR include session directory and select its sessions + -R operate on requirements of selected sessions + -X NAME exclude sessions from group NAME and all descendants + -a select all sessions + -d DIR include session directory + -g NAME select session group NAME + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -v verbose + -x NAME exclude session NAME and all descendants + + Maintain theory imports wrt. session structure. + + Old versions of files are preserved by appending "~~". +""", + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "R" -> (_ => requirements = true), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "o:" -> (arg => options = options + arg), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + + val sessions = getopts(args) + if (args.isEmpty) getopts.usage() + + val selection = + Sessions.Selection(requirements, all_sessions, exclude_session_groups, + exclude_sessions, session_groups, sessions) + + val progress = new Console_Progress(verbose = verbose) + + val updates = + update_imports(options, progress = progress, selection = selection, + dirs = dirs, select_dirs = select_dirs, verbose = verbose) + + apply_updates(updates) + }) +} diff -r a04afc400156 -r 29c69a599743 src/Pure/Tools/update_imports.scala --- a/src/Pure/Tools/update_imports.scala Sun Apr 23 14:27:22 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,206 +0,0 @@ -/* Title: Pure/Tools/update_imports.scala - Author: Makarius - -Update theory imports to use session qualifiers. -*/ - -package isabelle - - -import java.io.{File => JFile} - - -object Update_Imports -{ - /* update imports */ - - sealed case class Update(range: Text.Range, old_text: String, new_text: String) - { - def edits: List[Text.Edit] = - Text.Edit.replace(range.start, old_text, new_text) - - override def toString: String = - range.toString + ": " + old_text + " -> " + new_text - } - - def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String) - : Option[(JFile, Update)] = - { - val file = - pos match { - case Position.File(file) => Path.explode(file).file.getCanonicalFile - case _ => error("Missing file in position" + Position.here(pos)) - } - - val text = File.read(file) - - val range = - pos match { - case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range) - case _ => error("Missing range in position" + Position.here(pos)) - } - - Token.read_name(keywords, range.substring(text)) match { - case Some(tok) => - val s1 = tok.source - val s2 = Token.quote_name(keywords, update(tok.content)) - if (s1 == s2) None else Some((file, Update(range, s1, s2))) - case None => error("Name token expected" + Position.here(pos)) - } - } - - def update_imports( - options: Options, - progress: Progress = No_Progress, - selection: Sessions.Selection = Sessions.Selection.empty, - dirs: List[Path] = Nil, - select_dirs: List[Path] = Nil, - verbose: Boolean = false): List[(JFile, Update)] = - { - val full_sessions = Sessions.load(options, dirs, select_dirs) - val (selected, selected_sessions) = full_sessions.selection(selection) - - val deps = - Sessions.deps(selected_sessions, progress = progress, verbose = verbose, - global_theories = full_sessions.global_theories) - - selected.flatMap(session_name => - { - val info = full_sessions(session_name) - val session_base = deps(session_name) - val session_resources = new Resources(session_base) - val imports_resources = new Resources(session_base.get_imports) - - val local_theories = - (for { - (_, name) <- session_base.known.theories_local.iterator - if session_resources.theory_qualifier(name) == info.theory_qualifier - } yield name).toSet - - def standard_import(qualifier: String, dir: String, s: String): String = - { - val name = imports_resources.import_name(qualifier, dir, s) - val file = Path.explode(name.node).file - val s1 = - imports_resources.session_base.known.get_file(file) match { - case Some(name1) if session_resources.theory_qualifier(name1) != qualifier => - name1.theory - case Some(name1) if Thy_Header.is_base_name(s) => - name1.theory_base_name - case _ => s - } - val name2 = imports_resources.import_name(qualifier, dir, s1) - if (name.node == name2.node) s1 else s - } - - val updates_root = - for { - (_, pos) <- info.theories.flatMap(_._2) - upd <- update_name(Sessions.root_syntax.keywords, pos, - standard_import(info.theory_qualifier, info.dir.implode, _)) - } yield upd - - val updates_theories = - for { - (_, name) <- session_base.known.theories_local.toList - (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports - upd <- update_name(session_base.syntax.keywords, pos, - standard_import(session_resources.theory_qualifier(name), name.master_dir, _)) - } yield upd - - updates_root ::: updates_theories - }) - } - - def apply_updates(updates: List[(JFile, Update)]) - { - val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _) - val conflicts = - file_updates.iterator_list.flatMap({ case (file, upds) => - Library.duplicates(upds.sortBy(_.range.start), - (x: Update, y: Update) => x.range overlaps y.range) match - { - case Nil => None - case bad => Some((file, bad)) - } - }) - if (conflicts.nonEmpty) - error(cat_lines( - conflicts.map({ case (file, bad) => - "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") }))) - - for ((file, upds) <- file_updates.iterator_list) { - val edits = - upds.sortBy(upd => - upd.range.start).flatMap(upd => - Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text)) - val new_text = - (File.read(file) /: edits)({ case (text, edit) => - edit.edit(text, 0) match { - case (None, text1) => text1 - case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file) - } - }) - File.write_backup2(Path.explode(File.standard_path(file)), new_text) - } - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = - Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args => - { - var select_dirs: List[Path] = Nil - var requirements = false - var exclude_session_groups: List[String] = Nil - var all_sessions = false - var dirs: List[Path] = Nil - var session_groups: List[String] = Nil - var options = Options.init() - var verbose = false - var exclude_sessions: List[String] = Nil - - val getopts = Getopts(""" -Usage: isabelle update_imports [OPTIONS] [SESSIONS ...] - - Options are: - -D DIR include session directory and select its sessions - -R operate on requirements of selected sessions - -X NAME exclude sessions from group NAME and all descendants - -a select all sessions - -d DIR include session directory - -g NAME select session group NAME - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -v verbose - -x NAME exclude session NAME and all descendants - - Update theory imports to use session qualifiers. - - Old versions of files are preserved by appending "~~". -""", - "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), - "R" -> (_ => requirements = true), - "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), - "a" -> (_ => all_sessions = true), - "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "g:" -> (arg => session_groups = session_groups ::: List(arg)), - "o:" -> (arg => options = options + arg), - "v" -> (_ => verbose = true), - "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) - - val sessions = getopts(args) - if (args.isEmpty) getopts.usage() - - val selection = - Sessions.Selection(requirements, all_sessions, exclude_session_groups, - exclude_sessions, session_groups, sessions) - - val progress = new Console_Progress(verbose = verbose) - - val updates = - update_imports(options, progress = progress, selection = selection, - dirs = dirs, select_dirs = select_dirs, verbose = verbose) - - apply_updates(updates) - }) -} diff -r a04afc400156 -r 29c69a599743 src/Pure/build-jars --- a/src/Pure/build-jars Sun Apr 23 14:27:22 2017 +0200 +++ b/src/Pure/build-jars Sun Apr 23 15:59:51 2017 +0200 @@ -135,6 +135,7 @@ Tools/check_keywords.scala Tools/debugger.scala Tools/doc.scala + Tools/imports.scala Tools/main.scala Tools/print_operation.scala Tools/profiling_report.scala @@ -143,7 +144,6 @@ Tools/task_statistics.scala Tools/update_cartouches.scala Tools/update_header.scala - Tools/update_imports.scala Tools/update_then.scala Tools/update_theorems.scala library.scala