# HG changeset patch
# User wenzelm
# Date 1212005611 -7200
# Node ID 616c553c7cf1942093ac71cb217923f891fa354c
# Parent  aae9b369b338bd64dbb378bf1d34c88e76d90da3
added ISABELLE_HOME to startup;
pathed OS.FileSys.tmpName to drop C string terminator;
added OS.FileSys.fullPath;

diff -r aae9b369b338 -r 616c553c7cf1 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Wed May 28 21:06:17 2008 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Wed May 28 22:13:31 2008 +0200
@@ -6,7 +6,7 @@
 NOTE: there is no wrapper script; may run it interactively as follows:
 
 $ cd Isabelle/src/Pure
-$ env ALICE_JIT_MODE=0 alice
+$ env ALICE_JIT_MODE=0 ISABELLE_HOME=$(cd ../..; pwd) alice
 - val ml_system = "alice";
 - use "ML-Systems/exn.ML";
 - use "ML-Systems/universal.ML";
@@ -145,6 +145,21 @@
 
 (** OS related **)
 
+structure OS =
+struct
+  open OS;
+  structure FileSys =
+  struct
+    open FileSys;
+    fun tmpName () =
+      let val name = FileSys.tmpName () in
+        if String.isSuffix "\000" name
+        then String.substring (name, 0, size name - 1)
+        else name
+      end;
+  end;
+end;
+
 val cd = OS.FileSys.chDir;
 val pwd = OS.FileSys.getDir;
 
@@ -189,10 +204,23 @@
         ("", _) => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
       | (s, _) => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
     val compare = Int.compare;
+    fun fullPath name =
+      (case system_out ("FILE='" ^ name ^
+        "' && cd \"$(dirname \"$FILE\")\" && echo -n \"$(pwd -P)/$(basename \"$FILE\")\"") of
+        ("", _) => raise SysErr ("Bad file", NONE)
+      | (s, _) => s);
     open FileSys;
   end;
 end;
 
+structure Posix =
+struct
+  structure ProcEnv =
+  struct
+    fun getpid () = raise Fail "Posix.ProcEnv.getpoid undefined";
+  end;
+end;
+
 fun string_of_pid _ = raise Fail "string_of_pid undefined";
 
 fun getenv var =