author  wenzelm 
Mon, 23 Mar 2009 21:40:11 +0100  
changeset 30673  60568c168040 
parent 30638  15cc4ad0e6e9 
child 30676  edca392a2abb 
permissions  rwrr 
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/MLSystems/polyml.ML 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

2 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

3 
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1. 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

4 
*) 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

5 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

6 
open Thread; 
30673  7 

8 
structure ML_Name_Space = 

9 
struct 

10 
open PolyML.NameSpace; 

11 
type T = PolyML.NameSpace.nameSpace; 

12 
val global = PolyML.globalNameSpace; 

13 
end; 

14 

29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

15 
use "MLSystems/polyml_common.ML"; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

16 
use "MLSystems/multithreading_polyml.ML"; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

17 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

18 
val pointer_eq = PolyML.pointerEq; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

19 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

20 
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

21 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

22 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

23 
(* runtime compilation *) 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

24 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

25 
local 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

26 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

27 
fun drop_newline s = 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

28 
if String.isSuffix "\n" s then String.substring (s, 0, size s  1) 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

29 
else s; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

30 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

31 
in 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

32 

30673  33 
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context) 
34 
(start_line, name) verbose txt = 

29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

35 
let 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

36 
val current_line = ref start_line; 
30673  37 
val in_buffer = ref (String.explode (tune_source txt)); 
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

38 
val out_buffer = ref ([]: string list); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

39 
fun output () = drop_newline (implode (rev (! out_buffer))); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

40 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

41 
fun get () = 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

42 
(case ! in_buffer of 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

43 
[] => NONE 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

44 
 c :: cs => 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

45 
(in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

46 
fun put s = out_buffer := s :: ! out_buffer; 
30673  47 
fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} = 
30205  48 
(put (if hard then "Error: " else "Warning: "); 
30673  49 
PolyML.prettyPrint (put, 76) msg1; 
50 
(case context of NONE => ()  SOME msg2 => PolyML.prettyPrint (put, 76) msg2); 

51 
put ("At" ^ str_of_pos line name ^ "\n")); 

29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

52 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

53 
val parameters = 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

54 
[PolyML.Compiler.CPOutStream put, 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

55 
PolyML.Compiler.CPLineNo (fn () => ! current_line), 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

56 
PolyML.Compiler.CPErrorMessageProc put_message, 
30205  57 
PolyML.Compiler.CPNameSpace name_space, 
58 
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; 

29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

59 
val _ = 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

60 
(while not (List.null (! in_buffer)) do 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

61 
PolyML.compiler (get, parameters) ()) 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

62 
handle exn => 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

63 
(put ("Exception " ^ General.exnMessage exn ^ " raised"); 
30673  64 
error (output ()); raise exn); 
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

65 
in if verbose then print (output ()) else () end; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

66 

30673  67 
fun use_file context verbose name = 
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

68 
let 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

69 
val instream = TextIO.openIn name; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

70 
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); 
30673  71 
in use_text context (1, name) verbose txt end; 
29714
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

72 

6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

73 
end; 
30626  74 

75 

76 
(* toplevel pretty printing *) 

77 

30638  78 
fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind) 
79 
 pretty_ml (PrettyString s) = ML_Pretty.String (s, size s) 

80 
 pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2)); 

81 

30626  82 
fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts) 
83 
 ml_pretty (ML_Pretty.String (s, _)) = PrettyString s 

84 
 ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0) 

85 
 ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0); 

86 

30673  87 
fun toplevel_pp context (_: string list) pp = 
88 
use_text context (1, "pp") false 

30626  89 
("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))"); 
90 