| author | wenzelm | 
| Sat, 08 Oct 2005 18:51:03 +0200 | |
| changeset 17791 | f4453001cbde | 
| parent 17775 | 2679ba74411f | 
| permissions | -rw-r--r-- | 
| 15604 | 1 | (* Title: HOL/Tools/res_lib.ML | 
| 2 | Author: Jia Meng, Cambridge University Computer Laboratory | |
| 3 | ID: $Id$ | |
| 4 | Copyright 2004 University of Cambridge | |
| 15347 | 5 | |
| 15604 | 6 | Some auxiliary functions frequently used by files in this directory. | 
| 15347 | 7 | *) | 
| 8 | ||
| 9 | signature RES_LIB = | |
| 10 | sig | |
| 16515 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 11 | val helper_path : string -> string -> string | 
| 17488 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 12 | val intOfPid : Posix.Process.pid -> Int.int | 
| 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 13 | val pidOfInt : Int.int -> Posix.Process.pid | 
| 15347 | 14 | end; | 
| 15 | ||
| 16 | ||
| 17 | structure ResLib : RES_LIB = | |
| 18 | struct | |
| 19 | ||
| 16515 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 20 | (*Return the path to a "helper" like SPASS or tptp2X, first checking that | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 21 | it exists. --lcp *) | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 22 | fun helper_path evar base = | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 23 | case getenv evar of | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 24 |       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
 | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 25 | | home => | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 26 | let val path = home ^ "/" ^ base | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 27 | in if File.exists (File.unpack_platform_path path) then path | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 28 | 	    else error ("Could not find the file " ^ path)
 | 
| 
7896ea4f3a87
VAMPIRE_HOME, helper_path and various stylistic tweaks
 paulson parents: 
15774diff
changeset | 29 | end; | 
| 15347 | 30 | |
| 17488 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 31 | (*** Converting between process ids and integers ***) | 
| 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 32 | |
| 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 33 | fun intOfPid pid = Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)); | 
| 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 34 | |
| 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 35 | fun pidOfInt n = Posix.Process.wordToPid (Word.toLargeWord (Word.fromInt n)); | 
| 
67376a311a2b
further simplification of the Isabelle-ATP linkup
 paulson parents: 
17305diff
changeset | 36 | |
| 15604 | 37 | end; |