proper platform_path for executables run from Java;

--- a/src/Doc/Nitpick/document/root.tex	Thu Oct 07 13:04:15 2021 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Thu Oct 07 13:10:53 2021 +0200
@@ -2196,9 +2196,6 @@
 the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
 \texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
 executable.%
-\footnote{Important note for Cygwin users: The path must be specified using
-native Windows syntax. Make sure to escape backslashes properly.%
-\label{cygwin-paths}}
 The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
 \url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
 Nitpick has been tested with version 2.51.
@@ -2212,7 +2209,6 @@
 written in \cpp{}. To use MiniSat, set the environment variable
 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
 executable.%
-\footref{cygwin-paths}
 The \cpp{} sources and executables for MiniSat are available at
 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
 and 2.2.
@@ -2226,7 +2222,6 @@
 \item[\labelitemi] \textbf{\textit{Riss3g}:} Riss3g is an efficient solver written in
 \cpp{}. To use Riss3g, set the environment variable \texttt{RISS3G\_HOME} to the
 directory that contains the \texttt{riss3g} executable.%
-\footref{cygwin-paths}
 The \cpp{} sources for Riss3g are available at
 \url{http://tools.computational-logic.org/content/riss3g.php}.
 Nitpick has been tested with the SAT Competition 2013 version.
@@ -2234,7 +2229,6 @@
 \item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written
 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
 the directory that contains the \texttt{zchaff} executable.%
-\footref{cygwin-paths}
 The \cpp{} sources and executables for zChaff are available at
 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
 versions 2004-05-13, 2004-11-15, and 2007-03-12.
@@ -2242,7 +2236,6 @@
 \item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver written in
 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
 directory that contains the \texttt{rsat} executable.%
-\footref{cygwin-paths}
 The \cpp{} sources for RSat are available at
 \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
 2.01.
@@ -2250,7 +2243,7 @@
 \item[\labelitemi] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
 written in C. To use BerkMin, set the environment variable
 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
-executable.\footref{cygwin-paths}
+executable.
 The BerkMin executables are available at
 \url{http://eigold.tripod.com/BerkMin.html}.
 
@@ -2259,7 +2252,6 @@
 version of BerkMin, set the environment variable
 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
 executable.%
-\footref{cygwin-paths}
 
 \item[\labelitemi] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
 written in Java that can be used incrementally. It is bundled with Kodkodi and

--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Oct 07 13:04:15 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Oct 07 13:10:53 2021 +0200
@@ -51,22 +51,19 @@
 
 fun dynamic_entry_for_external name dev home exec args markers =
   let
-    fun make_args dir () =
+    fun make_args () =
       let
         val serial_str = serial_string ()
         val base = name ^ serial_str
         val out_file = base ^ ".out"
-        val dir_sep =
-          if String.isSubstring "\\" dir andalso not (String.isSubstring "/" dir)
-          then "\\" else "/"
+        val exe = Path.variable home + Path.platform_exe (Path.basic exec)
       in
-       [if null markers then "External" else "ExternalV2",
-        dir ^ dir_sep ^ exec, base ^ ".cnf"] @
-        (if null markers then []
-         else [if dev = ToFile then out_file else ""]) @ markers @
+       [if null markers then "External" else "ExternalV2"] @
+       [File.platform_path exe, base ^ ".cnf"] @
+       (if null markers then [] else [if dev = ToFile then out_file else ""]) @ markers @
        (if dev = ToFile then [out_file] else []) @ args
       end
-  in case getenv home of "" => NONE | dir => SOME (name, make_args dir) end
+  in if getenv home = "" then NONE else SOME (name, make_args) end
 
 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
     if incremental andalso mode = Batch then NONE else SOME (name, K ss)