src/Pure/ML-Systems/mosml.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 30672 beaadd5af500
child 31321 fe786d4633b9
permissions -rw-r--r--
more modular setup of runtime compilation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/mosml.ML
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
29284
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
     3
    Author:     Makarius
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     4
17491
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
     5
Compatibility file for Moscow ML 2.01
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     6
17491
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
     7
NOTE: saving images does not work; may run it interactively as follows:
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     8
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22252
diff changeset
     9
$ cd Isabelle/src/Pure
29284
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    10
$ isabelle-process RAW_ML_SYSTEM
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    11
> val ml_system = "mosml";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    12
> use "ML-Systems/mosml.ML";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    13
> use "ROOT.ML";
16470
051db5bb21b5 improved comment;
wenzelm
parents: 16469
diff changeset
    14
> Session.finish ();
23836
c6094fe98dfd adapted TextIO.inputLine;
wenzelm
parents: 23826
diff changeset
    15
> cd "../FOL";
16470
051db5bb21b5 improved comment;
wenzelm
parents: 16469
diff changeset
    16
> use "ROOT.ML";
24808
7c9a970d7ab5 fixed use_text;
wenzelm
parents: 24688
diff changeset
    17
> Session.finish ();
7c9a970d7ab5 fixed use_text;
wenzelm
parents: 24688
diff changeset
    18
> cd "../ZF";
7c9a970d7ab5 fixed use_text;
wenzelm
parents: 24688
diff changeset
    19
> use "ROOT.ML";
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    20
*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    21
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    22
(** ML system related **)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    23
24597
cbf2c5cf335e added ml_system_fix_ints;
wenzelm
parents: 24329
diff changeset
    24
val ml_system_fix_ints = false;
cbf2c5cf335e added ml_system_fix_ints;
wenzelm
parents: 24329
diff changeset
    25
26474
94735cff132c added forget_structure;
wenzelm
parents: 26223
diff changeset
    26
fun forget_structure _ = ();
94735cff132c added forget_structure;
wenzelm
parents: 26223
diff changeset
    27
16517
4699288139f4 proper implementation of pointer_eq;
wenzelm
parents: 16502
diff changeset
    28
load "Obj";
29284
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    29
load "Word";
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    30
load "Bool";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    31
load "Int";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    32
load "Real";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    33
load "ListPair";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    34
load "OS";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    35
load "Process";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    36
load "FileSys";
21298
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
    37
load "IO";
29285
5cf577cb2253 provide structure CharVector;
wenzelm
parents: 29284
diff changeset
    38
load "CharVector";
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    39
28443
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28268
diff changeset
    40
exception Interrupt;
de653f1ad78b more robust treatment of Interrupt (cf. exn.ML);
wenzelm
parents: 28268
diff changeset
    41
23965
f93e509659c1 ML-Systems/exn.ML, ML-Systems/multithreading_dummy.ML;
wenzelm
parents: 23921
diff changeset
    42
use "ML-Systems/exn.ML";
25732
308315ee2b6d added ML-Systems/universal.ML;
wenzelm
parents: 24808
diff changeset
    43
use "ML-Systems/universal.ML";
28489
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
    44
use "ML-Systems/thread_dummy.ML";
24688
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24597
diff changeset
    45
use "ML-Systems/multithreading.ML";
a5754ca5c510 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
wenzelm
parents: 24597
diff changeset
    46
use "ML-Systems/time_limit.ML";
28268
ac8431ecd57e use_text/use_file now depend on explicit ML name space;
wenzelm
parents: 27003
diff changeset
    47
use "ML-Systems/ml_name_space.ML";
30619
0226c07352db added generic ML_Pretty interface;
wenzelm
parents: 30187
diff changeset
    48
use "ML-Systems/ml_pretty.ML";
30672
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents: 30625
diff changeset
    49
use "ML-Systems/use_context.ML";
23921
947152add153 added compatibility file for ML systems without multithreading;
wenzelm
parents: 23836
diff changeset
    50
947152add153 added compatibility file for ML systems without multithreading;
wenzelm
parents: 23836
diff changeset
    51
16517
4699288139f4 proper implementation of pointer_eq;
wenzelm
parents: 16502
diff changeset
    52
(*low-level pointer equality*)
4699288139f4 proper implementation of pointer_eq;
wenzelm
parents: 16502
diff changeset
    53
local val cast : 'a -> int = Obj.magic
4699288139f4 proper implementation of pointer_eq;
wenzelm
parents: 16502
diff changeset
    54
in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
4699288139f4 proper implementation of pointer_eq;
wenzelm
parents: 16502
diff changeset
    55
16469
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    56
(*proper implementation available?*)
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    57
structure IntInf =
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    58
struct
24808
7c9a970d7ab5 fixed use_text;
wenzelm
parents: 24688
diff changeset
    59
  fun divMod (x, y) = (x div y, x mod y);
29284
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    60
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    61
  local
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    62
    fun log 1 a = a
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    63
      | log n a = log (n div 2) (a + 1);
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    64
  in
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    65
    fun log2 n = if n > 0 then log n 0 else raise Domain;
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    66
  end;
4588e0070d4c isabelle-process;
wenzelm
parents: 28489
diff changeset
    67
16469
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    68
  open Int;
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    69
end;
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    70
27003
aae9b369b338 added Substring.full;
wenzelm
parents: 26884
diff changeset
    71
structure Substring =
aae9b369b338 added Substring.full;
wenzelm
parents: 26884
diff changeset
    72
struct
aae9b369b338 added Substring.full;
wenzelm
parents: 26884
diff changeset
    73
  open Substring;
aae9b369b338 added Substring.full;
wenzelm
parents: 26884
diff changeset
    74
  val full = all;
aae9b369b338 added Substring.full;
wenzelm
parents: 26884
diff changeset
    75
end;
aae9b369b338 added Substring.full;
wenzelm
parents: 26884
diff changeset
    76
16469
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    77
structure Real =
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    78
struct
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    79
  open Real;
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    80
  val realFloor = real o floor;
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    81
end;
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    82
17491
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    83
structure String =
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    84
struct
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    85
  fun isSuffix s1 s2 =
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    86
    let val n1 = size s1 and n2 = size s2
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    87
    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    88
  open String;
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    89
end;
2bd5a6e26e1e added String.isSuffix;
wenzelm
parents: 16993
diff changeset
    90
16469
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    91
structure Time =
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    92
struct
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    93
  open Time;
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    94
  fun toString t = Time.toString t
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    95
    handle Overflow => Real.toString (Time.toReal t);   (*workaround Y2004 bug*)
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    96
end;
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    97
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    98
structure OS =
16469
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
    99
struct
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   100
  open OS
28489
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   101
  structure Process =
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   102
  struct
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   103
    open Process
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   104
    fun sleep _ = raise Fail "OS.Process.sleep undefined"
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   105
  end;
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   106
  structure FileSys = FileSys
16469
7e27422c603e some minor adaptions to make it work again;
wenzelm
parents: 16266
diff changeset
   107
end;
16993
wenzelm
parents: 16681
diff changeset
   108
22252
ce77e9622002 pervasive exception Option;
wenzelm
parents: 22144
diff changeset
   109
exception Option = Option.Option;
ce77e9622002 pervasive exception Option;
wenzelm
parents: 22144
diff changeset
   110
ce77e9622002 pervasive exception Option;
wenzelm
parents: 22144
diff changeset
   111
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   112
(*limit the printing depth*)
24329
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   113
local
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   114
  val depth = ref 10;
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   115
in
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   116
  fun get_print_depth () = ! depth;
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   117
  fun print_depth n =
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   118
   (depth := n;
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   119
    Meta.printDepth := n div 2;
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   120
    Meta.printLength := n);
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24290
diff changeset
   121
end;
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   122
30625
d53d1a16d5ee replaced install_pp/make_pp by more general toplevel_pp based on use_text;
wenzelm
parents: 30619
diff changeset
   123
(*dummy implementation*)
30672
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents: 30625
diff changeset
   124
fun toplevel_pp _ _ _ = ();
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   125
16681
d54dfd724b35 dummy exception_trace;
wenzelm
parents: 16660
diff changeset
   126
(*dummy implementation*)
d54dfd724b35 dummy exception_trace;
wenzelm
parents: 16660
diff changeset
   127
fun ml_prompts p1 p2 = ();
d54dfd724b35 dummy exception_trace;
wenzelm
parents: 16660
diff changeset
   128
d54dfd724b35 dummy exception_trace;
wenzelm
parents: 16660
diff changeset
   129
(*dummy implementation*)
16660
76613dff2c9a added profiler interface (dummy);
wenzelm
parents: 16517
diff changeset
   130
fun profile (n: int) f x = f x;
76613dff2c9a added profiler interface (dummy);
wenzelm
parents: 16517
diff changeset
   131
18384
fa38cca42913 added dummy 'print' to non-polyml systems
haftmann
parents: 17824
diff changeset
   132
(*dummy implementation*)
16681
d54dfd724b35 dummy exception_trace;
wenzelm
parents: 16660
diff changeset
   133
fun exception_trace f = f ();
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   134
18384
fa38cca42913 added dummy 'print' to non-polyml systems
haftmann
parents: 17824
diff changeset
   135
(*dummy implementation*)
fa38cca42913 added dummy 'print' to non-polyml systems
haftmann
parents: 17824
diff changeset
   136
fun print x = x;
fa38cca42913 added dummy 'print' to non-polyml systems
haftmann
parents: 17824
diff changeset
   137
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   138
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   139
(** Compiler-independent timing functions **)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   140
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   141
load "Timer";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   142
21298
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   143
fun start_timing () =
30187
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   144
  let
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   145
    val timer = Timer.startCPUTimer ();
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   146
    val time = Timer.checkCPUTimer timer;
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   147
  in (timer, time) end;
21298
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   148
30187
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   149
fun end_timing (timer, {gc, sys, usr}) =
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   150
  let
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   151
    open Time;  (*...for Time.toString, Time.+ and Time.- *)
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   152
    val {gc = gc2, sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   153
    val user = usr2 - usr + gc2 - gc;
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   154
    val all = user + sys2 - sys;
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   155
    val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
b92b3375e919 end_timing: generalized result -- message plus with explicit time values;
wenzelm
parents: 29285
diff changeset
   156
  in {message = message, user = user, all = all} end;
21298
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   157
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   158
fun check_timer timer =
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   159
  let val {sys, usr, gc} = Timer.checkCPUTimer timer
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   160
  in (sys, usr, gc) end;
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   161
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   162
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   163
(* SML basis library fixes *)
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   164
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   165
structure TextIO =
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   166
struct
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   167
  fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""};
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   168
  open TextIO;
23836
c6094fe98dfd adapted TextIO.inputLine;
wenzelm
parents: 23826
diff changeset
   169
  fun inputLine is =
c6094fe98dfd adapted TextIO.inputLine;
wenzelm
parents: 23826
diff changeset
   170
    let val s = TextIO.inputLine is
c6094fe98dfd adapted TextIO.inputLine;
wenzelm
parents: 23826
diff changeset
   171
    in if s = "" then NONE else SOME s end;
28489
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   172
  fun getOutstream _ = ();
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   173
  structure StreamIO =
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   174
  struct
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   175
    fun setBufferMode _ = ();
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   176
  end
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   177
end;
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   178
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   179
structure IO =
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   180
struct
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   181
  open IO;
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   182
  val BLOCK_BUF = ();
21298
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   183
end;
6d2306b2376d tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 21280
diff changeset
   184
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   185
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   186
(* ML command execution *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   187
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   188
(*Can one redirect 'use' directly to an instream?*)
30672
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents: 30625
diff changeset
   189
fun use_text ({tune_source, ...}: use_context) _ _ txt =
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   190
  let
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   191
    val tmp_name = FileSys.tmpName ();
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   192
    val tmp_file = TextIO.openOut tmp_name;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   193
  in
30672
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents: 30625
diff changeset
   194
    TextIO.output (tmp_file, tune_source txt);
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   195
    TextIO.closeOut tmp_file;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   196
    use tmp_name;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   197
    FileSys.remove tmp_name
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   198
  end;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   199
30672
beaadd5af500 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
wenzelm
parents: 30625
diff changeset
   200
fun use_file _ _ name = use name;
21770
ea6f846d8c4b added use_file;
wenzelm
parents: 21298
diff changeset
   201
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   202
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   203
16993
wenzelm
parents: 16681
diff changeset
   204
(** interrupts **)      (*Note: may get into race conditions*)
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   205
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   206
(* FIXME proper implementation available? *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   207
26084
a7475459c740 replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents: 25732
diff changeset
   208
fun interruptible f x = f x;
a7475459c740 replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
wenzelm
parents: 25732
diff changeset
   209
fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   210
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   211
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   212
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   213
(** OS related **)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   214
26223
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   215
(*dummy implementation*)
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   216
structure Posix =
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   217
struct
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   218
  structure ProcEnv =
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   219
  struct
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   220
    fun getpid () = 0;
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   221
  end;  
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   222
end;
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   223
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   224
local
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   225
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   226
fun read_file name =
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   227
  let val is = TextIO.openIn name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26474
diff changeset
   228
  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
26223
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   229
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   230
fun write_file name txt =
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   231
  let val os = TextIO.openOut name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26474
diff changeset
   232
  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
26223
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   233
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   234
in
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   235
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   236
fun system_out script =
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   237
  let
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   238
    val script_name = OS.FileSys.tmpName ();
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   239
    val _ = write_file script_name script;
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   240
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   241
    val output_name = OS.FileSys.tmpName ();
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   242
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   243
    val status =
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   244
      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   245
        script_name ^ " /dev/null " ^ output_name);
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   246
    val rc = if status = OS.Process.success then 0 else 1;
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   247
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   248
    val output = read_file output_name handle IO.Io _ => "";
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   249
    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   250
    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   251
  in (output, rc) end;
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   252
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   253
end;
f4a1a96cc07c specific system_out (MosML lacks structure Posix);
wenzelm
parents: 26220
diff changeset
   254
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22252
diff changeset
   255
val cd = OS.FileSys.chDir;
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22252
diff changeset
   256
val pwd = OS.FileSys.getDir;
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22252
diff changeset
   257
28489
404649964f09 removed obsolete Posix/Signal compatibility wrappers;
wenzelm
parents: 28443
diff changeset
   258
val process_id = Int.toString o Posix.ProcEnv.getpid;
17824
36b2978d339a added string_of_pid;
wenzelm
parents: 17491
diff changeset
   259
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   260
fun getenv var =
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   261
  (case Process.getEnv var of
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   262
    NONE => ""
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   263
  | SOME txt => txt);