# HG changeset patch
# User bulwahn
# Date 1284637746 -7200
# Node ID 3a86194d15344fbf601d224f21170aa33ac1cd08
# Parent  0ed0f015d1401a6b4c0572ba4843512ab9326810
registering code_prolog as component; using environment variable; adding settings file for prolog code generation

diff -r 0ed0f015d140 -r 3a86194d1534 etc/components
--- a/etc/components	Thu Sep 16 13:49:04 2010 +0200
+++ b/etc/components	Thu Sep 16 13:49:06 2010 +0200
@@ -17,3 +17,4 @@
 src/HOL/Mirabelle
 src/HOL/Library/Sum_Of_Squares
 src/HOL/Tools/SMT
+src/HOL/Tools/Predicate_Compile
diff -r 0ed0f015d140 -r 3a86194d1534 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 13:49:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 13:49:06 2010 +0200
@@ -104,8 +104,11 @@
 
 datatype prolog_system = SWI_PROLOG | YAP
 
+fun string_of_system SWI_PROLOG = "swiprolog"
+  | string_of_system YAP = "yap"
+
 type system_configuration = {timeout : Time.time, prolog_system : prolog_system}
-
+                                                
 structure System_Config = Generic_Data
 (
   type T = system_configuration
@@ -638,6 +641,7 @@
   in
     fst (fold_map reorder' p [])
   end
+
 (* rename variables to prolog-friendly names *)
 
 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
@@ -739,9 +743,16 @@
 
 fun invoke system file_name =
   let
+    val env_var =
+      (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP")
+    val prog = getenv env_var
     val cmd =
-      case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
-  in fst (bash_output (cmd ^ file_name)) end
+      case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L "
+  in
+    if prog = "" then
+      (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
+    else fst (bash_output (cmd ^ file_name))
+  end
 
 (* parsing prolog solution *)
 
diff -r 0ed0f015d140 -r 3a86194d1534 src/HOL/Tools/Predicate_Compile/etc/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/etc/settings	Thu Sep 16 13:49:06 2010 +0200
@@ -0,0 +1,13 @@
+
+EXEC_SWIPL=$(choosefrom \
+  "$ISABELLE_HOME/contrib/swipl/bin/swipl" \
+  "$ISABELLE_HOME/contrib_devel/swipl/bin/swipl" \
+  "$ISABELLE_HOME/../swipl" \
+  $(type -p swipl) \
+  "")
+
+EXEC_YAP=$(choosefrom \
+  "$ISABELLE_HOME/contrib/yap" \
+  "$ISABELLE_HOME/../yap" \
+  $(type -p yap) \
+  "")