src/Pure/General/symbol_pos.ML
2016-04-01 wenzelm 2016-04-01 tuned signature;
2016-03-31 wenzelm 2016-03-31 clarified modules;
2016-03-31 wenzelm 2016-03-31 tuned signature;
2016-03-29 wenzelm 2016-03-29 tuned signature;
2016-03-06 wenzelm 2016-03-06 clarified treatment of fragments of Isabelle symbols during bootstrap;
2016-01-24 wenzelm 2016-01-24 tuned;
2016-01-20 wenzelm 2016-01-20 tuned signature (according to Scala version);
2015-11-19 wenzelm 2015-11-19 tuned;
2015-11-19 wenzelm 2015-11-19 trim lines for @{theory_text} similarly to @{text};
2015-10-22 wenzelm 2015-10-22 clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;
2015-10-18 wenzelm 2015-10-18 tuned signature;
2015-10-15 wenzelm 2015-10-15 trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-01 wenzelm 2014-11-01 recover via scanner; tuned signature;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete \<^sync> marker;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete tty and prompt;
2014-08-27 wenzelm 2014-08-27 tuned signature -- prefer quasi-abstract Symbol_Pos.source;
2014-03-01 wenzelm 2014-03-01 tuned signature;
2014-03-01 wenzelm 2014-03-01 clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
2014-02-24 wenzelm 2014-02-24 clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;
2014-01-20 wenzelm 2014-01-20 tuned signature;
2014-01-20 wenzelm 2014-01-20 tuned error messages, more accurate position;
2014-01-20 wenzelm 2014-01-20 tuned -- more direct err_prefix;
2014-01-20 wenzelm 2014-01-20 clarified scan_cartouche_depth, according to Scala version; more accurate error position;
2014-01-20 wenzelm 2014-01-20 tuned errors;
2014-01-18 wenzelm 2014-01-18 unused;
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
2013-12-12 wenzelm 2013-12-12 discontinued legacy_isub_isup;
2013-08-13 wenzelm 2013-08-13 disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
2013-08-08 wenzelm 2013-08-08 more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
2013-07-10 wenzelm 2013-07-10 more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
2012-12-12 wenzelm 2012-12-12 more systematic identifier variants to facilitate experimentation;
2012-11-30 wenzelm 2012-11-30 eliminated redundant is_ident -- more official is_identifier;
2012-11-28 wenzelm 2012-11-28 clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);
2012-11-27 wenzelm 2012-11-27 support for sub-structured identifier syntax (inactive);
2012-11-26 wenzelm 2012-11-26 tuned signature; tuned;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-23 wenzelm 2012-08-23 tuned messages: end-of-input rarely means physical end-of-file from the past;
2012-08-11 wenzelm 2012-08-11 tuned markup;
2012-08-10 wenzelm 2012-08-10 proper error prefixes;
2012-08-09 wenzelm 2012-08-09 refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
2011-07-23 wenzelm 2011-07-23 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
2011-07-12 wenzelm 2011-07-12 more precise Symbol_Pos.quote_string;
2011-07-08 wenzelm 2011-07-08 discontinued special treatment of hard tabulators;
2011-04-30 wenzelm 2011-04-30 more uniform variations of scan_string;
2010-12-29 wenzelm 2010-12-29 more scalable Symbol_Pos.explode;
2010-11-13 wenzelm 2010-11-13 eliminated slightly odd pervasive Symbol_Pos.symbol;
2010-05-17 wenzelm 2010-05-17 tuned signature;
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-03-19 wenzelm 2009-03-19 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML; scan_comment: recovered change_prompt; moved read_antiq to outer_lex.ML;
2009-03-18 wenzelm 2009-03-18 de-camelized Symbol_Pos;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-08-24 wenzelm 2008-08-24 untabify: silently turn tab into space if column information is unavailable;
2008-08-14 wenzelm 2008-08-14 made SML/NJ happy;
2008-08-13 wenzelm 2008-08-13 added untabify_content;
2008-08-09 wenzelm 2008-08-09 added content; simplified implode: interface and permissive padding via Position.distance_of; added range; renamed implode_delim to implode_range;
2008-08-07 wenzelm 2008-08-07 renamed SymbolPos.scan_position to SymbolPos.scan_pos; implode/explode: explicit type text = string; added implode_delim; explode: Position.reset_range;