src/HOL/Tools/Nitpick/kodkod_sat.ML
changeset 74481 9333a6ee57ba
parent 74479 bf34175e64dc
child 74486 74a36aae067a
equal deleted inserted replaced
74480:d8015e659e15 74481:9333a6ee57ba
    49    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    49    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    50    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
    50    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
    51 
    51 
    52 fun dynamic_entry_for_external name dev home exec args markers =
    52 fun dynamic_entry_for_external name dev home exec args markers =
    53   let
    53   let
    54     fun make_args dir () =
    54     fun make_args () =
    55       let
    55       let
    56         val serial_str = serial_string ()
    56         val serial_str = serial_string ()
    57         val base = name ^ serial_str
    57         val base = name ^ serial_str
    58         val out_file = base ^ ".out"
    58         val out_file = base ^ ".out"
    59         val dir_sep =
    59         val exe = Path.variable home + Path.platform_exe (Path.basic exec)
    60           if String.isSubstring "\\" dir andalso not (String.isSubstring "/" dir)
       
    61           then "\\" else "/"
       
    62       in
    60       in
    63        [if null markers then "External" else "ExternalV2",
    61        [if null markers then "External" else "ExternalV2"] @
    64         dir ^ dir_sep ^ exec, base ^ ".cnf"] @
    62        [File.platform_path exe, base ^ ".cnf"] @
    65         (if null markers then []
    63        (if null markers then [] else [if dev = ToFile then out_file else ""]) @ markers @
    66          else [if dev = ToFile then out_file else ""]) @ markers @
       
    67        (if dev = ToFile then [out_file] else []) @ args
    64        (if dev = ToFile then [out_file] else []) @ args
    68       end
    65       end
    69   in case getenv home of "" => NONE | dir => SOME (name, make_args dir) end
    66   in if getenv home = "" then NONE else SOME (name, make_args) end
    70 
    67 
    71 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    68 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    72     if incremental andalso mode = Batch then NONE else SOME (name, K ss)
    69     if incremental andalso mode = Batch then NONE else SOME (name, K ss)
    73   | dynamic_entry_for_info incremental (name, Internal (JNI from_version, mode, ss)) =
    70   | dynamic_entry_for_info incremental (name, Internal (JNI from_version, mode, ss)) =
    74     if (incremental andalso mode = Batch) orelse
    71     if (incremental andalso mode = Batch) orelse