wrapper for "isabelle update_imports" with selection options like "isabelle build";
--- a/src/Pure/System/isabelle_tool.scala Wed Apr 19 20:10:34 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala Wed Apr 19 21:32:46 2017 +0200
@@ -115,6 +115,7 @@
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,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update_imports.scala Wed Apr 19 21:32:46 2017 +0200
@@ -0,0 +1,88 @@
+/* Title: Pure/Tools/update_imports.scala
+ Author: Makarius
+
+Update theory imports to use session qualifiers.
+*/
+
+package isabelle
+
+
+object Update_Imports
+{
+ /* update imports */
+
+ 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)
+ {
+ 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)
+
+ // FIXME
+ selected.foreach(progress.echo(_))
+ }
+
+
+ /* 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)
+
+ update_imports(options, progress = progress, selection = selection,
+ dirs = dirs, select_dirs = select_dirs, verbose = verbose)
+ })
+}
--- a/src/Pure/build-jars Wed Apr 19 20:10:34 2017 +0200
+++ b/src/Pure/build-jars Wed Apr 19 21:32:46 2017 +0200
@@ -143,6 +143,7 @@
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