| author | wenzelm | 
| Mon, 16 Sep 2024 15:49:36 +0200 | |
| changeset 80886 | 5d562dd387ae | 
| parent 79958 | 6c4e20a02ac7 | 
| child 81602 | 3b93da12e9bd | 
| permissions | -rw-r--r-- | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 1 | /* Title: Pure/Admin/component_jsoup.scala | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 2 | Author: Makarius | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 3 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 4 | Build Isabelle jsoup component from official download. | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 5 | */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 6 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 7 | package isabelle | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 8 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 9 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 10 | object Component_Jsoup {
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 11 | /* build jsoup */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 12 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 13 | val default_download_url = | 
| 79958 | 14 | "https://repo1.maven.org/maven2/org/jsoup/jsoup/1.17.2/jsoup-1.17.2.jar" | 
| 77619 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 15 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 16 | def build_jsoup( | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 17 | download_url: String = default_download_url, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 18 | progress: Progress = new Progress, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 19 | target_dir: Path = Path.current | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 20 |   ): Unit = {
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 21 | val Download_Name = """^.*/([^/]+)\.jar""".r | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 22 | val download_name = | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 23 |       download_url match {
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 24 | case Download_Name(download_name) => download_name | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 25 |         case _ => error("Malformed jar download URL: " + quote(download_url))
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 26 | } | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 27 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 28 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 29 | /* component */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 30 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 31 | val component_dir = | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 32 | Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 33 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 34 | File.write(component_dir.LICENSE, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 35 |       Url.read("https://raw.githubusercontent.com/jhy/jsoup/master/LICENSE"))
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 36 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 37 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 38 | /* README */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 39 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 40 | File.write(component_dir.README, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 41 | "This is " + download_name + " from\n" + download_url + | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 42 | "\n\nSee also https://jsoup.org and https://github.com/jhy/jsoup" + | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 43 | "\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n") | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 44 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 45 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 46 | /* settings */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 47 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 48 |     component_dir.write_settings("""
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 49 | ISABELLE_JSOUP_HOME="$COMPONENT" | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 50 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 51 | classpath "$ISABELLE_JSOUP_HOME/lib/""" + download_name + """.jar" | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 52 | """) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 53 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 54 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 55 | /* jar */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 56 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 57 | val jar = component_dir.lib + Path.basic(download_name).jar | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 58 | Isabelle_System.make_directory(jar.dir) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 59 | Isabelle_System.download_file(download_url, jar, progress = progress) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 60 | } | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 61 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 62 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 63 | /* Isabelle tool wrapper */ | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 64 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 65 | val isabelle_tool = | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 66 |     Isabelle_Tool("component_jsoup", "build Isabelle jsoup component from official download",
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 67 | Scala_Project.here, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 68 |       { args =>
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 69 | var target_dir = Path.current | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 70 | var download_url = default_download_url | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 71 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 72 |         val getopts = Getopts("""
 | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 73 | Usage: isabelle component_jsoup [OPTIONS] DOWNLOAD | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 74 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 75 | Options are: | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 76 | -D DIR target directory (default ".") | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 77 | -U URL download URL | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 78 | (default: """" + default_download_url + """") | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 79 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 80 | Build jsoup component from the specified download URL (JAR). | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 81 | """, | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 82 | "D:" -> (arg => target_dir = Path.explode(arg)), | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 83 | "U:" -> (arg => download_url = arg)) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 84 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 85 | val more_args = getopts(args) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 86 | if (more_args.nonEmpty) getopts.usage() | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 87 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 88 | val progress = new Console_Progress() | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 89 | |
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 90 | build_jsoup(download_url = download_url, progress = progress, target_dir = target_dir) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 91 | }) | 
| 
6d0985955872
discontinued apache-commons in favour of jsoup, which is smaller and more useful;
 wenzelm parents: diff
changeset | 92 | } |