// URLs ////////////////////////////////////////////////////////////////////////////// #import tokens.g as tok // "public" ///////////////////////////////////////////////////////////////////// Path:: = urlchar+ Email:: = username "@" Host URL:: = method "://" Login Host Port (()|"/"|"/" Path) (()|"#"|"#" Path) -> (~(urlc|[%\#]) | avoidOnUrlTail) // An url must not end with these characters if it appears "bare" // inline within a text block (ie without braces surrounding it). // This ensures that punctuation doesn't "stick" to the end of the url. avoidOnUrlTail = [,.;)!] // "private" //////////////////////////////////////////////////////////////////// Login:: = username "@" | username ":" password "@" | () Host = IP:: tok.digit "." tok.digit "." tok.digit "." tok.digit | DNS:: (part:: [a-zA-Z0-9\-]++) ++/ "." Port:: = (":" `tok.Int)? username:: = [a-zA-Z0-9;/?:&=$\-_.+]++ password:: = [a-zA-Z0-9;/?:&=$\-_.+]++ method:: = [+\-.a-z0-9]+ urlchar = urlc | "%":: "%" [0-9] [0-9] urlc = [a-zA-Z0-9;/?:&=$\-_.+] | [@~,] // technically illegal (RFC1738)