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