src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 41940 a3b68a7a0e15
parent 41472 f6ab14e61604
child 41941 f823f7fae9a2
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 13:57:20 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Mar 13 14:51:38 2011 +0100
     1.3 @@ -782,17 +782,16 @@
     1.4  fun prelude system =
     1.5    case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
     1.6  
     1.7 -fun invoke system file_name =
     1.8 +fun invoke system file =
     1.9    let
    1.10 -    val env_var =
    1.11 -      (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP")
    1.12 -    val prog = getenv env_var
    1.13 -    val cmd =
    1.14 -      case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L "
    1.15 +    val (env_var, cmd) =
    1.16 +      (case system of
    1.17 +        SWI_PROLOG => ("EXEC_SWIPL", "\"$EXEC_SWIPL\" -f ")
    1.18 +      | YAP => ("EXEC_YAP", "\"$EXEC_YAP\" -L "))
    1.19    in
    1.20 -    if prog = "" then
    1.21 +    if getenv env_var = "" then
    1.22        (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
    1.23 -    else fst (bash_output (cmd ^ file_name))
    1.24 +    else fst (bash_output (cmd ^ File.shell_path file))
    1.25    end
    1.26  
    1.27  (* parsing prolog solution *)
    1.28 @@ -857,7 +856,7 @@
    1.29      val _ = tracing ("Generated prolog program:\n" ^ prog)
    1.30      val solution = TimeLimit.timeLimit timeout (fn prog =>
    1.31        Isabelle_System.with_tmp_file "prolog_file" (fn prolog_file =>
    1.32 -        (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
    1.33 +        (File.write prolog_file prog; invoke system prolog_file))) prog
    1.34      val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
    1.35      val tss = parse_solutions solution
    1.36    in