src/Pure/ML-Systems/polyml.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29638 1f8f3d26a2cf
child 30627 fb9e73c01603
permissions -rw-r--r--
use long names for old-style fold combinators;
wenzelm@2341
     1
(*  Title:      Pure/ML-Systems/polyml.ML
wenzelm@2341
     2
wenzelm@28255
     3
Compatibility wrapper for Poly/ML 5.2 or later.
wenzelm@2341
     4
*)
wenzelm@2341
     5
wenzelm@28152
     6
open Thread;
wenzelm@26215
     7
use "ML-Systems/polyml_common.ML";
wenzelm@28676
     8
wenzelm@28796
     9
if ml_system = "polyml-5.2"
wenzelm@28796
    10
then use "ML-Systems/thread_dummy.ML"
wenzelm@28676
    11
else use "ML-Systems/multithreading_polyml.ML";
wenzelm@26215
    12
wenzelm@26215
    13
val pointer_eq = PolyML.pointerEq;
wenzelm@23921
    14
wenzelm@29638
    15
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
wenzelm@29638
    16
wenzelm@25023
    17
wenzelm@26390
    18
(* runtime compilation *)
wenzelm@3588
    19
wenzelm@28268
    20
structure ML_NameSpace =
wenzelm@28268
    21
struct
wenzelm@28268
    22
  open PolyML.NameSpace;
wenzelm@28268
    23
  val global = PolyML.globalNameSpace;
wenzelm@28268
    24
end;
wenzelm@28268
    25
wenzelm@26883
    26
local
wenzelm@26883
    27
wenzelm@26883
    28
fun drop_newline s =
wenzelm@26883
    29
  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
wenzelm@26883
    30
  else s;
wenzelm@26883
    31
wenzelm@26883
    32
in
wenzelm@26883
    33
wenzelm@28268
    34
fun use_text (tune: string -> string) str_of_pos
wenzelm@28268
    35
    name_space (start_line, name) (print, err) verbose txt =
wenzelm@3588
    36
  let
wenzelm@26883
    37
    val current_line = ref start_line;
wenzelm@26379
    38
    val in_buffer = ref (String.explode (tune txt));
wenzelm@5090
    39
    val out_buffer = ref ([]: string list);
wenzelm@26883
    40
    fun output () = drop_newline (implode (rev (! out_buffer)));
wenzelm@5090
    41
wenzelm@5038
    42
    fun get () =
wenzelm@5090
    43
      (case ! in_buffer of
wenzelm@26379
    44
        [] => NONE
wenzelm@26385
    45
      | c :: cs =>
wenzelm@26385
    46
          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
wenzelm@5090
    47
    fun put s = out_buffer := s :: ! out_buffer;
wenzelm@26883
    48
    fun message (msg, is_err, line) =
wenzelm@26883
    49
      (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
wenzelm@5090
    50
wenzelm@26879
    51
    val parameters =
wenzelm@26879
    52
     [PolyML.Compiler.CPOutStream put,
wenzelm@26879
    53
      PolyML.Compiler.CPLineNo (fn () => ! current_line),
wenzelm@28268
    54
      PolyML.Compiler.CPErrorMessageProc (put o message),
wenzelm@28268
    55
      PolyML.Compiler.CPNameSpace name_space];
wenzelm@26379
    56
    val _ =
wenzelm@26379
    57
      (while not (List.null (! in_buffer)) do
wenzelm@26879
    58
        PolyML.compiler (get, parameters) ())
wenzelm@26625
    59
      handle exn =>
wenzelm@26625
    60
       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
wenzelm@26625
    61
        err (output ()); raise exn);
wenzelm@26883
    62
  in if verbose then print (output ()) else () end;
wenzelm@3588
    63
wenzelm@28268
    64
fun use_file tune str_of_pos name_space output verbose name =
wenzelm@24598
    65
  let
wenzelm@24598
    66
    val instream = TextIO.openIn name;
wenzelm@26504
    67
    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
wenzelm@28268
    68
  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
wenzelm@26379
    69
wenzelm@26883
    70
end;