src/Pure/ML-Systems/polyml.ML
author wenzelm
Mon, 02 Aug 1999 15:39:04 +0200
changeset 7148 e9c253036b45
parent 7147 ff492d5d77cc
child 7855 092a6435afad
permissions -rw-r--r--
removed obsolete concat;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml.ML
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     5
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
     6
Compatibility file for Poly/ML (versions 2.x and 3.x).
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     7
*)
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     8
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
     9
open PolyML ExtendedIO;
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    10
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    11
(*needs the Basis Library emulation*)
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    12
use "basis.ML";
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    13
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    14
6042
0ccde2f25dd6 Basis Library compatible substring oeration
paulson
parents: 5813
diff changeset
    15
structure String =
7148
e9c253036b45 removed obsolete concat;
wenzelm
parents: 7147
diff changeset
    16
struct
6042
0ccde2f25dd6 Basis Library compatible substring oeration
paulson
parents: 5813
diff changeset
    17
  fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j)
0ccde2f25dd6 Basis Library compatible substring oeration
paulson
parents: 5813
diff changeset
    18
                          handle Substring => raise Subscript
7147
ff492d5d77cc String.isPrefix
paulson
parents: 7114
diff changeset
    19
  fun isPrefix s1 s2 = (s1 = substring(s2,0, size s1))
ff492d5d77cc String.isPrefix
paulson
parents: 7114
diff changeset
    20
                       handle Subscript => false
7148
e9c253036b45 removed obsolete concat;
wenzelm
parents: 7147
diff changeset
    21
end;
6042
0ccde2f25dd6 Basis Library compatible substring oeration
paulson
parents: 5813
diff changeset
    22
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    23
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    24
(** ML system related **)
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    25
4326
7211ea5f29e2 New timing functions startTiming and endTiming
paulson
parents: 3631
diff changeset
    26
(** Compiler-independent timing functions **)
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    27
4326
7211ea5f29e2 New timing functions startTiming and endTiming
paulson
parents: 3631
diff changeset
    28
(*Note start point for timing*)
7211ea5f29e2 New timing functions startTiming and endTiming
paulson
parents: 3631
diff changeset
    29
fun startTiming() = System.processtime ();
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    30
4326
7211ea5f29e2 New timing functions startTiming and endTiming
paulson
parents: 3631
diff changeset
    31
(*Finish timing and return string*)
5813
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    32
fun endTiming before =
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    33
  "User + GC: " ^
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    34
  makestring (real (System.processtime () - before) / 10.0) ^
4326
7211ea5f29e2 New timing functions startTiming and endTiming
paulson
parents: 3631
diff changeset
    35
  " secs";
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    36
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    37
4977
6cec2c0ffdbf added ml_prompts;
wenzelm
parents: 4428
diff changeset
    38
(* prompts *)
6cec2c0ffdbf added ml_prompts;
wenzelm
parents: 4428
diff changeset
    39
4984
d17004d4c13b fixed ml_prompts;
wenzelm
parents: 4977
diff changeset
    40
fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
4977
6cec2c0ffdbf added ml_prompts;
wenzelm
parents: 4428
diff changeset
    41
6cec2c0ffdbf added ml_prompts;
wenzelm
parents: 4428
diff changeset
    42
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    43
(* toplevel pretty printing (see also Pure/install_pp.ML) *)
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    44
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    45
fun make_pp _ pprint (str, blk, brk, en) obj =
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    46
  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    47
    fn () => brk (99999, 0), en);
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    48
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    49
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    50
(* ML command execution -- 'eval' *)
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    51
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    52
fun use_text verbose txt =
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    53
  let
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    54
    val in_buffer = ref (explode txt);
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    55
    val out_buffer = ref ([]: string list);
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    56
5038
301c37df931d use_text replaces use_strings;
wenzelm
parents: 4984
diff changeset
    57
    fun get () =
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    58
      (case ! in_buffer of
5038
301c37df931d use_text replaces use_strings;
wenzelm
parents: 4984
diff changeset
    59
        [] => ""
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    60
      | c :: cs => (in_buffer := cs; c));
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    61
    fun put s = out_buffer := s :: ! out_buffer;
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    62
5038
301c37df931d use_text replaces use_strings;
wenzelm
parents: 4984
diff changeset
    63
    fun exec () =
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    64
      (case ! in_buffer of
5038
301c37df931d use_text replaces use_strings;
wenzelm
parents: 4984
diff changeset
    65
        [] => ()
5090
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    66
      | _ => (PolyML.compiler (get, put) (); exec ()));
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    67
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    68
    fun show_output () = print (implode (rev (! out_buffer)));
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    69
  in
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    70
    exec () handle exn => (show_output (); raise exn);
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    71
    if verbose then show_output () else ()
75ac9b451ae0 use_text: verbose flag;
wenzelm
parents: 5038
diff changeset
    72
  end;
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    73
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    74
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    75
5813
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    76
(** interrupts **)      (*Note: may get into race conditions*)
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    77
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    78
fun mask_interrupt f x = f x;
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    79
fun unmask_interrupt f x = f x;
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    80
fun exhibit_interrupt f x = f x;
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    81
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    82
4eea84a9427d fake interrupt handler;
wenzelm
parents: 5090
diff changeset
    83
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    84
(** OS related **)
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    85
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    86
local
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    87
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    88
fun drop_last [] = []
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    89
  | drop_last [x] = []
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    90
  | drop_last (x :: xs) = x :: drop_last xs;
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    91
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    92
val drop_last_char = implode o drop_last o explode;
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    93
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    94
in
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    95
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    96
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    97
(* system command execution *)
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
    98
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
    99
(*execute Unix command which doesn't take any input from stdin and
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   100
  sends its output to stdout*)
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   101
fun execute command =
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   102
  let
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   103
    val (is, os) =  ExtendedIO.execute command;
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   104
    val result = input (is, 999999);
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   105
  in
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   106
    close_out os;
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   107
    close_in is;
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   108
    result
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   109
  end;
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   110
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   111
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   112
(* file handling *)
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   113
6227
3198f547f8af fixed file_info;
wenzelm
parents: 6042
diff changeset
   114
(*get time of last modification*)
3198f547f8af fixed file_info;
wenzelm
parents: 6042
diff changeset
   115
fun file_info name = Int.toString (System.filedate name) handle _ => "";
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   116
3588
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   117
structure OS =
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   118
struct
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   119
  structure FileSys =
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   120
  struct
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   121
    val chDir = PolyML.cd;
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   122
    fun remove name = (execute ("rm " ^ name); ());
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   123
    fun getDir () = drop_last_char (execute "pwd");
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   124
  end;
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   125
end;
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   126
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   127
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   128
(* getenv *)
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   129
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   130
fun getenv var = drop_last_char
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   131
  (execute ("env | grep '^" ^ var ^ "=' | sed -e 's/" ^ var ^ "=//'"));
e487bf0ed6c4 cleaned up;
wenzelm
parents: 2408
diff changeset
   132
2341
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   133
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   134
end;
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   135
e154da40ef00 Compatibility file for Poly/ML (versions 2.x, 3.x).
wenzelm
parents:
diff changeset
   136
4428
5c26253b8a2e tuned comment;
wenzelm
parents: 4326
diff changeset
   137
(* non-ASCII input (see also Thy/use.ML) *)
2408
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2341
diff changeset
   138
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2341
diff changeset
   139
val needs_filtered_use =
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2341
diff changeset
   140
  (case explode ml_system of
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2341
diff changeset
   141
    "p" :: "o" :: "l" :: "y" :: "m" :: "l" :: "-" :: "3" :: _ => true
acddf41dbbf7 added needs_filtered_use;
wenzelm
parents: 2341
diff changeset
   142
  | _ => false);