src/Pure/General/symbol.ML
2004-01-26 schirmer 2004-01-26 * Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy
2003-10-15 kleing 2003-10-15 use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)
2003-10-15 kleing 2003-10-15 included \<^sub> in the range of identifier chars
2003-10-08 paulson 2003-10-08 now accepts DOS and Mac line breaks
2003-08-29 skalberg 2003-08-29 Removed the extended digits again.
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2002-11-27 berghofe 2002-11-27 default_output now escapes \'s more carefully.
2002-09-05 paulson 2002-09-05 added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier
2002-02-20 wenzelm 2002-02-20 added is_quasi; added bump_string (clarified version of old Library.bump_string);
2001-11-09 wenzelm 2001-11-09 got rid of obsolete input filtering;
2001-01-31 wenzelm 2001-01-31 added strip_blanks;
2001-01-21 wenzelm 2001-01-21 added spaces; added default_indent, indent;
2001-01-16 wenzelm 2001-01-16 export plain_output;
2000-12-29 wenzelm 2000-12-29 scan: malformed result;
2000-12-23 wenzelm 2000-12-23 tuned length;
2000-09-15 wenzelm 2000-09-15 updated;
2000-05-30 wenzelm 2000-05-30 fixed comment;
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-03 wenzelm 2000-04-03 tuned recover;
2000-02-10 wenzelm 2000-02-10 is_symbolic;
1999-06-30 wenzelm 1999-06-30 added sync marker;
1999-05-21 wenzelm 1999-05-21 avoid string constants;
1999-05-12 wenzelm 1999-05-12 rearranged order of modules;
1999-03-09 wenzelm 1999-03-09 tuned using nth_elem_string, exists_string;
1999-02-11 wenzelm 1999-02-11 added output_width; output subject to print_mode;
1999-02-04 wenzelm 1999-02-04 added 'use';
1999-01-29 oheimb 1999-01-29 renamed space2 to spacespace prepared switch for escaped output of symbols (used for ProofGeneral in connection with the x-symbol package)
1999-01-13 wenzelm 1999-01-13 fixed titles;
1999-01-13 wenzelm 1999-01-13 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;