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