# HG changeset patch
# User wenzelm
# Date 1669819138 -3600
# Node ID b10926dbb763d665f7bf2af52b360ec3370bba40
# Parent  fef0195f8d8e68bdea58966fa52b78d31901ea2d
more standard component build process;

diff -r fef0195f8d8e -r b10926dbb763 src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Wed Nov 30 15:32:25 2022 +0100
+++ b/src/Pure/Admin/build_sqlite.scala	Wed Nov 30 15:38:58 2022 +0100
@@ -10,8 +10,11 @@
 object Build_SQLite {
   /* build sqlite */
 
+  val default_download_url =
+    "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.36.0.3/sqlite-jdbc-3.36.0.3.jar"
+
   def build_sqlite(
-    download_url: String,
+    download_url: String = default_download_url,
     progress: Progress = new Progress,
     target_dir: Path = Path.current
   ): Unit = {
@@ -82,28 +85,28 @@
       Scala_Project.here,
       { args =>
         var target_dir = Path.current
+        var download_url = default_download_url
 
         val getopts = Getopts("""
 Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
 
   Options are:
     -D DIR       target directory (default ".")
+    -U URL       download URL
+                 (default: """" + default_download_url + """")
 
   Build sqlite-jdbc component from the specified download URL (JAR), see also
   https://github.com/xerial/sqlite-jdbc and
   https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
 """,
-          "D:" -> (arg => target_dir = Path.explode(arg)))
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "U:" -> (arg => download_url = arg))
 
         val more_args = getopts(args)
-        val download_url =
-          more_args match {
-            case List(download_url) => download_url
-            case _ => getopts.usage()
-          }
+        if (more_args.nonEmpty) getopts.usage()
 
         val progress = new Console_Progress()
 
-        build_sqlite(download_url, progress = progress, target_dir = target_dir)
+        build_sqlite(download_url = download_url, progress = progress, target_dir = target_dir)
       })
 }