# HG changeset patch
# User wenzelm
# Date 1633555281 -7200
# Node ID 3984b1e91df69165b458ec94c2ecce0fe9fefcc9
# Parent  149c8ba1ebb2d7c706e68fab2c7af7eba73e6b69
tuned whitespace;

diff -r 149c8ba1ebb2 -r 3984b1e91df6 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Oct 06 21:37:59 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Oct 06 23:21:21 2021 +0200
@@ -18,9 +18,7 @@
 open Kodkod
 
 datatype sink = ToStdout | ToFile
-datatype availability =
-  Java |
-  JNI of int list
+datatype availability = Java | JNI of int list
 datatype mode = Batch | Incremental
 
 datatype sat_solver_info =
@@ -35,8 +33,7 @@
   [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
    ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    ("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
-   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
-                           "UNSAT")),
+   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", "UNSAT")),
    ("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
@@ -77,21 +74,17 @@
 
 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
     if incremental andalso mode = Batch then NONE else SOME (name, K ss)
-  | dynamic_entry_for_info incremental
-        (name, Internal (JNI from_version, mode, ss)) =
+  | dynamic_entry_for_info incremental (name, Internal (JNI from_version, mode, ss)) =
     if (incremental andalso mode = Batch) orelse
-       is_less (dict_ord int_ord (kodkodi_version (), from_version)) then
-      NONE
+       is_less (dict_ord int_ord (kodkodi_version (), from_version))
+    then NONE
     else
       let
-        val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH"
-                        |> space_explode ":"
+        val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH" |> space_explode ":"
       in
-        if exists (fn path => File.exists (Path.explode (path ^ "/")))
-                  lib_paths then
-          SOME (name, K ss)
-        else
-          NONE
+        if exists (fn path => File.exists (Path.explode (path ^ "/"))) lib_paths
+        then SOME (name, K ss)
+        else NONE
       end
   | dynamic_entry_for_info false (name, External (home, exec, args)) =
     dynamic_entry_for_external name ToStdout home exec args []