src/Pure/Thy/thy_header.ML
2013-09-27 wenzelm 2013-09-27 more robust parser: 'imports' are mandatory except for bootstrapping Pure;
2013-04-05 wenzelm 2013-04-05 tuned signature -- agree with markup terminology;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2012-11-19 wenzelm 2012-11-19 alternative completion for outer syntax keywords;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-22 wenzelm 2012-08-22 clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-21 wenzelm 2012-08-21 refined Thy_Load.check_thy: find more uses in body text, based on keywords; refined Thy_Info.require_thy(s): cumulate additional keywords; slightly more value-oriented type Keywords.keywords;
2012-08-20 wenzelm 2012-08-20 added keyword kind "thy_load" (with optional list of file extensions);
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure.thy;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare minor keywords via theory header;
2012-03-15 wenzelm 2012-03-15 clarified syntax of prospective keywords;
2012-03-15 wenzelm 2012-03-15 allow multiple 'keywords' as in 'fixes'; tuned comments;
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2012-02-29 wenzelm 2012-02-29 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
2011-08-21 wenzelm 2011-08-21 tuned Parse.group: delayed failure message;
2011-08-12 wenzelm 2011-08-12 clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-03-20 wenzelm 2011-03-20 replaced File.check by specific File.check_file, File.check_dir; clarified File.full_path -- include parts of former Thy_Load.get_file; simplified Thy_Load.check_file -- do not read/digest yet; merged Thy_Load.check_thy/deps_thy -- always read text and parse header; clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator; Thy_Info.check_deps etc.: File.read exactly once;
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2010-11-13 wenzelm 2010-11-13 tuned message;
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-08-05 wenzelm 2010-08-05 somewhat uniform Thy_Header.split_thy_path in ML and Scala;
2010-07-27 wenzelm 2010-07-27 simplified Thy_Header.read -- include Source.of_string_limited here; tuned;
2010-07-24 wenzelm 2010-07-24 moved basic thy file name operations from Thy_Load to Thy_Header;
2010-05-17 wenzelm 2010-05-17 renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2009-12-22 wenzelm 2009-12-22 tuned;
2009-09-01 wenzelm 2009-09-01 modernized Thy_Header;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-08-15 wenzelm 2008-08-15 args: explicit groups for file_name, theory_name;
2008-08-14 wenzelm 2008-08-14 P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-12 wenzelm 2008-08-12 Symbol.source/OuterLex.source: more explicit do_recover argument;
2007-09-27 wenzelm 2007-09-27 read: explicit treatment of scanner failure;
2007-09-15 wenzelm 2007-09-15 removed redundant OuterLex.make_lexicon;
2007-07-19 wenzelm 2007-07-19 tuned signature;
2007-07-09 wenzelm 2007-07-09 adapted OuterLex/T.source;
2007-01-19 wenzelm 2007-01-19 renamed Isar/thy_header.ML to Thy/thy_header.ML;