author | nipkow |
Tue, 17 Jun 2025 06:29:55 +0200 | |
changeset 82732 | 71574900b6ba |
parent 82546 | 553aa1dd0feb |
permissions | -rw-r--r-- |
82546
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Admin/component_jsvg.scala |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
3 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
4 |
Build Isabelle jsvg component from official download. |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
6 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
8 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
9 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
10 |
object Component_JSVG { |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
11 |
/* build jsvg */ |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
12 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
13 |
val default_download_url = |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
14 |
"https://repo1.maven.org/maven2/com/github/weisj/jsvg/1.7.1/jsvg-1.7.1.jar" |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
15 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
16 |
def build_jsvg( |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
17 |
download_url: String = default_download_url, |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
18 |
progress: Progress = new Progress, |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
19 |
target_dir: Path = Path.current |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
20 |
): Unit = { |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
21 |
val Download_Name = """^.*/([^/]+)\.jar""".r |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
22 |
val download_name = |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
23 |
download_url match { |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
24 |
case Download_Name(download_name) => download_name |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
25 |
case _ => error("Malformed jar download URL: " + quote(download_url)) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
26 |
} |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
27 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
28 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
29 |
/* component */ |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
30 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
31 |
val component_dir = |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
32 |
Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
33 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
34 |
File.write(component_dir.LICENSE, |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
35 |
Url.read("https://raw.githubusercontent.com/weisJ/jsvg/refs/heads/master/LICENSE")) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
36 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
37 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
38 |
/* README */ |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
39 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
40 |
File.write(component_dir.README, |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
41 |
"This is a Java SVG implementation (JSVG) from\n" + download_url + |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
42 |
"\n\nSee also https://github.com/weisJ/jsvg" + |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
43 |
"\n\n Makarius\n " + Date.Format.date(Date.now()) + "\n") |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
44 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
45 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
46 |
/* settings */ |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
47 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
48 |
component_dir.write_settings(""" |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
49 |
ISABELLE_JSVG_HOME="$COMPONENT" |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
50 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
51 |
classpath "$ISABELLE_JSVG_HOME/lib/""" + download_name + """.jar" |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
52 |
""") |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
53 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
54 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
55 |
/* jar */ |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
56 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
57 |
val jar = component_dir.lib + Path.basic(download_name).jar |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
58 |
Isabelle_System.make_directory(jar.dir) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
59 |
Isabelle_System.download_file(download_url, jar, progress = progress) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
60 |
} |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
61 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
62 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
63 |
/* Isabelle tool wrapper */ |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
64 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
65 |
val isabelle_tool = |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
66 |
Isabelle_Tool("component_jsvg", "build Isabelle jsvg component from official download", |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
67 |
Scala_Project.here, |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
68 |
{ args => |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
69 |
var target_dir = Path.current |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
70 |
var download_url = default_download_url |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
71 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
72 |
val getopts = Getopts(""" |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
73 |
Usage: isabelle component_jsvg [OPTIONS] DOWNLOAD |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
74 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
75 |
Options are: |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
76 |
-D DIR target directory (default ".") |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
77 |
-U URL download URL |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
78 |
(default: """" + default_download_url + """") |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
79 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
80 |
Build jsvg component from the specified download URL (JAR). |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
81 |
""", |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
82 |
"D:" -> (arg => target_dir = Path.explode(arg)), |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
83 |
"U:" -> (arg => download_url = arg)) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
84 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
85 |
val more_args = getopts(args) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
86 |
if (more_args.nonEmpty) getopts.usage() |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
87 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
88 |
val progress = new Console_Progress() |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
89 |
|
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
90 |
build_jsvg(download_url = download_url, progress = progress, target_dir = target_dir) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
91 |
}) |
553aa1dd0feb
support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);
wenzelm
parents:
diff
changeset
|
92 |
} |