src/Pure/ML-Systems/alice.ML
author wenzelm
Tue, 24 Jul 2007 19:44:33 +0200
changeset 23962 e0358fac0541
parent 23921 947152add153
child 23965 f93e509659c1
permissions -rw-r--r--
Runtime exceptions as values (from library.ML);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22563
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/alice.ML
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
     3
22837
82cceaf768c8 updated Alice version;
wenzelm
parents: 22576
diff changeset
     4
Compatibility file for Alice 1.4.
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
     5
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
     6
NOTE: there is no wrapper script; may run it interactively as follows:
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
     7
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
     8
$ cd Isabelle/src/Pure
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
     9
$ env ALICE_JIT_MODE=0 alice
23835
1990e9acc7d1 tuned comment;
wenzelm
parents: 23826
diff changeset
    10
- val ml_system = "alice";
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
    11
- use "ML-Systems/alice.ML";
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
    12
- use "ROOT.ML";
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
    13
- Session.finish ();
22563
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    14
*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    15
23921
947152add153 added compatibility file for ML systems without multithreading;
wenzelm
parents: 23835
diff changeset
    16
use "ML-Systems/no_multithreading.ML";
947152add153 added compatibility file for ML systems without multithreading;
wenzelm
parents: 23835
diff changeset
    17
947152add153 added compatibility file for ML systems without multithreading;
wenzelm
parents: 23835
diff changeset
    18
22563
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    19
fun exit 0 = (OS.Process.exit OS.Process.success): unit
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    20
  | exit _ = OS.Process.exit OS.Process.failure;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    21
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    22
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    23
(** ML system related **)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    24
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    25
(*low-level pointer equality*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    26
fun pointer_eq (_: 'a, _: 'a) = false;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    27
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    28
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    29
(* restore old-style character / string functions *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    30
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    31
exception Ord;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    32
fun ord "" = raise Ord
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    33
  | ord s = Char.ord (String.sub (s, 0));
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    34
22575
2ed8a11f3172 fixed chr/explode;
wenzelm
parents: 22563
diff changeset
    35
val chr = String.str o chr;
2ed8a11f3172 fixed chr/explode;
wenzelm
parents: 22563
diff changeset
    36
val explode = map String.str o String.explode;
22563
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    37
val implode = String.concat;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    38
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    39
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    40
(* Poly/ML emulation *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    41
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    42
fun quit () = exit 0;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    43
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    44
fun print_depth n = Print.depth := n;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    45
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    46
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    47
(* compiler-independent timing functions *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    48
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    49
structure Timer =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    50
struct
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    51
  open Timer;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    52
  type cpu_timer = unit;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    53
  fun startCPUTimer () = ();
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    54
  fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    55
  fun checkGCTime () = Time.zeroTime;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    56
end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    57
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    58
fun start_timing () =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    59
  let val CPUtimer = Timer.startCPUTimer();
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    60
      val time = Timer.checkCPUTimer(CPUtimer)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    61
  in  (CPUtimer,time)  end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    62
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    63
fun end_timing (CPUtimer, {sys,usr}) =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    64
  let open Time  (*...for Time.toString, Time.+ and Time.- *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    65
      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    66
  in  "User " ^ toString (usr2-usr) ^
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    67
      "  All "^ toString (sys2-sys + usr2-usr) ^
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    68
      " secs"
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    69
      handle Time => ""
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    70
  end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    71
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    72
fun check_timer timer =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    73
  let
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    74
    val {sys, usr} = Timer.checkCPUTimer timer;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    75
    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    76
  in (sys, usr, gc) end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    77
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    78
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    79
(*prompts*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    80
fun ml_prompts p1 p2 = ();
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    81
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    82
(*dummy implementation*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    83
fun profile (n: int) f x = f x;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    84
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    85
(*dummy implementation*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    86
fun exception_trace f = f ();
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    87
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    88
(*dummy implementation*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    89
fun print x = x;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    90
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    91
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    92
(* toplevel pretty printing (see also Pure/install_pp.ML) *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    93
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    94
fun make_pp path pprint = (path, pprint);
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    95
fun install_pp (path, pp) = ();
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    96
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    97
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    98
(* ML command execution *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
    99
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   100
fun use_text name (print, err) verbose txt = (Compiler.eval txt; ());
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   101
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   102
fun use_file _ _ name = use name;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   103
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   104
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   105
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   106
(** interrupts **)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   107
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   108
exception Interrupt;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   109
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   110
fun ignore_interrupt f x = f x;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   111
fun raise_interrupt f x = f x;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   112
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   113
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   114
(* basis library fixes *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   115
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   116
structure TextIO =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   117
struct
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   118
  open TextIO;
23139
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents: 22837
diff changeset
   119
  fun inputLine is = TextIO.inputLine is
22563
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   120
    handle IO.Io _ => raise Interrupt;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   121
end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   122
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   123
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   124
(* bounded time execution *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   125
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   126
(*dummy implementation*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   127
fun interrupt_timeout time f x =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   128
  f x;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   129
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   130
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   131
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   132
(** OS related **)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   133
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
   134
(* current directory *)
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
   135
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
   136
val cd = OS.FileSys.chDir;
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
   137
val pwd = OS.FileSys.getDir;
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
   138
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 23139
diff changeset
   139
22563
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   140
(* system command execution *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   141
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   142
(*execute Unix command which doesn't take any input from stdin and
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   143
  sends its output to stdout; could be done more easily by Unix.execute,
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   144
  but that function doesn't use the PATH*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   145
fun execute command =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   146
  let
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   147
    val tmp_name = OS.FileSys.tmpName ();
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   148
    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   149
    val result = TextIO.inputAll is;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   150
  in
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   151
    TextIO.closeIn is;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   152
    OS.FileSys.remove tmp_name;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   153
    result
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   154
  end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   155
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   156
(*plain version; with return code*)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   157
val system = OS.Process.system: string -> int;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   158
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   159
structure OS =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   160
struct
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   161
  open OS;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   162
  structure FileSys =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   163
  struct
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   164
    fun fileId name =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   165
      (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   166
        "" => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   167
      | s => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   168
    val compare = Int.compare;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   169
    open FileSys;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   170
  end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   171
end;
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   172
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   173
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   174
(* getenv *)
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   175
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   176
fun getenv var =
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   177
  (case OS.Process.getEnv var of
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   178
    NONE => ""
78fb2af1a5c3 Compatibility file for Alice 1.3 -- experimental!
wenzelm
parents:
diff changeset
   179
  | SOME txt => txt);