keep smlnj HOL images around

merged

added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; adapted test configuration SML_makeall

avoid *** in normal output, which usually marks errors in logs

added Markup.Name and Markup.Kind convenience; token_style for entity kind markup;

decode_term: some context-sensitive markup; more informative Markup.entity and Name_Space.markup_entry; Markup.const: use "constant" to make it coincide with name space kind;