# HG changeset patch
# User wenzelm
# Date 1619382833 -7200
# Node ID 51f7bda1bfa2096bf7a9340ba7a3d81ea89f4e7c
# Parent  5c4a09c4bc9c48f7fd7d6ff825ffa9e906b2a5d0# Parent  51b291ae3e2d625028c6084a70dffcf3fa53c008
merged

diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 Admin/PLATFORMS
--- a/Admin/PLATFORMS	Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/PLATFORMS	Sun Apr 25 22:33:53 2021 +0200
@@ -33,7 +33,7 @@
 
 Official (full support):
 
-  x86_64-linux      Ubuntu 14.04 LTS
+  x86_64-linux      Ubuntu 16.04 LTS
 
   x86_64-darwin     macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2)
                     macOS 10.14 Mojave (mini2 Macmini8,1)
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 Admin/bash_process/bash_process.c
--- a/Admin/bash_process/bash_process.c	Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/bash_process/bash_process.c	Sun Apr 25 22:33:53 2021 +0200
@@ -37,13 +37,12 @@
 {
   /* args */
 
-  if (argc < 3) {
-    fprintf(stderr, "Bad arguments: PID_FILE and TIMING_FILE required\n");
+  if (argc < 2) {
+    fprintf(stderr, "Bad arguments: missing TIMING_FILE\n");
     fflush(stderr);
     exit(1);
   }
-  char *pid_name = argv[1];
-  char *timing_name = argv[2];
+  char *timing_name = argv[1];
 
 
   /* potential fork */
@@ -101,26 +100,16 @@
 
   /* report pid */
 
-  if (strcmp(pid_name, "-") == 0) {
-    fprintf(stdout, "%d\n", getpid());
-    fflush(stdout);
-  }
-  else if (strlen(pid_name) > 0) {
-    FILE *pid_file;
-    pid_file = fopen(pid_name, "w");
-    if (pid_file == NULL) fail("Cannot open pid file");
-    fprintf(pid_file, "%d", getpid());
-    fclose(pid_file);
-  }
+  fprintf(stdout, "%d\n", getpid());
+  fflush(stdout);
 
 
   /* shift command line */
 
   int i;
-  for (i = 3; i < argc; i++) {
-    argv[i - 3] = argv[i];
+  for (i = 2; i < argc; i++) {
+    argv[i - 2] = argv[i];
   }
-  argv[argc - 3] = NULL;
   argv[argc - 2] = NULL;
   argv[argc - 1] = NULL;
 
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 Admin/bash_process/build
--- a/Admin/bash_process/build	Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/bash_process/build	Sun Apr 25 22:33:53 2021 +0200
@@ -36,16 +36,16 @@
 mkdir -p "$TARGET"
 
 case "$TARGET" in
+  arm64-linux)
+    cc -Wall bash_process.c -o "$TARGET/bash_process"
+    ;;
   x86_64-linux | x86_64-darwin)
     cc -Wall -m64 bash_process.c -o "$TARGET/bash_process"
     ;;
-  x86-linux | x86-darwin)
-    cc -Wall -m32 bash_process.c -o "$TARGET/bash_process"
-    ;;
-  x86_64-cygwin | x86-cygwin)
+  x86_64-cygwin)
     cc -Wall bash_process.c -o "$TARGET/bash_process.exe"
     ;;
   *)
-    cc -Wall bash_process.c -o "$TARGET/bash_process"
+    fail "Bad target platform: \"$TARGET\""
     ;;
 esac
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 Admin/bash_process/etc/settings
--- a/Admin/bash_process/etc/settings	Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/bash_process/etc/settings	Sun Apr 25 22:33:53 2021 +0200
@@ -1,3 +1,3 @@
 # -*- shell-script -*- :mode=shellscript:
 
-ISABELLE_BASH_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bash_process"
+ISABELLE_BASH_PROCESS="$COMPONENT/$ISABELLE_PLATFORM64/bash_process"
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/components/components.sha1	Sun Apr 25 22:33:53 2021 +0200
@@ -13,6 +13,8 @@
 97b2491382130a841b3bbaebdcf8720c4d4fb227  bash_process-1.2.2.tar.gz
 5c5b7c18cc1dc2a4d22b997dac196da09eaca868  bash_process-1.2.3-1.tar.gz
 48b01bd9436e243ffcb7297f08b498d0c0875ed9  bash_process-1.2.3.tar.gz
+11815d5f3af0de9022e903ed8702c136591f06fe  bash_process-1.2.4-1.tar.gz
+7ae9ec8aab2d8a811842d9dc67d8bf6c179e11ee  bash_process-1.2.4.tar.gz
 9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
 a65ce644b6094d41e9f991ef851cf05eff5dd0a9  bib2xhtml-20171221.tar.gz
 4085dd6060a32d7e0d2e3f874c463a9964fd409b  bib2xhtml-20190409.tar.gz
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 Admin/components/main
--- a/Admin/components/main	Fri Apr 23 09:50:14 2021 +0000
+++ b/Admin/components/main	Sun Apr 25 22:33:53 2021 +0200
@@ -1,6 +1,6 @@
 #main components for everyday use, without big impact on overall build time
 gnu-utils-20210414
-bash_process-1.2.3-1
+bash_process-1.2.4-1
 bib2xhtml-20190409
 csdp-6.1.1
 cvc4-1.8
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 NEWS
--- a/NEWS	Fri Apr 23 09:50:14 2021 +0000
+++ b/NEWS	Sun Apr 25 22:33:53 2021 +0200
@@ -33,6 +33,10 @@
 \guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
 (which is now also the default in "isabelle mkroot").
 
+* Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
+\guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
+no longer required.
+
 
 *** HOL ***
 
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 lib/Tools/env
--- a/lib/Tools/env	Fri Apr 23 09:50:14 2021 +0000
+++ b/lib/Tools/env	Sun Apr 25 22:33:53 2021 +0200
@@ -25,4 +25,4 @@
 
 [ "$1" = "-?" ] && usage
 
-exec /usr/bin/env "$@"
+/usr/bin/env "$@"
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Fri Apr 23 09:50:14 2021 +0000
+++ b/lib/texinputs/isabellesym.sty	Sun Apr 25 22:33:53 2021 +0200
@@ -234,8 +234,8 @@
 \newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}}
 \newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}}
 \newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}}
-\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
-\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
+\newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}}
+\newcommand{\isasymguillemotright}{\isatext{\guillemotright}}
 \newcommand{\isasymbottom}{\isamath{\bot}}
 \newcommand{\isasymtop}{\isamath{\top}}
 \newcommand{\isasymand}{\isamath{\wedge}}
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Doc/Nitpick/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -2,7 +2,6 @@
 \usepackage[T1]{fontenc}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage[english]{babel}
 \usepackage{color}
 \usepackage{footmisc}
 \usepackage{graphicx}
@@ -32,7 +31,7 @@
 \def\undef{(\lambda x.\; \_)}
 %\def\unr{\textit{others}}
 \def\unr{\ldots}
-\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
+\def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}
 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
 
 \hyphenation{Mini-Sat size-change First-Steps grand-parent nit-pick
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Doc/Sledgehammer/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -2,7 +2,6 @@
 \usepackage[T1]{fontenc}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage[english]{babel}
 \usepackage{color}
 \usepackage{footmisc}
 \usepackage{graphicx}
@@ -40,7 +39,7 @@
 \def\undef{(\lambda x.\; \unk)}
 %\def\unr{\textit{others}}
 \def\unr{\ldots}
-\def\Abs#1{\hbox{\rm{\flqq}}{\,#1\,}\hbox{\rm{\frqq}}}
+\def\Abs#1{\hbox{\rm{\guillemetleft}}{\,#1\,}\hbox{\rm{\guillemetright}}}
 \def\Q{{\smash{\lower.2ex\hbox{$\scriptstyle?$}}}}
 
 \urlstyle{tt}
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Doc/Tutorial/document/root.tex
--- a/src/Doc/Tutorial/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Doc/Tutorial/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -3,7 +3,6 @@
 \usepackage{proof,amsmath,amsfonts,amssymb}
 \usepackage{wasysym,verbatim,graphicx,tutorial,ttbox,comment}
 \usepackage{eurosym}
-\usepackage[english]{babel}
 \usepackage{pdfsetup}   
 %last package!
 
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Bali/document/root.tex
--- a/src/HOL/Bali/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Bali/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -4,7 +4,6 @@
 \usepackage{latexsym}
 \usepackage{graphicx}
 \usepackage{pdfsetup}
-\usepackage[english]{babel}
 \usepackage{ifthen}
 
 \urlstyle{rm}
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Hoare/document/root.tex
--- a/src/HOL/Hoare/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Hoare/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
-\usepackage[english]{babel}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Hoare_Parallel/document/root.tex
--- a/src/HOL/Hoare_Parallel/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Hoare_Parallel/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -1,6 +1,6 @@
 \documentclass[11pt,a4paper]{report}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
-\usepackage[english]{babel}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
 
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Imperative_HOL/document/root.tex
--- a/src/HOL/Imperative_HOL/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Imperative_HOL/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,6 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
 \usepackage{amssymb}
-\usepackage[english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{pdfsetup}
 \usepackage{ifthen}
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Library/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,6 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
 \usepackage{ifthen}
-\usepackage[english]{babel}
 \usepackage{amsmath,amssymb,stmaryrd,textcomp,wasysym}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Probability/document/root.tex
--- a/src/HOL/Probability/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Probability/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -6,7 +6,6 @@
 \usepackage{wasysym}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{pdfsetup}
-\usepackage[english]{babel}
 
 \urlstyle{rm}
 \isabellestyle{it}
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Proofs/Lambda/document/root.tex
--- a/src/HOL/Proofs/Lambda/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Proofs/Lambda/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -1,7 +1,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage[T1]{fontenc}
+\usepackage[T1]{fontenc}
 \usepackage{graphicx}
-\usepackage[english]{babel}
 \usepackage{amssymb}
 \usepackage{textcomp}
 \usepackage{isabelle,isabellesym,pdfsetup}
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Apr 25 22:33:53 2021 +0200
@@ -271,7 +271,7 @@
                 let val {output, timing} = SystemOnTPTP.run_system_encoded args
                 in (output, timing) end
               else
-                let val res = Isabelle_System.bash_process ("exec 2>&1; " ^ command)
+                let val res = Isabelle_System.bash_process_redirect command
                 in (Process_Result.out res, Process_Result.timing_elapsed res) end
 
             val _ =
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/HOL/document/root.tex
--- a/src/HOL/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/HOL/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -4,7 +4,6 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{textcomp}
-\usepackage[english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
 \usepackage{pdfsetup}
 
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/ML/ml_process.scala	Sun Apr 25 22:33:53 2021 +0200
@@ -124,7 +124,7 @@
       use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
 
     Bash.process(
-      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
+      options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
         Bash.strings(bash_args),
       cwd = cwd,
       env = env ++ env_options ++ env_tmp ++ env_functions,
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/ML/ml_statistics.scala	Sun Apr 25 22:33:53 2021 +0200
@@ -70,7 +70,7 @@
     val env_prefix =
       if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
 
-    Bash.process(env_prefix + "exec \"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
+    Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
         Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
           ML_Syntax.print_double(delay.seconds)),
         cwd = Path.ISABELLE_HOME.file)
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/bash.scala	Sun Apr 25 22:33:53 2021 +0200
@@ -11,6 +11,7 @@
   BufferedWriter, OutputStreamWriter}
 
 import scala.annotation.tailrec
+import scala.jdk.OptionConverters._
 
 
 object Bash
@@ -65,12 +66,22 @@
     private val timing = Synchronized[Option[Timing]](None)
     def get_timing: Timing = timing.value getOrElse Timing.zero
 
-    private val script_file = Isabelle_System.tmp_file("bash_script")
-    File.write(script_file, script)
+    private val winpid_file: Option[JFile] =
+      if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None
+    private val winpid_script =
+      winpid_file match {
+        case None => script
+        case Some(file) =>
+          "read < /proc/self/winpid > /dev/null 2> /dev/null\n" +
+          """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script
+      }
+
+    private val script_file: JFile = Isabelle_System.tmp_file("bash_script")
+    File.write(script_file, winpid_script)
 
     private val proc =
       Isabelle_System.process(
-        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+        List(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)
 
@@ -89,17 +100,30 @@
 
     // signals
 
-    private val pid = stdout.readLine
+    private val group_pid = stdout.readLine
+
+    private def process_alive(pid: String): Boolean =
+      (for {
+        p <- Value.Long.unapply(pid)
+        handle <- ProcessHandle.of(p).toScala
+      } yield handle.isAlive) getOrElse false
 
-    @tailrec private def kill(signal: String, count: Int = 1): Boolean =
+    private def root_process_alive(): Boolean =
+      winpid_file match {
+        case None => process_alive(group_pid)
+        case Some(file) =>
+          file.exists() && process_alive(Library.trim_line(File.read(file)))
+      }
+
+    @tailrec private def signal(s: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
-        Isabelle_System.kill(signal, pid)
-        val running = Isabelle_System.kill("0", pid)._2 == 0
+        Isabelle_System.process_signal(group_pid, signal = s)
+        val running = root_process_alive() || Isabelle_System.process_signal(group_pid)
         if (running) {
           Time.seconds(0.1).sleep
-          kill(signal, count - 1)
+          signal(s, count - 1)
         }
         else false
       }
@@ -107,14 +131,14 @@
 
     def terminate(): Unit = Isabelle_Thread.try_uninterruptible
     {
-      kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
+      signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL")
       proc.destroy()
       do_cleanup()
     }
 
     def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
     {
-      Isabelle_System.kill("INT", pid)
+      Isabelle_System.process_signal(group_pid, "INT")
     }
 
 
@@ -133,7 +157,8 @@
       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
       catch { case _: IllegalStateException => }
 
-      script_file.delete
+      script_file.delete()
+      winpid_file.foreach(_.delete())
 
       timing.change {
         case None =>
@@ -211,7 +236,12 @@
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] =
     {
-      val result = Exn.capture { Isabelle_System.bash(cat_lines(args)) }
+      val result =
+        Exn.capture {
+          val redirect = args.head == "true"
+          val script = cat_lines(args.tail)
+          Isabelle_System.bash(script, redirect = redirect)
+        }
 
       val is_interrupt =
         result match {
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/isabelle_system.ML	Sun Apr 25 22:33:53 2021 +0200
@@ -7,6 +7,7 @@
 signature ISABELLE_SYSTEM =
 sig
   val bash_process: string -> Process_Result.T
+  val bash_process_redirect: string -> Process_Result.T
   val bash_output: string -> string * int
   val bash: string -> int
   val bash_functions: unit -> string list
@@ -34,9 +35,9 @@
 
 (* bash *)
 
-fun bash_process script =
+fun invoke_bash_process redirect script =
   Scala.function "bash_process"
-    ["export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
+    [Value.print_bool redirect, "export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script]
   |> (fn [] => raise Exn.Interrupt
       | [err] => error err
       | a :: b :: c :: d :: lines =>
@@ -53,6 +54,9 @@
          end
       | _ => raise Fail "Malformed Isabelle/Scala result");
 
+val bash_process = invoke_bash_process false;
+val bash_process_redirect = invoke_bash_process true;
+
 val bash = bash_process #> Process_Result.print #> Process_Result.rc;
 
 fun bash_output s =
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/isabelle_system.scala	Sun Apr 25 22:33:53 2021 +0200
@@ -13,6 +13,7 @@
   StandardCopyOption, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
 
+import scala.jdk.CollectionConverters._
 
 
 object Isabelle_System
@@ -465,7 +466,11 @@
     redirect: Boolean = false): Process =
   {
     val proc = new ProcessBuilder
-    proc.command(command_line:_*)  // fragile on Windows
+
+    // 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()
@@ -491,12 +496,13 @@
     (output, rc)
   }
 
-  def kill(signal: String, group_pid: String): (String, Int) =
+  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")
-    process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
+    val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
+    rc == 0
   }
 
 
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/Pure/System/platform.scala	Sun Apr 25 22:33:53 2021 +0200
@@ -14,6 +14,7 @@
   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 family: Family.Value =
     if (is_linux) Family.linux
diff -r 5c4a09c4bc9c -r 51f7bda1bfa2 src/ZF/document/root.tex
--- a/src/ZF/document/root.tex	Fri Apr 23 09:50:14 2021 +0000
+++ b/src/ZF/document/root.tex	Sun Apr 25 22:33:53 2021 +0200
@@ -2,7 +2,6 @@
 \usepackage[T1]{fontenc}
 \usepackage{graphicx,isabelle,isabellesym}
 \usepackage{amssymb}
-\usepackage[english]{babel}
 
 % this should be the last package used
 \usepackage{pdfsetup}