static String toXml (String s)
	{	int m=s.length();
		H.clear();
		for (int i=0; i<m; i++)
		{	char c=s.charAt(i);
			switch(c)
			{	case '<' : toH("&lt;"); break;
				case '>' : toH("&gt;"); break;
				case '&' : toH("&amp;"); break;
				case '\'' : toH("&apos;"); break;
				case '\"' : toH("&quot;"); break;
				default : H.append(c);
			}
		}
		return H.toString();
	}