Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* cpif-dev.sml |
2 | * 2005 Matthew Fluet (mfluet@acm.org) | |
3 | * Adapted for MLton. | |
4 | *) | |
5 | ||
6 | (* cpif-dev.sml | |
7 | * A simple pretty-printing device that eventually writes to a | |
8 | * text file unless the current contents of that file coincides | |
9 | * with what's being written. | |
10 | * | |
11 | * (C) 2002, Lucent Technologies, Bell Labs | |
12 | * | |
13 | * author: Matthias Blume (blume@research.bell-labs.com) | |
14 | *) | |
15 | structure CPIFDev : sig | |
16 | ||
17 | include PP_DEVICE | |
18 | ||
19 | val openOut : string * int -> device | |
20 | val closeOut : device -> unit | |
21 | ||
22 | end = struct | |
23 | ||
24 | datatype device = | |
25 | DEV of { filename: string, | |
26 | buffer : string list ref, | |
27 | wid : int } | |
28 | ||
29 | (* no style support *) | |
30 | type style = unit | |
31 | fun sameStyle _ = true | |
32 | fun pushStyle _ = () | |
33 | fun popStyle _ = () | |
34 | fun defaultStyle _ = () | |
35 | ||
36 | (* Allocate an empty buffer and remember the file name. *) | |
37 | fun openOut (f, w) = DEV { filename = f, buffer = ref [], wid = w } | |
38 | ||
39 | (* Calculate the final output and compare it with the current | |
40 | * contents of the file. If they do not coincide, write the file. *) | |
41 | fun closeOut (DEV { buffer = ref l, filename, ... }) = let | |
42 | val s = concat (rev l) | |
43 | fun write () = let | |
44 | val f = TextIO.openOut filename | |
45 | in | |
46 | TextIO.output (f, s); | |
47 | TextIO.closeOut f | |
48 | end | |
49 | in | |
50 | let val f = TextIO.openIn filename | |
51 | val s' = TextIO.inputAll f | |
52 | in | |
53 | TextIO.closeIn f; | |
54 | if s = s' then () else write () | |
55 | end handle _ => write () | |
56 | end | |
57 | ||
58 | (* maximum printing depth (in terms of boxes) *) | |
59 | fun depth _ = NONE | |
60 | ||
61 | (* the width of the device *) | |
62 | fun lineWidth (DEV{wid, ...}) = SOME wid | |
63 | (* the suggested maximum width of text on a line *) | |
64 | fun textWidth _ = NONE | |
65 | ||
66 | (* output a string/character in the current style to the device *) | |
67 | fun string (DEV { buffer, ... }, s) = buffer := s :: !buffer | |
68 | ||
69 | fun char (d, c) = string (d, String.str c) | |
70 | fun space (d, n) = string (d, StringCvt.padLeft #" " n "") | |
71 | fun newline d = string (d, "\n") | |
72 | ||
73 | fun flush d = () | |
74 | end |