# HG changeset patch
# User wenzelm
# Date 1611241843 -3600
# Node ID fc828f64da5b1c191926a5d5d4474ff8b3dab72c
# Parent  b95844134b9239f6d2c62955c0066e76522deec1
support isabelle components -u and -x;

diff -r b95844134b92 -r fc828f64da5b NEWS
--- 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
diff -r b95844134b92 -r fc828f64da5b lib/Tools/components
--- 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
diff -r b95844134b92 -r fc828f64da5b src/Doc/System/Misc.thy
--- 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>
 
 
diff -r b95844134b92 -r fc828f64da5b src/Pure/Admin/components.scala
--- 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 **/