(* Title: Pure/ML-Systems/polyml.ML
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
*)
open Thread;
structure ML_Name_Space =
struct
open PolyML.NameSpace;
type T = PolyML.NameSpace.nameSpace;
val global = PolyML.globalNameSpace;
end;
use "ML-Systems/polyml_common.ML";
use "ML-Systems/multithreading_polyml.ML";
val pointer_eq = PolyML.pointerEq;
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
(* runtime compilation *)
local
fun drop_newline s =
if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
else s;
in
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
(start_line, name) verbose txt =
let
val current_line = ref start_line;
val in_buffer = ref (String.explode (tune_source txt));
val out_buffer = ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
fun get () =
(case ! in_buffer of
[] => NONE
| c :: cs =>
(in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
fun put s = out_buffer := s :: ! out_buffer;
fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
(put (if hard then "Error: " else "Warning: ");
PolyML.prettyPrint (put, 76) msg1;
(case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
put ("At" ^ str_of_pos line name ^ "\n"));
val parameters =
[PolyML.Compiler.CPOutStream put,
PolyML.Compiler.CPLineNo (fn () => ! current_line),
PolyML.Compiler.CPErrorMessageProc put_message,
PolyML.Compiler.CPNameSpace name_space,
PolyML.Compiler.CPPrintInAlphabeticalOrder false];
val _ =
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
error (output ()); raise exn);
in if verbose then print (output ()) else () end;
fun use_file context verbose name =
let
val instream = TextIO.openIn name;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
in use_text context (1, name) verbose txt end;
end;
(* toplevel pretty printing *)
val pretty_ml =
let
fun convert len (PrettyBlock (ind, _, context, prts)) =
let
fun property name default =
(case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
SOME (ContextProperty (_, b)) => b
| NONE => default);
val bg = property "begin" "";
val en = property "end" "";
val len' = property "length" len;
in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
| convert len (PrettyString s) =
ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
| convert _ (PrettyBreak (wd, _)) =
ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
in convert "" end;
fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
PrettyBlock (ind, false,
[ContextProperty ("begin", bg), ContextProperty ("end", en)], map ml_pretty prts)
| ml_pretty (ML_Pretty.String (s, len)) =
if len = size s then PrettyString s
else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s])
| ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
| ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
fun toplevel_pp context (_: string list) pp =
use_text context (1, "pp") false
("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");