equal
deleted
inserted
replaced
51 (* unpack *) |
51 (* unpack *) |
52 |
52 |
53 local |
53 local |
54 |
54 |
55 val scan_host = |
55 val scan_host = |
56 (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --| |
56 (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --| |
57 Scan.ahead ($$ "/" || Scan.one Symbol.is_eof); |
57 Scan.ahead ($$ "/" || Scan.one Symbol.is_eof); |
58 |
58 |
59 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode); |
59 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode); |
60 val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/"); |
60 val scan_path_root = Scan.any Symbol.not_eof >> (Path.unpack o implode o cons "/"); |
61 |
61 |