# HG changeset patch
# User wenzelm
# Date 1674509605 -3600
# Node ID a5d3f3c07de87380cb66c915964c483822a5de05
# Parent  e293216df99453da79c38dce22833456a1141848# Parent  422c57b75b170f0b9f393bb93b8e099342a6f471
merged

diff -r e293216df994 -r a5d3f3c07de8 Admin/Windows/Cygwin/setup_server
--- a/Admin/Windows/Cygwin/setup_server	Mon Jan 23 14:34:07 2023 +0100
+++ b/Admin/Windows/Cygwin/setup_server	Mon Jan 23 22:33:25 2023 +0100
@@ -15,7 +15,7 @@
   local DIR="${2:-.}"
   mkdir -p "$DIR" || fail "Cannot create directory: \"$DIR\""
   echo "Downloading $URL ..."
-  curl --fail --silent "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
+  curl --fail --silent --location "$URL" > "$DIR"/"$(basename "$URL")" || fail "FAILED"
 }
 
 download "$CYGWIN_MAIN/setup-x86_64.exe"
diff -r e293216df994 -r a5d3f3c07de8 lib/Tools/components
--- a/lib/Tools/components	Mon Jan 23 14:34:07 2023 +0100
+++ b/lib/Tools/components	Mon Jan 23 22:33:25 2023 +0100
@@ -130,6 +130,7 @@
   isabelle scala_build || exit $?
   exec isabelle java isabelle.Components "${UPDATE_COMPONENTS[@]}"
 else
+  source "$ISABELLE_HOME/lib/scripts/download_file"
   for NAME in "${SELECTED_COMPONENTS[@]}"
   do
     BASE_NAME="$(basename "$NAME")"
@@ -144,30 +145,11 @@
       echo "Skipping existing component \"$FULL_NAME\""
     else
       if [ ! -e "${FULL_NAME}.tar.gz" ]; then
-        REMOTE="$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz"
-        type -p curl > /dev/null || fail "Cannot download files: missing curl"
-        echo "Getting \"$REMOTE\""
-        mkdir -p "$(dirname "$FULL_NAME")"
-
-        CURL_OPTIONS="--fail --silent --location"
-        if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
-          case $(sw_vers -productVersion) in
-            10.*)
-              CURL_OPTIONS="$CURL_OPTIONS --insecure"
-              ;;
-          esac
-        fi
-        if curl $CURL_OPTIONS "$REMOTE" > "${FULL_NAME}.tar.gz.part"
-        then
-          mv -f "${FULL_NAME}.tar.gz.part" "${FULL_NAME}.tar.gz"
-        else
-          rm -f "${FULL_NAME}.tar.gz.part"
-          fail "Failed to download \"$REMOTE\""
-        fi
+        download_file "$COMPONENT_REPOSITORY/${BASE_NAME}.tar.gz" "${FULL_NAME}.tar.gz" || exit $?
       fi
       if [ -e "${FULL_NAME}.tar.gz" ]; then
         echo "Unpacking \"${FULL_NAME}.tar.gz\""
-        tar -C "$(dirname "$FULL_NAME")" -x -f "${FULL_NAME}.tar.gz" || exit 2
+        tar -C "$(dirname "$FULL_NAME")" -x -z -f "${FULL_NAME}.tar.gz" || exit 2
       fi
     fi
   done
diff -r e293216df994 -r a5d3f3c07de8 lib/scripts/download_file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/download_file	Mon Jan 23 22:33:25 2023 +0100
@@ -0,0 +1,40 @@
+# -*- shell-script -*- :mode=shellscript:
+#
+# Bash function to download file via "curl".
+
+function download_file ()
+{
+  [ "$#" -ne 2 ] && {
+    echo "Bad arguments for download_file" >&2
+    return 2
+  }
+  local REMOTE="$1"
+  local LOCAL="$2"
+
+  type -p curl > /dev/null || {
+    echo "Require \"curl\" to download files" >&2
+    return 2
+  }
+
+  local CURL_OPTIONS="--fail --silent --location"
+  if [ "$(uname -s)" = "Darwin" ]
+  then
+    case $(sw_vers -productVersion) in
+      10.*)
+        CURL_OPTIONS="$CURL_OPTIONS --insecure"
+        ;;
+    esac
+  fi
+
+  echo "Getting \"$REMOTE\""
+  mkdir -p "$(dirname "$LOCAL")"
+
+  if curl $CURL_OPTIONS "$REMOTE" > "${LOCAL}.part"
+  then
+    mv -f "${LOCAL}.part" "$LOCAL"
+  else
+    rm -f "${LOCAL}.part"
+    echo "Failed to download \"$REMOTE\"" >&2
+    return 2
+  fi
+}
diff -r e293216df994 -r a5d3f3c07de8 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Mon Jan 23 22:33:25 2023 +0100
@@ -191,7 +191,7 @@
         other_isabelle.init_components(
           component_repository = component_repository,
           components_base = components_base,
-          catalogs = List("main", "optional"))
+          catalogs = Components.optional_catalogs)
       other_isabelle.init_settings(component_settings ::: init_settings)
       other_isabelle.resolve_components(echo = verbose)
       val ml_platform =
@@ -212,7 +212,7 @@
           Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
         }
         other_isabelle.bash(
-          "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
+          "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty")) + ":$PATH\" " +
             "bin/isabelle jedit -b", redirect = true, echo = verbose).check
 
         for {
diff -r e293216df994 -r a5d3f3c07de8 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Admin/build_release.scala	Mon Jan 23 22:33:25 2023 +0100
@@ -467,8 +467,7 @@
       val other_isabelle = context.other_isabelle(context.dist_dir)
 
       other_isabelle.init_settings(
-        other_isabelle.init_components(
-          components_base = context.components_base, catalogs = List("main")))
+        other_isabelle.init_components(components_base = context.components_base))
       other_isabelle.resolve_components(echo = true)
 
       try {
diff -r e293216df994 -r a5d3f3c07de8 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Mon Jan 23 22:33:25 2023 +0100
@@ -8,11 +8,14 @@
 
 
 object Other_Isabelle {
-  def apply(isabelle_home: Path,
-      isabelle_identifier: String = "",
-      user_home: Path = Path.USER_HOME,
-      progress: Progress = new Progress): Other_Isabelle =
+  def apply(
+    isabelle_home: Path,
+    isabelle_identifier: String = "",
+    user_home: Path = Path.USER_HOME,
+    progress: Progress = new Progress
+  ): Other_Isabelle = {
     new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
+  }
 }
 
 final class Other_Isabelle private(
@@ -65,7 +68,7 @@
   def init_components(
     component_repository: String = Components.default_component_repository,
     components_base: Path = Components.default_components_base,
-    catalogs: List[String] = Nil,
+    catalogs: List[String] = Components.default_catalogs,
     components: List[String] = Nil
   ): List[String] = {
     val dir = Components.admin(isabelle_home)
diff -r e293216df994 -r a5d3f3c07de8 src/Pure/General/ssh.scala
--- a/src/Pure/General/ssh.scala	Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/General/ssh.scala	Mon Jan 23 22:33:25 2023 +0100
@@ -190,6 +190,19 @@
         progress_stderr = progress_stderr, strict = strict)
     }
 
+    override def download_file(
+      url_name: String,
+      file: Path,
+      progress: Progress = new Progress
+    ): Unit = {
+      val cmd_line =
+        File.read(Path.explode("~~/lib/scripts/download_file")) + "\n" +
+          "download_file " + Bash.string(url_name) + " " + bash_path(file)
+      execute(cmd_line,
+        progress_stdout = progress.echo,
+        progress_stderr = progress.echo).check
+    }
+
     override lazy val isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(ssh))
 
 
@@ -213,6 +226,14 @@
       path
     }
 
+    override def copy_file(src: Path, dst: Path): Unit = {
+      val direct = if (is_dir(dst)) "/." else ""
+      if (!execute("cp -a " + bash_path(src) + " " + bash_path(dst) + direct).ok) {
+        error("Failed to copy file " + expand_path(src) + " to " +
+          expand_path(dst) + " (ssh " + toString + ")")
+      }
+    }
+
     def read_dir(path: Path): List[String] =
       run_sftp("@cd " + sftp_path(path) + "\n@ls -1 -a").out_lines.flatMap(s =>
         if (s == "." || s == "..") None
@@ -339,6 +360,7 @@
     def is_file(path: Path): Boolean = path.is_file
     def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
     def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
+    def copy_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
     def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
     def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
     def read_bytes(path: Path): Bytes = Bytes.read(path)
@@ -355,6 +377,9 @@
         env = if (settings) Isabelle_System.settings() else null,
         strict = strict)
 
+    def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
+      Isabelle_System.download_file(url_name, file, progress = progress)
+
     def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
   }
 
diff -r e293216df994 -r a5d3f3c07de8 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/System/components.scala	Mon Jan 23 22:33:25 2023 +0100
@@ -40,36 +40,51 @@
 
   val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE")
 
+  val default_catalogs: List[String] = List("main")
+  val optional_catalogs: List[String] = List("main", "optional")
+
   def admin(dir: Path): Path = dir + Path.explode("Admin/components")
 
   def contrib(dir: Path = Path.current, name: String = ""): Path =
     dir + Path.explode("contrib") + Path.explode(name)
 
-  def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
+  def unpack(
+    dir: Path,
+    archive: Path,
+    ssh: SSH.System = SSH.Local,
+    progress: Progress = new Progress
+  ): String = {
     val name = Archive.get_name(archive.file_name)
     progress.echo("Unpacking " + name)
-    Isabelle_System.extract(archive, dir)
+    ssh.execute(
+      "tar -C " + File.bash_path(dir) + " -x -z -f " + File.bash_path(archive),
+      progress_stdout = progress.echo,
+      progress_stderr = progress.echo).check
     name
   }
 
-  def resolve(base_dir: Path, names: List[String],
+  def resolve(
+    base_dir: Path,
+    names: List[String],
     target_dir: Option[Path] = None,
     copy_dir: Option[Path] = None,
+    component_repository: String = Components.default_component_repository,
+    ssh: SSH.System = SSH.Local,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.make_directory(base_dir)
+    ssh.make_directory(base_dir)
     for (name <- names) {
       val archive_name = Archive(name)
       val archive = base_dir + Path.explode(archive_name)
-      if (!archive.is_file) {
-        val remote = Components.default_component_repository + "/" + archive_name
-        Isabelle_System.download_file(remote, archive, progress = progress)
+      if (!ssh.is_file(archive)) {
+        val remote = Url.append_path(component_repository, archive_name)
+        ssh.download_file(remote, archive, progress = progress)
       }
       for (dir <- copy_dir) {
-        Isabelle_System.make_directory(dir)
-        Isabelle_System.copy_file(archive, dir)
+        ssh.make_directory(dir)
+        ssh.copy_file(archive, dir)
       }
-      unpack(target_dir getOrElse base_dir, archive, progress = progress)
+      unpack(target_dir getOrElse base_dir, archive, ssh = ssh, progress = progress)
     }
   }
 
diff -r e293216df994 -r a5d3f3c07de8 src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala	Mon Jan 23 14:34:07 2023 +0100
+++ b/src/Pure/Tools/build_docker.scala	Mon Jan 23 22:33:25 2023 +0100
@@ -68,7 +68,7 @@
 # Isabelle
 WORKDIR /home/isabelle
 """ + (if (is_remote)
-       "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
+       "RUN curl --fail --silent --location " + Bash.string(app_archive) + " > Isabelle.tar.gz"
       else "COPY Isabelle.tar.gz .") + """
 RUN tar xzf Isabelle.tar.gz && \
   mv """ + isabelle_name + """ Isabelle && \