src/Pure/General/symbol.scala
2011-09-17 wenzelm 2011-09-17 Symbol.explode as in ML;
2011-08-17 wenzelm 2011-08-17 some convenience actions/shortcuts for control symbols;
2011-08-13 wenzelm 2011-08-13 tuned;
2011-07-09 wenzelm 2011-07-09 tuned signature;
2011-07-07 wenzelm 2011-07-07 explicit indication of type Symbol.Symbol;
2011-07-07 wenzelm 2011-07-07 simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style"; tuned implicit build/init messages;
2011-07-05 wenzelm 2011-07-05 simplified Symbol.iterator: produce strings, which are mostly preallocated; eliminated Symbol.CharSequence complications;
2011-06-22 wenzelm 2011-06-22 clarified decoded control symbols;
2011-06-21 wenzelm 2011-06-21 more uniform treatment of recode_set/recode_map; HTML spans with user fonts;
2011-06-21 wenzelm 2011-06-21 tuned iteration over short symbols;
2011-06-21 wenzelm 2011-06-21 Symbol.is_ctrl: handle decoded version as well; clarified user font font index handling;
2011-06-21 wenzelm 2011-06-21 some support for user symbol fonts;
2011-06-19 wenzelm 2011-06-19 names for control symbols without "^", which is relevant for completion;
2011-06-19 wenzelm 2011-06-19 some unicode chars for special control symbols;
2011-06-18 wenzelm 2011-06-18 do not control malformed symbols;
2011-06-18 wenzelm 2011-06-18 basic support for extended syntax styles: sub/superscript;
2011-06-17 wenzelm 2011-06-17 recovered markup for non-alphabetic keywords;
2010-11-13 wenzelm 2010-11-13 proper escape in regex;
2010-11-13 wenzelm 2010-11-13 treat Unicode "replacement character" (i.e. decoding error) is malformed;
2010-11-13 wenzelm 2010-11-13 simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);
2010-11-13 wenzelm 2010-11-13 tuned;
2010-11-08 wenzelm 2010-11-08 explicitly check uniqueness of symbol recoding;
2010-08-30 wenzelm 2010-08-30 Command.newlines: account for physical newlines;
2010-08-18 wenzelm 2010-08-18 more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned;
2010-06-26 wenzelm 2010-06-26 treat alternative newline symbols as in Isabelle/ML;
2010-05-11 wenzelm 2010-05-11 predefined spaces;
2010-05-09 wenzelm 2010-05-09 static Symbol.spaces;
2010-03-29 wenzelm 2010-03-29 adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
2010-01-11 wenzelm 2010-01-11 clarified Symbol.is_plain/is_wellformed -- is_closed was rejecting plain backslashes;
2009-12-28 wenzelm 2009-12-28 some sanity checks for symbol interpretation;
2009-12-20 wenzelm 2009-12-20 refined some Symbol operations/signatures; tuned;
2009-12-19 wenzelm 2009-12-19 refined some Symbol operations/signatures; added Symbol.Matcher; flexible Scan.Lexicon.symbols, with one/many/many1 variants;
2009-12-19 wenzelm 2009-12-19 added symbol classification; tuned;
2009-12-17 wenzelm 2009-12-17 tuned signature;
2009-12-06 wenzelm 2009-12-06 elements: more convenient result;
2009-12-06 wenzelm 2009-12-06 added elements: Interator; first isHighSurrogate, not isLowSurrogate; misc tuning and generalization;
2009-07-04 wenzelm 2009-07-04 is_open: surrogate sequence is High..Low; added class Index for decoding offsets; tuned;
2009-06-16 wenzelm 2009-06-16 added names, abbrevs;
2009-06-10 wenzelm 2009-06-10 tuned;
2009-06-10 wenzelm 2009-06-10 discontinued escaped symbols such as \\<forall> -- only one backslash should be used;
2009-06-09 wenzelm 2009-06-09 tuned;
2009-06-09 wenzelm 2009-06-09 more native Scala style; added is_open; misc tuning;
2009-01-20 wenzelm 2009-01-20 more general init of Symbol.Interpretation, independent of IsabelleSystem instance;
2008-12-27 wenzelm 2008-12-27 proper class IsabelleSystem -- no longer static; tuned;
2008-12-19 wenzelm 2008-12-19 removed Ids;
2008-08-26 wenzelm 2008-08-26 tuned append;
2008-08-25 wenzelm 2008-08-25 simplified exceptions: use plain error function / RuntimeException;
2008-08-21 wenzelm 2008-08-21 pattern: proper "." not "[.]"! tuned;
2008-08-21 wenzelm 2008-08-21 recode: proper result for unmatched symbols;
2008-08-21 wenzelm 2008-08-21 more robust pattern: look at longer matches first, added catch-all case; more private fields; reworked Recoder: more direct char/string operations, avoids inefficiency of large alternatives (java.util.regex does not optimize regexps);
2008-08-21 wenzelm 2008-08-21 read_symbols: proper IsabelleSystem.platform_path;
2008-08-17 wenzelm 2008-08-17 decode escaped symbols as well; tuned;
2008-08-16 wenzelm 2008-08-16 tuned Recoder;
2008-08-16 wenzelm 2008-08-16 more private fields;
2008-08-16 wenzelm 2008-08-16 tuned comments; simplified symbol pattern presentation: no need to keep source strings, canonical ofString does the job; auxiliary class Recoder; proper implementation of Interpretation.decode/encode;
2008-08-16 wenzelm 2008-08-16 use scala.collection.jcl.HashMap, which seems to be more efficient; char_pattern: proper matching of surrogate unicode characters, those outside the Basic Multilingual Plane; class Interpretation: misc reorganization, more serious preparation of patterns and tables;
2008-08-16 wenzelm 2008-08-16 reading symbol interpretation tables;
2008-08-15 wenzelm 2008-08-15 tuned;
2008-08-15 wenzelm 2008-08-15 Basic support for Isabelle symbols.