author  wenzelm 
Sat, 21 Mar 2009 19:58:45 +0100  
changeset 30626  248de8dd839e 
parent 30619  0226c07352db 
child 30638  15cc4ad0e6e9 
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; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

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

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

9 

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

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

11 

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

12 
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

13 

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

14 

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

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

16 

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

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

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

19 
open PolyML.NameSpace; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

20 
val global = PolyML.globalNameSpace; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

21 
end; 
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 
local 
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 
fun drop_newline s = 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

26 
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

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

28 

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

29 
in 
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 
fun use_text (tune: string > string) str_of_pos 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

32 
name_space (start_line, name) (print, err) verbose txt = 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

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

34 
val current_line = ref start_line; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

35 
val in_buffer = ref (String.explode (tune txt)); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

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

37 
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

38 

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

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

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

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

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

43 
(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

44 
fun put s = out_buffer := s :: ! out_buffer; 
30205  45 
fun put_message {message, hard, location = {startLine = line, ...}, context} = 
46 
(put (if hard then "Error: " else "Warning: "); 

47 
PolyML.prettyPrint (put, 76) message; 

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

48 
put (str_of_pos line name ^ "\n")); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

49 

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

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

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

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

53 
PolyML.Compiler.CPErrorMessageProc put_message, 
30205  54 
PolyML.Compiler.CPNameSpace name_space, 
55 
PolyML.Compiler.CPPrintInAlphabeticalOrder false]; 

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

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

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

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

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

60 
(put ("Exception " ^ General.exnMessage exn ^ " raised"); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

61 
err (output ()); raise exn); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

62 
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

63 

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

64 
fun use_file tune str_of_pos name_space output verbose name = 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

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

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

67 
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

68 
in use_text tune str_of_pos name_space (1, name) output verbose txt end; 
6cef6700c841
Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
wenzelm
parents:
diff
changeset

69 

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

70 
end; 
30626  71 

72 

73 
(* toplevel pretty printing *) 

74 

75 
fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts) 

76 
 ml_pretty (ML_Pretty.String (s, _)) = PrettyString s 

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

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

79 

80 
fun toplevel_pp tune str_of_pos output (_: string list) pp = 

81 
use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false 

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

83 