diff options
| author | Vladimir Azarov <avm@intermediate-node.net> | 2025-08-04 15:12:55 +0200 |
|---|---|---|
| committer | Vladimir Azarov <avm@intermediate-node.net> | 2025-08-04 15:12:55 +0200 |
| commit | 396ebf0c76153e5e1e9dc77371bdd02b4d3d85d1 (patch) | |
| tree | 3c2aab25631581d5367a6288c2eb9e0f812d76b0 /stream.sml | |
| parent | 671760c2b5857312cac178f24cad8686c1d4b719 (diff) | |
Flattening of initializers
Diffstat (limited to 'stream.sml')
| -rw-r--r-- | stream.sml | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -73,6 +73,8 @@ structure Stream :> STREAM = struct fun create fname = createFromInstream fname (TextIO.openIn fname) + fun createFromString s = createFromInstream s (TextIO.openString s) + fun getOffset ({ off, ... }: t) = off fun isFirstOnLine ({ contents, ... }: t) off = |