src/Pure/ML-Systems/polyml-experimental.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29714 6cef6700c841
child 30205 e33ce8d765b4
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/ML-Systems/polyml.ML
     2 
     3 Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
     4 *)
     5 
     6 open Thread;
     7 use "ML-Systems/polyml_common.ML";
     8 use "ML-Systems/multithreading_polyml.ML";
     9 
    10 val pointer_eq = PolyML.pointerEq;
    11 
    12 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    13 
    14 
    15 (* toplevel pretty printers *)
    16 
    17 (*dummy version*)
    18 fun make_pp path pprint = ();
    19 fun install_pp _ = ();
    20 
    21 
    22 (* runtime compilation *)
    23 
    24 structure ML_NameSpace =
    25 struct
    26   open PolyML.NameSpace;
    27   val global = PolyML.globalNameSpace;
    28 end;
    29 
    30 local
    31 
    32 fun drop_newline s =
    33   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    34   else s;
    35 
    36 in
    37 
    38 fun use_text (tune: string -> string) str_of_pos
    39     name_space (start_line, name) (print, err) verbose txt =
    40   let
    41     val current_line = ref start_line;
    42     val in_buffer = ref (String.explode (tune txt));
    43     val out_buffer = ref ([]: string list);
    44     fun output () = drop_newline (implode (rev (! out_buffer)));
    45 
    46     fun get () =
    47       (case ! in_buffer of
    48         [] => NONE
    49       | c :: cs =>
    50           (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    51     fun put s = out_buffer := s :: ! out_buffer;
    52     fun put_message (prt, is_err, {file, line, offset}) =
    53      (put (if is_err then "Error: " else "Warning: ");
    54       PolyML.prettyPrint (put, 76) prt;
    55       put (str_of_pos line name ^ "\n"));
    56 
    57     val parameters =
    58      [PolyML.Compiler.CPOutStream put,
    59       PolyML.Compiler.CPLineNo (fn () => ! current_line),
    60       PolyML.Compiler.CPErrorMessageProc put_message,
    61       PolyML.Compiler.CPNameSpace name_space];
    62     val _ =
    63       (while not (List.null (! in_buffer)) do
    64         PolyML.compiler (get, parameters) ())
    65       handle exn =>
    66        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    67         err (output ()); raise exn);
    68   in if verbose then print (output ()) else () end;
    69 
    70 fun use_file tune str_of_pos name_space output verbose name =
    71   let
    72     val instream = TextIO.openIn name;
    73     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    74   in use_text tune str_of_pos name_space (1, name) output verbose txt end;
    75 
    76 end;