annotate lib/ur/string.ur @ 1233:8d1d2f7163c2
Fix problem with overly weak ambients for queries; fix known-related bug in assert for Dt1
author |
Adam Chlipala <adamc@hcoop.net> |
date |
Tue, 13 Apr 2010 10:40:55 -0400 |
parents |
9df124fcab3d |
children |
56bd4a4f6e66 |
rev |
line source |
adamc@821
|
1 type t = Basis.string
|
adamc@821
|
2
|
adamc@1023
|
3 val str = Basis.str1
|
adamc@1023
|
4
|
adamc@828
|
5 val length = Basis.strlen
|
adamc@828
|
6 val append = Basis.strcat
|
adamc@828
|
7
|
adamc@821
|
8 val sub = Basis.strsub
|
adamc@821
|
9 val suffix = Basis.strsuffix
|
adamc@829
|
10
|
adamc@829
|
11 val index = Basis.strindex
|
adamc@829
|
12 val atFirst = Basis.strchr
|
adamc@829
|
13
|
adamc@831
|
14 fun mindex {Haystack = s, Needle = chs} = Basis.strcspn s chs
|
adamc@831
|
15
|
adamc@829
|
16 fun substring s {Start = start, Len = len} = Basis.substring s start len
|
adamc@829
|
17
|
adamc@829
|
18 fun split s ch =
|
adamc@829
|
19 case index s ch of
|
adamc@829
|
20 None => None
|
adamc@829
|
21 | Some i => Some (substring s {Start = 0, Len = i},
|
adamc@829
|
22 substring s {Start = i + 1, Len = length s - i - 1})
|
adamc@831
|
23 fun msplit {Haystack = s, Needle = chs} =
|
adamc@831
|
24 case mindex {Haystack = s, Needle = chs} of
|
adamc@831
|
25 None => None
|
adamc@831
|
26 | Some i => Some (substring s {Start = 0, Len = i},
|
adamc@831
|
27 sub s i,
|
adamc@831
|
28 substring s {Start = i + 1, Len = length s - i - 1})
|
adamc@1057
|
29
|
adamc@1057
|
30 fun all f s =
|
adamc@1057
|
31 let
|
adamc@1057
|
32 val len = length s
|
adamc@1057
|
33
|
adamc@1057
|
34 fun al i =
|
adamc@1057
|
35 i >= len
|
adamc@1057
|
36 || (f (sub s i) && al (i + 1))
|
adamc@1057
|
37 in
|
adamc@1057
|
38 al 0
|
adamc@1057
|
39 end
|
adamc@1122
|
40
|
adamc@1131
|
41 fun mp f s =
|
adamc@1131
|
42 let
|
adamc@1131
|
43 fun mp' i acc =
|
adamc@1131
|
44 if i < 0 then
|
adamc@1131
|
45 acc
|
adamc@1131
|
46 else
|
adamc@1131
|
47 mp' (i - 1) (str (f (sub s i)) ^ acc)
|
adamc@1131
|
48 in
|
adamc@1131
|
49 mp' (length s - 1) ""
|
adamc@1131
|
50 end
|
adamc@1131
|
51
|
adamc@1122
|
52 fun newlines [ctx] [[Body] ~ ctx] s : xml ([Body] ++ ctx) [] [] =
|
adamc@1122
|
53 case split s #"\n" of
|
adamc@1122
|
54 None => cdata s
|
adamc@1122
|
55 | Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml>
|
adamc@1174
|
56
|
adamc@1174
|
57 fun isPrefix {Full = f, Prefix = p} =
|
adamc@1174
|
58 length f >= length p && substring f {Start = 0, Len = length p} = p
|