src/Pure/General/markup.ML
2007-07-12 wenzelm 2007-07-12 added get_string, get_int; tuned;
2007-07-11 wenzelm 2007-07-11 removed ident, space; added antiq; tuned;
2007-07-10 wenzelm 2007-07-10 more markup for inner and outer syntax; added enclose;
2007-07-10 wenzelm 2007-07-10 added print_mode setup (from pretty.ML); removed no_state;
2007-07-10 aspinall 2007-07-10 Add widthN to signature
2007-07-09 wenzelm 2007-07-09 proper position markup; added properties operation; tuned;
2007-07-08 wenzelm 2007-07-08 tuned;
2007-07-08 wenzelm 2007-07-08 added markup for pretty printing;
2007-07-07 wenzelm 2007-07-07 make smlnj happy;
2007-07-07 wenzelm 2007-07-07 added toplevel markup; misc cleanup;
2007-07-07 wenzelm 2007-07-07 position: line and name; tuned operations;
2007-07-07 wenzelm 2007-07-07 Common markup elements.