# HG changeset patch # User wenzelm # Date 1492957111 -7200 # Node ID 479406635409fa882675b8d8d9657245e2ed2548 # Parent 29c69a599743cbba3646ed29686a46f7ebd0e9a5 support for multiple operations via options; diff -r 29c69a599743 -r 479406635409 src/Pure/Tools/imports.scala --- a/src/Pure/Tools/imports.scala Sun Apr 23 15:59:51 2017 +0200 +++ b/src/Pure/Tools/imports.scala Sun Apr 23 16:18:31 2017 +0200 @@ -49,69 +49,6 @@ } } - 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)(_ + _) @@ -144,6 +81,74 @@ } } + def imports( + options: Options, + operation_update: Boolean = false, + progress: Progress = No_Progress, + selection: Sessions.Selection = Sessions.Selection.empty, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, + verbose: Boolean = false) = + { + 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) + + if (operation_update) { + val updates = + 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 + }) + apply_updates(updates) + } + } + /* Isabelle tool wrapper */ @@ -152,6 +157,7 @@ { var select_dirs: List[Path] = Nil var requirements = false + var operation_update = false var exclude_session_groups: List[String] = Nil var all_sessions = false var dirs: List[Path] = Nil @@ -166,6 +172,7 @@ Options are: -D DIR include session directory and select its sessions -R operate on requirements of selected sessions + -U operation: update theory imports to use session qualifiers -X NAME exclude sessions from group NAME and all descendants -a select all sessions -d DIR include session directory @@ -174,12 +181,12 @@ -v verbose -x NAME exclude session NAME and all descendants - Maintain theory imports wrt. session structure. - - Old versions of files are preserved by appending "~~". + Maintain theory imports wrt. session structure. At least one operation + needs to be specified (see option -U). """, "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "R" -> (_ => requirements = true), + "U" -> (_ => operation_update = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), @@ -189,7 +196,7 @@ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) - if (args.isEmpty) getopts.usage() + if (args.isEmpty || !operation_update) getopts.usage() val selection = Sessions.Selection(requirements, all_sessions, exclude_session_groups, @@ -197,10 +204,7 @@ 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) + imports(options, operation_update = operation_update, progress = progress, + selection = selection, dirs = dirs, select_dirs = select_dirs, verbose = verbose) }) }