--- a/NEWS Wed Jan 20 23:31:23 2021 +0100
+++ b/NEWS Thu Jan 21 16:10:43 2021 +0100
@@ -288,6 +288,10 @@
(for DVI documents) has been discontinued. Former option -n has been
turned into -o with explicit file name. Minor INCOMPATIBILITY.
+* The command-line tool "isabelle components" supports new options -u
+and -x to manage $ISABELLE_HOME_USER/etc/components without manual
+editing of Isabelle configuration files.
+
* The shell function "isabelle_directory" (within etc/settings of
components) augments the list of special directories for persistent
symbolic path names. This improves portability of heap images and
--- a/lib/Tools/components Wed Jan 20 23:31:23 2021 +0100
+++ b/lib/Tools/components Thu Jan 21 16:10:43 2021 +0100
@@ -19,11 +19,15 @@
echo " -R URL component repository (default \$ISABELLE_COMPONENT_REPOSITORY)"
echo " -a resolve all missing components"
echo " -l list status"
+ echo " -u DIR update \$ISABELLE_HOME_USER/components: add directory"
+ echo " -x DIR update \$ISABELLE_HOME_USER/components: remove directory"
echo
- echo " Resolve Isabelle components via download and installation."
- echo " COMPONENTS are identified via base name."
+ echo " Resolve Isabelle components via download and installation: given COMPONENTS"
+ echo " are identified via base name. Further operations manage etc/settings and"
+ echo " etc/components in \$ISABELLE_HOME_USER."
echo
echo " ISABELLE_COMPONENT_REPOSITORY=\"$ISABELLE_COMPONENT_REPOSITORY\""
+ echo " ISABELLE_HOME_USER=\"$ISABELLE_HOME_USER\""
echo
exit 1
}
@@ -43,8 +47,9 @@
COMPONENT_REPOSITORY="$ISABELLE_COMPONENT_REPOSITORY"
ALL_MISSING=""
LIST_ONLY=""
+declare -a UPDATE_COMPONENTS=()
-while getopts "IR:al" OPT
+while getopts "IR:alu:x:" OPT
do
case "$OPT" in
I)
@@ -59,6 +64,12 @@
l)
LIST_ONLY="true"
;;
+ u)
+ UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="+$OPTARG"
+ ;;
+ x)
+ UPDATE_COMPONENTS["${#UPDATE_COMPONENTS[@]}"]="-$OPTARG"
+ ;;
\?)
usage
;;
@@ -70,7 +81,7 @@
# args
-[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" ] && usage
+[ "$#" -eq 0 -a -z "$INIT_SETTINGS" -a -z "$ALL_MISSING" -a -z "$LIST_ONLY" -a "${#UPDATE_COMPONENTS[@]}" -eq 0 ] && usage
if [ -z "$ALL_MISSING" ]; then
splitarray ":" "$@"
@@ -112,6 +123,9 @@
echo
echo "Missing components:"
for NAME in "${MISSING_COMPONENTS[@]}"; do echo " $NAME"; done
+elif [ "${#UPDATE_COMPONENTS[@]}" -ne 0 ]; then
+ isabelle_admin_build jars || exit $?
+ exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
else
for NAME in "${SELECTED_COMPONENTS[@]}"
do
--- a/src/Doc/System/Misc.thy Wed Jan 20 23:31:23 2021 +0100
+++ b/src/Doc/System/Misc.thy Thu Jan 21 16:10:43 2021 +0100
@@ -119,24 +119,28 @@
\<close>
-section \<open>Resolving Isabelle components \label{sec:tool-components}\<close>
+section \<open>Managing Isabelle components \label{sec:tool-components}\<close>
text \<open>
- The @{tool_def components} tool resolves Isabelle components:
+ The @{tool_def components} tool manages Isabelle components:
@{verbatim [display]
\<open>Usage: isabelle components [OPTIONS] [COMPONENTS ...]
Options are:
-I init user settings
- -R URL component repository
- (default $ISABELLE_COMPONENT_REPOSITORY)
+ -R URL component repository (default $ISABELLE_COMPONENT_REPOSITORY)
-a resolve all missing components
-l list status
+ -u DIR update $ISABELLE_HOME_USER/components: add directory
+ -x DIR update $ISABELLE_HOME_USER/components: remove directory
- Resolve Isabelle components via download and installation.
- COMPONENTS are identified via base name.
+ Resolve Isabelle components via download and installation: given COMPONENTS
+ are identified via base name. Further operations manage etc/settings and
+ etc/components in $ISABELLE_HOME_USER.
- ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"\<close>}
+ ISABELLE_COMPONENT_REPOSITORY="..."
+ ISABELLE_HOME_USER="..."
+\<close>}
Components are initialized as described in \secref{sec:components} in a
permissive manner, which can mark components as ``missing''. This state is
@@ -153,13 +157,20 @@
installation takes place in the location that was specified in the attempt
to initialize the component before.
+ \<^medskip>
Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components
with their location (full name) within the file-system.
+ \<^medskip>
Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard
components specified in the Isabelle repository clone --- this does not make
any sense for regular Isabelle releases. If the file already exists, it
needs to be edited manually according to the printed explanation.
+
+ \<^medskip>
+ Options \<^verbatim>\<open>-u\<close> and \<^verbatim>\<open>-x\<close> operate on user components listed in
+ \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>: this avoid manual editing if
+ Isabelle configuration files.
\<close>
--- a/src/Pure/Admin/components.scala Wed Jan 20 23:31:23 2021 +0100
+++ b/src/Pure/Admin/components.scala Thu Jan 21 16:10:43 2021 +0100
@@ -130,6 +130,55 @@
File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n"))
+ /** manage user components **/
+
+ val components_path = Path.explode("$ISABELLE_HOME_USER/components")
+
+ def read_components(): List[String] =
+ if (components_path.is_file) Library.trim_split_lines(File.read(components_path))
+ else Nil
+
+ def write_components(lines: List[String]): Unit =
+ {
+ Isabelle_System.make_directory(components_path.dir)
+ File.write(components_path, Library.terminate_lines(lines))
+ }
+
+ def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit =
+ {
+ val path = path0.expand.absolute
+ if (!(path + Path.explode("etc/settings")).is_file &&
+ !(path + Path.explode("etc/components")).is_file) error("Bad component directory: " + path)
+
+ val lines1 = read_components()
+ val lines2 =
+ lines1.filter(line =>
+ line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path))
+ val lines3 = if (add) lines2 ::: List(path.implode) else lines2
+
+ if (lines1 != lines3) write_components(lines3)
+
+ val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed"
+ progress.echo(prefix + " component " + path)
+ }
+
+
+ /* main entry point */
+
+ def main(args: Array[String]): Unit =
+ {
+ Command_Line.tool {
+ for (arg <- args) {
+ val add =
+ if (arg.startsWith("+")) true
+ else if (arg.startsWith("-")) false
+ else error("Bad argument: " + quote(arg))
+ val path = Path.explode(arg.substring(1))
+ update_components(add, path, progress = new Console_Progress)
+ }
+ }
+ }
+
/** build and publish components **/