--- a/Admin/components/components.sha1 Fri Jul 02 15:54:31 2021 +0100
+++ b/Admin/components/components.sha1 Fri Jul 02 15:54:41 2021 +0100
@@ -121,6 +121,7 @@
b166b4bd583b6442a5d75eab06f7adbb66919d6d isabelle_fonts-20210319.tar.gz
9467ad54a9ac10a6e7e8db5458d8d2a5516eba96 isabelle_fonts-20210321.tar.gz
1f7a0b9829ecac6552b21e995ad0f0ac168634f3 isabelle_fonts-20210322.tar.gz
+916adccd2f40c55116b68b92ce1eccb24d4dd9a2 isabelle_setup-20210630.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -346,6 +347,7 @@
a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
+0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
--- a/Admin/components/main Fri Jul 02 15:54:31 2021 +0100
+++ b/Admin/components/main Fri Jul 02 15:54:41 2021 +0100
@@ -8,6 +8,7 @@
flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
+isabelle_setup-20210630
jdk-15.0.2+7
jedit_build-20210510-1
jfreechart-1.5.1
@@ -17,7 +18,7 @@
opam-2.0.7
polyml-5.8.2
postgresql-42.2.18
-scala-2.13.5
+scala-2.13.6
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.34.0
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/build_setup Fri Jul 02 15:54:41 2021 +0100
@@ -0,0 +1,83 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: build component for Isabelle/Java setup tool
+
+## sources
+
+declare -a SOURCES=(
+ "Environment.java"
+ "Setup.java"
+)
+
+
+## usage
+
+PRG=$(basename "$0")
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] COMPONENT_DIR"
+ echo
+ echo " Build component for Isabelle/Java setup tool."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+[ "$#" -ge 1 ] && { COMPONENT_DIR="$1"; shift; }
+[ "$#" -ne 0 -o -z "$COMPONENT_DIR" ] && usage
+
+
+
+## main
+
+[ -d "$COMPONENT_DIR" ] && fail "Directory already exists: \"$COMPONENT_DIR\""
+
+
+# build jar
+
+TARGET_DIR="$COMPONENT_DIR/lib"
+mkdir -p "$TARGET_DIR/isabelle/setup"
+
+declare -a ARGS=("-Xlint:unchecked")
+for SRC in "${SOURCES[@]}"
+do
+ ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/src/isabelle/setup/$SRC")"
+done
+
+isabelle_jdk javac -d "$TARGET_DIR" "${ARGS[@]}" || \
+ fail "Failed to compile sources"
+
+isabelle_jdk jar -c -f "$(platform_path "$TARGET_DIR/isabelle_setup.jar")" \
+ -e "isabelle.setup.Setup" -C "$TARGET_DIR" isabelle || fail "Failed to produce jar"
+
+rm -rf "$TARGET_DIR/isabelle"
+
+
+# etc/settings
+
+mkdir -p "$COMPONENT_DIR/etc"
+cat > "$COMPONENT_DIR/etc/settings" <<EOF
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_SETUP_JAR="\$COMPONENT/lib/isabelle_setup.jar"
+classpath "\$ISABELLE_SETUP_JAR"
+EOF
+
+
+# README
+
+cat > "$COMPONENT_DIR/README" <<EOF
+Isabelle setup in pure Java, see also \$ISABELLE_HOME/src/Tools/Setup/.
+EOF
--- a/src/Pure/Admin/build_release.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/Admin/build_release.scala Fri Jul 02 15:54:41 2021 +0100
@@ -861,7 +861,7 @@
var rev = ""
val getopts = Getopts("""
-Usage: Admin/build_release [OPTIONS] BASE_DIR
+Usage: Admin/build_release [OPTIONS]
Options are:
-A REV corresponding AFP changeset id
--- a/src/Pure/GUI/gui.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/GUI/gui.scala Fri Jul 02 15:54:41 2021 +0100
@@ -6,6 +6,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point,
Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit}
import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
@@ -299,7 +300,7 @@
font.getLineMetrics("", new FontRenderContext(null, false, false))
def transform_font(font: Font, transform: AffineTransform): Font =
- font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
+ font.deriveFont(JMap.of(TextAttribute.TRANSFORM, new TransformAttribute(transform)))
def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
--- a/src/Pure/General/file.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/General/file.scala Fri Jul 02 15:54:41 2021 +0100
@@ -15,13 +15,11 @@
import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
-import java.util.regex.Pattern
import java.util.EnumSet
import org.tukaani.xz.{XZInputStream, XZOutputStream}
import scala.collection.mutable
-import scala.util.matching.Regex
object File
@@ -31,20 +29,7 @@
def standard_path(path: Path): String = path.expand.implode
def standard_path(platform_path: String): String =
- if (Platform.is_windows) {
- val Platform_Root = new Regex("(?i)" +
- Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
- val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
-
- platform_path.replace('/', '\\') match {
- case Platform_Root(rest) => "/" + rest.replace('\\', '/')
- case Drive(letter, rest) =>
- "/cygdrive/" + Word.lowercase(letter) +
- (if (rest == "") "" else "/" + rest.replace('\\', '/'))
- case path => path.replace('\\', '/')
- }
- }
- else platform_path
+ isabelle.setup.Environment.standard_path(Isabelle_System.cygwin_root(), platform_path)
def standard_path(file: JFile): String = standard_path(file.getPath)
@@ -60,36 +45,8 @@
/* platform path (Windows or Posix) */
- private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
- private val Named_Root = new Regex("//+([^/]*)(.*)")
-
def platform_path(standard_path: String): String =
- if (Platform.is_windows) {
- val result_path = new StringBuilder
- val rest =
- standard_path match {
- case Cygdrive(drive, rest) =>
- result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
- rest
- case Named_Root(root, rest) =>
- result_path ++= JFile.separator
- result_path ++= JFile.separator
- result_path ++= root
- rest
- case path if path.startsWith("/") =>
- result_path ++= Isabelle_System.cygwin_root()
- path
- case path => path
- }
- for (p <- space_explode('/', rest) if p != "") {
- val len = result_path.length
- if (len > 0 && result_path(len - 1) != JFile.separatorChar)
- result_path += JFile.separatorChar
- result_path ++= p
- }
- result_path.toString
- }
- else standard_path
+ isabelle.setup.Environment.platform_path(Isabelle_System.cygwin_root(), standard_path)
def platform_path(path: Path): String = platform_path(standard_path(path))
def platform_file(path: Path): JFile = new JFile(platform_path(path))
--- a/src/Pure/General/file_watcher.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/General/file_watcher.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{List => JList}
import java.io.{File => JFile}
import java.nio.file.FileSystems
import java.nio.file.{WatchKey, WatchEvent, Path => JPath}
@@ -102,7 +103,7 @@
st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match {
case Some(dir) =>
val events: Iterable[WatchEvent[JPath]] =
- key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala
+ key.pollEvents.asInstanceOf[JList[WatchEvent[JPath]]].asScala
val remove = if (key.reset) None else Some(dir)
val changed =
events.iterator.foldLeft(Set.empty[JFile]) {
--- a/src/Pure/General/path.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/General/path.scala Fri Jul 02 15:54:41 2021 +0100
@@ -8,6 +8,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile}
import scala.util.matching.Regex
@@ -256,7 +257,7 @@
/* expand */
- def expand_env(env: Map[String, String]): Path =
+ def expand_env(env: JMap[String, String]): Path =
{
def eval(elem: Path.Elem): List[Path.Elem] =
elem match {
--- a/src/Pure/General/ssh.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/General/ssh.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{InputStream, OutputStream, ByteArrayOutputStream}
import scala.collection.mutable
@@ -349,10 +350,10 @@
override def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
- val settings: Map[String, String] =
+ val settings: JMap[String, String] =
{
val home = sftp.getHome
- Map("HOME" -> home, "USER_HOME" -> home)
+ JMap.of("HOME", home, "USER_HOME", home)
}
override def expand_path(path: Path): Path = path.expand_env(settings)
def remote_path(path: Path): String = expand_path(path).implode
--- a/src/Pure/ML/ml_process.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/ML/ml_process.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap, HashMap}
import java.io.{File => JFile}
@@ -22,7 +23,7 @@
args: List[String] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
+ env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
session_base: Option[Sessions.Base] = None): Bash.Process =
@@ -70,11 +71,11 @@
if (modes.isEmpty) Nil
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
+
// options
val isabelle_process_options = Isabelle_System.tmp_file("options")
Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
- val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
// session base
@@ -99,11 +100,6 @@
// ISABELLE_TMP
val isabelle_tmp = Isabelle_System.tmp_dir("process")
- val env_tmp =
- Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp),
- "POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath)
-
- val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
val ml_runtime_options =
{
@@ -123,11 +119,17 @@
(eval_init ::: eval_modes ::: eval_options ::: eval_init_session).flatMap(List("--eval", _)) :::
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
+ val bash_env = new HashMap(env)
+ bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options))
+ bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
+ bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
+ bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(","))
+
Bash.process(
options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
Bash.strings(bash_args),
cwd = cwd,
- env = env ++ env_options ++ env_tmp ++ env_functions,
+ env = bash_env,
redirect = redirect,
cleanup = () =>
{
--- a/src/Pure/ROOT.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/ROOT.scala Fri Jul 02 15:54:41 2021 +0100
@@ -21,3 +21,4 @@
val proper_string = Library.proper_string _
def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
}
+
--- a/src/Pure/System/bash.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/System/bash.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,9 +7,8 @@
package isabelle
-import java.io.{File => JFile, BufferedReader, InputStreamReader,
- BufferedWriter, OutputStreamWriter}
-
+import java.util.{LinkedList, List => JList, Map => JMap}
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile}
import scala.annotation.tailrec
import scala.jdk.OptionConverters._
@@ -48,9 +47,24 @@
type Watchdog = (Time, Process => Boolean)
+ def process_signal(group_pid: String, signal: String = "0"): Boolean =
+ {
+ val cmd = new LinkedList[String]
+ if (Platform.is_windows) {
+ cmd.add(Isabelle_System.cygwin_root() + "\\bin\\bash.exe")
+ }
+ else {
+ cmd.add("/usr/bin/env")
+ cmd.add("bash")
+ }
+ cmd.add("-c")
+ cmd.add("kill -" + signal + " -" + group_pid)
+ isabelle.setup.Environment.exec_process(cmd, null, null, false).ok
+ }
+
def process(script: String,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
+ env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => ()): Process =
new Process(script, cwd, env, redirect, cleanup)
@@ -58,7 +72,7 @@
class Process private[Bash](
script: String,
cwd: JFile,
- env: Map[String, String],
+ env: JMap[String, String],
redirect: Boolean,
cleanup: () => Unit)
{
@@ -80,10 +94,10 @@
File.write(script_file, winpid_script)
private val proc =
- Isabelle_System.process(
- List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
+ isabelle.setup.Environment.process_builder(
+ JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
File.standard_path(timing_file), "bash", File.standard_path(script_file)),
- cwd = cwd, env = env, redirect = redirect)
+ cwd, env, redirect).start()
// channels
@@ -119,8 +133,8 @@
{
count <= 0 ||
{
- Isabelle_System.process_signal(group_pid, signal = s)
- val running = root_process_alive() || Isabelle_System.process_signal(group_pid)
+ process_signal(group_pid, signal = s)
+ val running = root_process_alive() || process_signal(group_pid)
if (running) {
Time.seconds(0.1).sleep()
signal(s, count - 1)
@@ -138,7 +152,7 @@
def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
{
- Isabelle_System.process_signal(group_pid, "INT")
+ process_signal(group_pid, "INT")
}
--- a/src/Pure/System/cygwin.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/System/cygwin.scala Fri Jul 02 15:54:41 2021 +0100
@@ -15,54 +15,4 @@
object Cygwin
{
- /* init (e.g. after extraction via 7zip) */
-
- def init(isabelle_root: String, cygwin_root: String): Unit =
- {
- require(Platform.is_windows, "Windows platform expected")
-
- def exec(cmdline: String*): Unit =
- {
- val cwd = new JFile(isabelle_root)
- val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
- val proc = Isabelle_System.process(cmdline.toList, cwd = cwd, env = env, redirect = true)
- val (output, rc) = Isabelle_System.process_output(proc)
- if (rc != 0) error(output)
- }
-
- val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
- val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
-
- if (uninitialized) {
- val symlinks =
- {
- val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
- Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
- }
- @tailrec def recover_symlinks(list: List[String]): Unit =
- {
- list match {
- case Nil | List("") =>
- case target :: content :: rest =>
- link(content, new JFile(isabelle_root, target))
- recover_symlinks(rest)
- case _ => error("Unbalanced symlinks list")
- }
- }
- recover_symlinks(symlinks)
-
- exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
- exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
- }
- }
-
- def link(content: String, target: JFile): Unit =
- {
- val target_path = target.toPath
-
- using(Files.newBufferedWriter(target_path, UTF8.charset))(
- _.write("!<symlink>" + content + "\u0000"))
-
- Files.setAttribute(target_path, "dos:system", true)
- }
}
--- a/src/Pure/System/isabelle_charset.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/System/isabelle_charset.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{List => JList}
import java.nio.Buffer
import java.nio.{ByteBuffer, CharBuffer}
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
@@ -45,6 +46,6 @@
{
// FIXME inactive
// Iterator(Isabelle_Charset.charset)
- java.util.List.of[Charset]().listIterator()
+ JList.of[Charset]().listIterator()
}
}
--- a/src/Pure/System/isabelle_process.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/System/isabelle_process.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile}
@@ -23,7 +24,7 @@
eval_main: String = "",
modes: List[String] = Nil,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings()): Isabelle_Process =
+ env: JMap[String, String] = Isabelle_System.settings()): Isabelle_Process =
{
val channel = System_Channel()
val process =
--- a/src/Pure/System/isabelle_system.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Jul 02 15:54:41 2021 +0100
@@ -1,63 +1,41 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
-Fundamental Isabelle system environment: quasi-static module with
-optional init operation.
+Miscellaneous Isabelle system operations.
*/
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile, IOException}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
-import scala.jdk.CollectionConverters._
-
object Isabelle_System
{
- /** bootstrap information **/
+ /* settings */
- def jdk_home(): String =
- {
- val java_home = System.getProperty("java.home", "")
- val home = new JFile(java_home)
- val parent = home.getParent
- if (home.getName == "jre" && parent != null &&
- (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
- else java_home
- }
+ def settings(): JMap[String, String] = isabelle.setup.Environment.settings()
- def bootstrap_directory(
- preference: String, envar: String, property: String, description: String): String =
- {
- val value =
- proper_string(preference) orElse // explicit argument
- proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool
- proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process
- error("Unknown " + description + " directory")
+ def getenv(name: String, env: JMap[String, String] = settings()): String =
+ Option(env.get(name)).getOrElse("")
- if ((new JFile(value)).isDirectory) value
- else error("Bad " + description + " directory " + quote(value))
- }
+ def getenv_strict(name: String, env: JMap[String, String] = settings()): String =
+ proper_string(getenv(name, env)) getOrElse
+ error("Undefined Isabelle environment variable: " + quote(name))
+
+ def cygwin_root(): String = getenv("CYGWIN_ROOT")
-
- /** implicit settings environment **/
+ /* services */
abstract class Service
- @volatile private var _settings: Option[Map[String, String]] = None
@volatile private var _services: Option[List[Class[Service]]] = None
- def settings(): Map[String, String] =
- {
- if (_settings.isEmpty) init() // unsynchronized check
- _settings.get
- }
-
def services(): List[Class[Service]] =
{
if (_services.isEmpty) init() // unsynchronized check
@@ -68,110 +46,32 @@
for { c1 <- services() if Library.is_subclass(c1, c) }
yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
- def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
- {
- if (_settings.isEmpty || _services.isEmpty) {
- val isabelle_root1 =
- bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
- val cygwin_root1 =
- if (Platform.is_windows)
- bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
- else ""
-
- if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
-
- def set_cygwin_root(): Unit =
- {
- if (Platform.is_windows)
- _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
- }
-
- set_cygwin_root()
-
- def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
- if (env.isDefinedAt(entry._1) || entry._2 == "") env
- else env + entry
-
- val env =
- {
- val temp_windows =
- {
- val temp = if (Platform.is_windows) System.getenv("TEMP") else null
- if (temp != null && temp.contains('\\')) temp else ""
- }
- val user_home = System.getProperty("user.home", "")
- val isabelle_app = System.getProperty("isabelle.app", "")
-
- default(
- default(
- default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
- "TEMP_WINDOWS" -> temp_windows),
- "HOME" -> user_home),
- "ISABELLE_APP" -> "true")
- }
+ /* init settings + services */
- val settings =
- {
- val dump = JFile.createTempFile("settings", null)
- dump.deleteOnExit
- try {
- val cmd1 =
- if (Platform.is_windows)
- List(cygwin_root1 + "\\bin\\bash", "-l",
- File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
- else
- List(isabelle_root1 + "/bin/isabelle")
- val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
-
- val (output, rc) = process_output(process(cmd, env = env, redirect = true))
- if (rc != 0) error(output)
-
- val entries =
- space_explode('\u0000', File.read(dump)).flatMap(
- {
- case Properties.Eq(a, b) => Some(a -> b)
- case s => if (s.isEmpty || s.startsWith("=")) None else Some(s -> "")
- }).toMap
- entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
- }
- finally { dump.delete }
+ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit =
+ {
+ isabelle.setup.Environment.init(isabelle_root, cygwin_root)
+ synchronized {
+ if (_services.isEmpty) {
+ val variable = "ISABELLE_SCALA_SERVICES"
+ val services =
+ for (name <- space_explode(':', getenv_strict(variable)))
+ yield {
+ def err(msg: String): Nothing =
+ error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+ try { Class.forName(name).asInstanceOf[Class[Service]] }
+ catch {
+ case _: ClassNotFoundException => err("Class not found")
+ case exn: Throwable => err(Exn.message(exn))
+ }
+ }
+ _services = Some(services)
}
- _settings = Some(settings)
- set_cygwin_root()
-
- val variable = "ISABELLE_SCALA_SERVICES"
- val services =
- for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
- yield {
- def err(msg: String): Nothing =
- error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
- try { Class.forName(name).asInstanceOf[Class[Service]] }
- catch {
- case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
- }
- }
- _services = Some(services)
}
}
- /* getenv -- dynamic process environment */
-
- private def getenv_error(name: String): Nothing =
- error("Undefined Isabelle environment variable: " + quote(name))
-
- def getenv(name: String, env: Map[String, String] = settings()): String =
- env.getOrElse(name, "")
-
- def getenv_strict(name: String, env: Map[String, String] = settings()): String =
- proper_string(getenv(name, env)) getOrElse
- error("Undefined Isabelle environment variable: " + quote(name))
-
- def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
-
-
/* getetc -- static distribution parameters */
def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
@@ -352,12 +252,13 @@
if (force) target.delete
+ def cygwin_link(): Unit =
+ isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
+
try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
catch {
- case _: UnsupportedOperationException if Platform.is_windows =>
- Cygwin.link(File.standard_path(src), target)
- case _: FileSystemException if Platform.is_windows =>
- Cygwin.link(File.standard_path(src), target)
+ case _: UnsupportedOperationException if Platform.is_windows => cygwin_link()
+ case _: FileSystemException if Platform.is_windows => cygwin_link()
}
}
@@ -458,59 +359,11 @@
/** external processes **/
- /* raw process */
-
- def process(command_line: List[String],
- cwd: JFile = null,
- env: Map[String, String] = settings(),
- redirect: Boolean = false): Process =
- {
- val proc = new ProcessBuilder
-
- // fragile on Windows:
- // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
- proc.command(command_line.asJava)
-
- if (cwd != null) proc.directory(cwd)
- if (env != null) {
- proc.environment.clear()
- for ((x, y) <- env) proc.environment.put(x, y)
- }
- proc.redirectErrorStream(redirect)
- proc.start
- }
-
- def process_output(proc: Process): (String, Int) =
- {
- proc.getOutputStream.close()
-
- val output = File.read_stream(proc.getInputStream)
- val rc =
- try { proc.waitFor }
- finally {
- proc.getInputStream.close()
- proc.getErrorStream.close()
- proc.destroy()
- Exn.Interrupt.dispose()
- }
- (output, rc)
- }
-
- def process_signal(group_pid: String, signal: String = "0"): Boolean =
- {
- val bash =
- if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
- else List("/usr/bin/env", "bash")
- val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
- rc == 0
- }
-
-
/* GNU bash */
def bash(script: String,
cwd: JFile = null,
- env: Map[String, String] = settings(),
+ env: JMap[String, String] = settings(),
redirect: Boolean = false,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
--- a/src/Pure/System/platform.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/System/platform.scala Fri Jul 02 15:54:41 2021 +0100
@@ -11,9 +11,9 @@
{
/* platform family */
+ val is_windows: Boolean = isabelle.setup.Environment.is_windows()
val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
- val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
val is_unix: Boolean = is_linux || is_macos
def is_arm: Boolean = cpu_arch.startsWith("arm")
--- a/src/Pure/System/progress.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/System/progress.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,6 +7,7 @@
package isabelle
+import java.util.{Map => JMap}
import java.io.{File => JFile}
@@ -50,7 +51,7 @@
def bash(script: String,
cwd: JFile = null,
- env: Map[String, String] = Isabelle_System.settings(),
+ env: JMap[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
echo: Boolean = false,
watchdog: Time = Time.zero,
--- a/src/Pure/Tools/build_job.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Jul 02 15:54:41 2021 +0100
@@ -7,6 +7,8 @@
package isabelle
+import java.util.HashMap
+
import scala.collection.mutable
@@ -217,9 +219,8 @@
val base = deps(parent)
val result_base = deps(session_name)
- val env =
- Isabelle_System.settings() +
- ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
+ val env = new HashMap(Isabelle_System.settings())
+ env.put("ISABELLE_ML_DEBUGGER", options.bool("ML_debugger").toString)
val is_pure = Sessions.is_pure(session_name)
--- a/src/Pure/Tools/scala_project.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala Fri Jul 02 15:54:41 2021 +0100
@@ -111,12 +111,18 @@
if (project_dir.is_file || project_dir.is_dir)
error("Project directory already exists: " + project_dir)
- val src_dir = project_dir + Path.explode("src/main/scala")
val java_src_dir = project_dir + Path.explode("src/main/java")
val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)
+ if (symlinks) {
+ Isabelle_System.symlink(Path.explode("~~/src/Tools/Setup/src/isabelle"), java_src_dir)
+ }
+ else {
+ Isabelle_System.copy_dir(Path.explode("~~/src/Tools/Setup/src"), java_src_dir)
+ }
+
val files = isabelle_files
isabelle_scala_files
--- a/src/Pure/Tools/spell_checker.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/Tools/spell_checker.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,7 @@
import java.lang.Class
+import java.util.{List => JList}
import scala.collection.mutable
import scala.annotation.tailrec
@@ -223,7 +224,7 @@
{
val res =
Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
- invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+ invoke(dict, word).asInstanceOf[JList[AnyRef]].toArray.toList.map(_.toString)
if (res.isEmpty) None else Some(res)
}
--- a/src/Pure/build-jars Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Pure/build-jars Fri Jul 02 15:54:41 2021 +0100
@@ -133,7 +133,6 @@
src/Pure/System/bash.scala
src/Pure/System/command_line.scala
src/Pure/System/components.scala
- src/Pure/System/cygwin.scala
src/Pure/System/executable.scala
src/Pure/System/getopts.scala
src/Pure/System/isabelle_charset.scala
--- a/src/Tools/Graphview/metrics.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Tools/Graphview/metrics.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.HashMap
import java.awt.{Font, RenderingHints}
import java.awt.font.FontRenderContext
import java.awt.geom.Rectangle2D
@@ -18,7 +19,7 @@
{
val rendering_hints: RenderingHints =
{
- val hints = new java.util.HashMap[RenderingHints.Key, AnyRef]
+ val hints = new HashMap[RenderingHints.Key, AnyRef]
hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON)
hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON)
new RenderingHints(hints)
--- a/src/Tools/Setup/.idea/.name Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-isabelle-setup
\ No newline at end of file
--- a/src/Tools/Setup/.idea/artifacts/Setup_jar.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-<component name="ArtifactManager">
- <artifact type="jar" name="Setup:jar">
- <output-path>$PROJECT_DIR$/out/artifacts/</output-path>
- <root id="archive" name="Setup.jar">
- <element id="module-output" name="Setup" />
- </root>
- </artifact>
-</component>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/codeStyles/Project.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
- <code_scheme name="Project" version="173">
- <option name="LINE_SEPARATOR" value=" " />
- <option name="SOFT_MARGINS" value="100" />
- <codeStyleSettings language="Scala">
- <option name="ALIGN_MULTILINE_PARAMETERS" value="false" />
- </codeStyleSettings>
- </code_scheme>
-</component>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/codeStyles/codeStyleConfig.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-<component name="ProjectCodeStyleConfiguration">
- <state>
- <option name="PREFERRED_PROJECT_CODE_STYLE" value="Default" />
- </state>
-</component>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/misc.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ProjectRootManager" version="2" languageLevel="JDK_11" default="true" project-jdk-name="11" project-jdk-type="JavaSDK">
- <output url="file://$PROJECT_DIR$/out" />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/modules.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ProjectModuleManager">
- <modules>
- <module fileurl="file://$PROJECT_DIR$/Setup.iml" filepath="$PROJECT_DIR$/Setup.iml" />
- </modules>
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/sbt.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ScalaSbtSettings">
- <option name="customVMPath" />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/vcs.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="VcsDirectoryMappings">
- <mapping directory="$PROJECT_DIR$/../../.." vcs="hg4idea" />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/.idea/workspace.xml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<project version="4">
- <component name="ArtifactsWorkspaceSettings">
- <artifacts-to-build>
- <artifact name="Setup:jar" />
- </artifacts-to-build>
- </component>
- <component name="AutoImportSettings">
- <option name="autoReloadType" value="SELECTIVE" />
- </component>
- <component name="ChangeListManager">
- <list default="true" id="a00f79eb-e202-4706-95b3-a972b05b3ddb" name="Default Changelist" comment="" />
- <option name="SHOW_DIALOG" value="false" />
- <option name="HIGHLIGHT_CONFLICTS" value="true" />
- <option name="HIGHLIGHT_NON_ACTIVE_CHANGELIST" value="false" />
- <option name="LAST_RESOLUTION" value="IGNORE" />
- </component>
- <component name="CodeStyleSettingsInfer">
- <option name="done" value="true" />
- </component>
- <component name="FileTemplateManagerImpl">
- <option name="RECENT_TEMPLATES">
- <list>
- <option value="Class" />
- </list>
- </option>
- </component>
- <component name="ProjectCodeStyleSettingsMigration">
- <option name="version" value="1" />
- </component>
- <component name="ProjectId" id="1sP6lEsakYWhAQI9WzuHpAcovaN" />
- <component name="ProjectLevelVcsManager" settingsEditedManually="true" />
- <component name="ProjectViewState">
- <option name="hideEmptyMiddlePackages" value="true" />
- <option name="showLibraryContents" value="true" />
- </component>
- <component name="PropertiesComponent">
- <property name="RunOnceActivity.OpenProjectViewOnStart" value="true" />
- <property name="RunOnceActivity.ShowReadmeOnStart" value="true" />
- <property name="project.structure.last.edited" value="Artifacts" />
- <property name="project.structure.proportion" value="0.15" />
- <property name="project.structure.side.proportion" value="0.18055555" />
- </component>
- <component name="SpellCheckerSettings" RuntimeDictionaries="0" Folders="0" CustomDictionaries="0" DefaultDictionary="application-level" UseSingleDictionary="true" transferred="true" />
- <component name="TaskManager">
- <task active="true" id="Default" summary="Default task">
- <changelist id="a00f79eb-e202-4706-95b3-a972b05b3ddb" name="Default Changelist" comment="" />
- <created>1620762028428</created>
- <option name="number" value="Default" />
- <option name="presentableId" value="Default" />
- <updated>1620762028428</updated>
- </task>
- <servers />
- </component>
- <component name="hg4idea.settings">
- <option name="CHECK_INCOMING_OUTGOING" value="true" />
- <option name="RECENT_HG_ROOT_PATH" value="$PROJECT_DIR$/../../.." />
- </component>
-</project>
\ No newline at end of file
--- a/src/Tools/Setup/Setup.iml Fri Jul 02 15:54:31 2021 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<module type="JAVA_MODULE" version="4">
- <component name="NewModuleRootManager" inherit-compiler-output="true">
- <exclude-output />
- <content url="file://$MODULE_DIR$">
- <sourceFolder url="file://$MODULE_DIR$/src" isTestSource="false" />
- </content>
- <orderEntry type="inheritedJdk" />
- <orderEntry type="sourceFolder" forTests="false" />
- </component>
-</module>
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/isabelle/setup/Environment.java Fri Jul 02 15:54:41 2021 +0100
@@ -0,0 +1,336 @@
+/* Title: Pure/System/isabelle_env.scala
+ Author: Makarius
+
+Fundamental Isabelle system environment: quasi-static module with
+optional init operation.
+*/
+
+package isabelle.setup;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.function.BiFunction;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+
+public class Environment
+{
+ /** Support for Cygwin as POSIX emulation on Windows **/
+
+ public static Boolean is_windows()
+ {
+ return System.getProperty("os.name", "").startsWith("Windows");
+ }
+
+ public static String quote(String s)
+ {
+ return "\"" + s + "\"";
+ }
+
+
+
+ /* system path representations */
+
+ private static String slashes(String s) { return s.replace('\\', '/'); }
+
+ public static String standard_path(String cygwin_root, String platform_path)
+ {
+ if (is_windows()) {
+ String backslashes = platform_path.replace('/', '\\');
+
+ Pattern root_pattern =
+ Pattern.compile("(?i)" + Pattern.quote(cygwin_root) + "(?:\\\\+|\\z)(.*)");
+ Matcher root_matcher = root_pattern.matcher(backslashes);
+
+ Pattern drive_pattern = Pattern.compile("([a-zA-Z]):\\\\*(.*)");
+ Matcher drive_matcher = drive_pattern.matcher(backslashes);
+
+ if (root_matcher.matches()) {
+ String rest = root_matcher.group(1);
+ return "/" + slashes(rest);
+ }
+ else if (drive_matcher.matches()) {
+ String letter = drive_matcher.group(1).toLowerCase(Locale.ROOT);
+ String rest = drive_matcher.group(2);
+ return "/cygdrive/" + letter + (rest.isEmpty() ? "" : "/" + slashes(rest));
+ }
+ else { return slashes(backslashes); }
+ }
+ else { return platform_path; }
+ }
+
+ public static String platform_path(String cygwin_root, String standard_path)
+ {
+ if (is_windows()) {
+ StringBuilder result_path = new StringBuilder();
+
+ Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)");
+ Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path);
+
+ Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)");
+ Matcher named_root_matcher = named_root_pattern.matcher(standard_path);
+
+ String rest;
+ if (cygdrive_matcher.matches()) {
+ String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT);
+ rest = cygdrive_matcher.group(2);
+ result_path.append(drive);
+ result_path.append(':');
+ result_path.append(File.separatorChar);
+ }
+ else if (named_root_matcher.matches()) {
+ String root = named_root_matcher.group(1);
+ rest = named_root_matcher.group(2);
+ result_path.append(File.separatorChar);
+ result_path.append(File.separatorChar);
+ result_path.append(root);
+ }
+ else {
+ if (standard_path.startsWith("/")) { result_path.append(cygwin_root); }
+ rest = standard_path;
+ }
+
+ for (String p : rest.split("/", -1)) {
+ if (!p.isEmpty()) {
+ int len = result_path.length();
+ if (len > 0 && result_path.charAt(len - 1) != File.separatorChar) {
+ result_path.append(File.separatorChar);
+ }
+ result_path.append(p);
+ }
+ }
+
+ return result_path.toString();
+ }
+ else { return standard_path; }
+ }
+
+
+ /* raw process */
+
+ public static ProcessBuilder process_builder(
+ List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
+ {
+ ProcessBuilder builder = new ProcessBuilder();
+
+ // fragile on Windows:
+ // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
+ builder.command(cmd);
+
+ if (cwd != null) builder.directory(cwd);
+ if (env != null) {
+ builder.environment().clear();
+ builder.environment().putAll(env);
+ }
+ builder.redirectErrorStream(redirect);
+
+ return builder;
+ }
+
+ public static class Exec_Result
+ {
+ private final int _rc;
+ private final String _out;
+ private final String _err;
+
+ Exec_Result(int rc, String out, String err)
+ {
+ _rc = rc;
+ _out = out;
+ _err = err;
+ }
+
+ public int rc() { return _rc; }
+ public boolean ok() { return _rc == 0; }
+ public String out() { return _out; }
+ public String err() { return _err; }
+ }
+
+ public static Exec_Result exec_process(
+ List<String> command_line,
+ File cwd,
+ Map<String,String> env,
+ boolean redirect) throws IOException, InterruptedException
+ {
+ Path out_file = Files.createTempFile(null, null);
+ Path err_file = Files.createTempFile(null, null);
+ Exec_Result res;
+ try {
+ ProcessBuilder builder = process_builder(command_line, cwd, env, redirect);
+ builder.redirectOutput(out_file.toFile());
+ builder.redirectError(err_file.toFile());
+
+ Process proc = builder.start();
+ proc.getOutputStream().close();
+ try { proc.waitFor(); }
+ finally {
+ proc.getInputStream().close();
+ proc.getErrorStream().close();
+ proc.destroy();
+ Thread.interrupted();
+ }
+
+ int rc = proc.exitValue();
+ String out = Files.readString(out_file);
+ String err = Files.readString(err_file);
+ res = new Exec_Result(rc, out, err);
+ }
+ finally {
+ Files.deleteIfExists(out_file);
+ Files.deleteIfExists(err_file);
+ }
+ return res;
+ }
+
+
+ /* init (e.g. after extraction via 7zip) */
+
+ private static String bootstrap_directory(
+ String preference, String variable, String property, String description)
+ {
+ String a = preference; // explicit argument
+ String b = System.getenv(variable); // e.g. inherited from running isabelle tool
+ String c = System.getProperty(property); // e.g. via JVM application boot process
+ String dir;
+
+ if (a != null && !a.isEmpty()) { dir = a; }
+ else if (b != null && !b.isEmpty()) { dir = b; }
+ else if (c != null && !c.isEmpty()) { dir = c; }
+ else { throw new RuntimeException("Unknown " + description + " directory"); }
+
+ if ((new File(dir)).isDirectory()) { return dir; }
+ else { throw new RuntimeException("Bad " + description + " directory " + quote(dir)); }
+ }
+
+ private static void cygwin_exec(String isabelle_root, List<String> cmd)
+ throws IOException, InterruptedException
+ {
+ File cwd = new File(isabelle_root);
+ Map<String,String> env = new HashMap<String,String>(System.getenv());
+ env.put("CYGWIN", "nodosfilewarning");
+ Exec_Result res = exec_process(cmd, cwd, env, true);
+ if (!res.ok()) throw new RuntimeException(res.out());
+ }
+
+ public static void cygwin_link(String content, File target) throws IOException
+ {
+ Path target_path = target.toPath();
+ Files.writeString(target_path, "!<symlink>" + content + "\u0000");
+ Files.setAttribute(target_path, "dos:system", true);
+ }
+
+ public static void cygwin_init(String isabelle_root, String cygwin_root)
+ throws IOException, InterruptedException
+ {
+ if (is_windows()) {
+ File uninitialized_file = new File(cygwin_root, "isabelle\\uninitialized");
+ boolean uninitialized = uninitialized_file.isFile() && uninitialized_file.delete();
+
+ if (uninitialized) {
+ Path symlinks_path = (new File(cygwin_root + "\\isabelle\\symlinks")).toPath();
+ String[] symlinks = Files.readAllLines(symlinks_path).toArray(new String[0]);
+
+ // recover symlinks
+ int i = 0;
+ int m = symlinks.length;
+ int n = (m > 0 && symlinks[m - 1].isEmpty()) ? m - 1 : m;
+ while (i < n) {
+ if (i + 1 < n) {
+ String target = symlinks[i];
+ String content = symlinks[i + 1];
+ cygwin_link(content, new File(isabelle_root, target));
+ i += 2;
+ } else { throw new RuntimeException("Unbalanced symlinks list"); }
+ }
+
+ cygwin_exec(isabelle_root,
+ List.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"));
+ cygwin_exec(isabelle_root,
+ List.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"));
+ }
+ }
+ }
+
+
+ /* implicit settings environment */
+
+ private static volatile Map<String,String> _settings = null;
+
+ public static Map<String,String> settings()
+ throws IOException, InterruptedException
+ {
+ if (_settings == null) { init("", ""); } // unsynchronized check
+ return _settings;
+ }
+
+ public static synchronized void init(String _isabelle_root, String _cygwin_root)
+ throws IOException, InterruptedException
+ {
+ if (_settings == null) {
+ String isabelle_root =
+ bootstrap_directory(_isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root");
+
+ String cygwin_root = "";
+ if (is_windows()) {
+ cygwin_root = bootstrap_directory(_cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root");
+ cygwin_init(isabelle_root, cygwin_root);
+ }
+
+ Map<String,String> env = new HashMap<String,String>(System.getenv());
+
+ BiFunction<String,String,Void> env_default =
+ (String a, String b) -> { if (!b.isEmpty()) env.putIfAbsent(a, b); return null; };
+
+ String temp_windows = is_windows() ? System.getenv("TEMP") : null;
+
+ env_default.apply("CYGWIN_ROOT", cygwin_root);
+ env_default.apply("TEMP_WINDOWS",
+ (temp_windows != null && temp_windows.contains("\\")) ? temp_windows : "");
+ env_default.apply("ISABELLE_JDK_HOME",
+ standard_path(cygwin_root, System.getProperty("java.home", "")));
+ env_default.apply("HOME", System.getProperty("user.home", ""));
+ env_default.apply("ISABELLE_APP", System.getProperty("isabelle.app", ""));
+
+ Map<String,String> settings = new HashMap<String,String>();
+ Path settings_file = Files.createTempFile(null, null);
+ try {
+ List<String> cmd = new LinkedList<String>();
+ if (is_windows()) {
+ cmd.add(cygwin_root + "\\bin\\bash");
+ cmd.add("-l");
+ cmd.add(standard_path(cygwin_root, isabelle_root + "\\bin\\isabelle"));
+ } else {
+ cmd.add(isabelle_root + "/bin/isabelle");
+ }
+ cmd.add("getenv");
+ cmd.add("-d");
+ cmd.add(settings_file.toString());
+
+ Exec_Result res = exec_process(cmd, null, env, true);
+ if (!res.ok()) throw new RuntimeException(res.out());
+
+ for (String s : Files.readString(settings_file).split("\u0000", -1)) {
+ int i = s.indexOf('=');
+ if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
+ else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
+ }
+ }
+ finally { Files.delete(settings_file); }
+
+ if (is_windows()) { settings.put("CYGWIN_ROOT", cygwin_root); }
+
+ settings.put("PATH", settings.get("PATH_JVM"));
+ settings.remove("PATH_JVM");
+
+ _settings = Map.copyOf(settings);
+ }
+ }
+}
--- a/src/Tools/jEdit/src-base/pide_docking_framework.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{List => JList}
import java.awt.event.{ActionListener, ActionEvent}
import javax.swing.{JPopupMenu, JMenuItem}
@@ -42,7 +43,7 @@
}
case panel: PanelWindowContainer =>
- val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray
+ val entries = Untyped.get[JList[AnyRef]](panel, "dockables").toArray
val wins =
(for {
entry <- entries.iterator
--- a/src/Tools/jEdit/src/fold_handling.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Tools/jEdit/src/fold_handling.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import javax.swing.text.Segment
import scala.jdk.CollectionConverters._
@@ -32,7 +34,7 @@
Token_Markup.Line_Context.after(buffer, line).structure.depth max 0
override def getPrecedingFoldLevels(
- buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
+ buffer: JEditBuffer, line: Int, seg: Segment, level: Int): JList[Integer] =
{
val structure = Token_Markup.Line_Context.after(buffer, line).structure
val result =
--- a/src/Tools/jEdit/src/keymap_merge.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Tools/jEdit/src/keymap_merge.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{Properties => JProperties}
import java.awt.{Color, Dimension, BorderLayout}
import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
import javax.swing.table.AbstractTableModel
@@ -64,7 +65,7 @@
/* content wrt. keymap */
- def convert_properties(props: java.util.Properties): List[Shortcut] =
+ def convert_properties(props: JProperties): List[Shortcut] =
if (props == null) Nil
else {
var result = List.empty[Shortcut]
@@ -82,7 +83,7 @@
{
val keymap_shortcuts =
if (keymap == null) Nil
- else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
+ else convert_properties(Untyped.get[JProperties](keymap, "props"))
for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
val conflicts =
--- a/src/Tools/jEdit/src/syntax_style.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,7 @@
import isabelle._
+import java.util.{Map => JMap}
import java.awt.{Font, Color}
import java.awt.font.TextAttribute
import java.awt.geom.AffineTransform
@@ -40,8 +41,7 @@
{
font_style(style, font0 =>
{
- val font1 =
- font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
+ val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
def shift(y: Float): Font =
GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
--- a/src/Tools/jEdit/src/text_structure.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Tools/jEdit/src/text_structure.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -45,7 +47,7 @@
private val keyword_close = Keyword.proof_close
def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
- actions: java.util.List[IndentAction]): Unit =
+ actions: JList[IndentAction]): Unit =
{
Isabelle.buffer_syntax(buffer) match {
case Some(syntax) =>
--- a/src/Tools/jEdit/src/token_markup.scala Fri Jul 02 15:54:31 2021 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Fri Jul 02 15:54:41 2021 +0100
@@ -9,6 +9,8 @@
import isabelle._
+import java.util.{List => JList}
+
import javax.swing.text.Segment
import org.gjt.sp.jedit.{Mode, Buffer}
@@ -314,8 +316,7 @@
super.loadMode(mode, xmh)
Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker)
Isabelle.indent_rule(mode.getName).foreach(indent_rule =>
- Untyped.set[java.util.List[IndentRule]](
- mode, "indentRules", java.util.List.of(indent_rule)))
+ Untyped.set[JList[IndentRule]](mode, "indentRules", JList.of(indent_rule)))
}
}
}