src/Pure/Thy/thy_header.ML
20 months ago wenzelm 2017-10-06 clarified error for bad session-qualified imports;
2017-06-01 wenzelm 2017-06-01 tuned signature;
2017-04-10 wenzelm 2017-04-10 clarified signature;
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-09-22 wenzelm 2016-09-22 discontinued raw symbols; discontinued Symbol.source; use initial Symbol.explode;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-07-11 wenzelm 2016-07-11 clarified keywords;
2016-07-11 wenzelm 2016-07-11 clarified keywords;
2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2016-04-19 wenzelm 2016-04-19 more IDE support for Isabelle/Pure bootstrap;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2016-04-09 wenzelm 2016-04-09 support ROOT0.ML as well -- independently of ROOT.ML;
2016-04-06 wenzelm 2016-04-06 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
2016-02-28 wenzelm 2016-02-28 discontinued old 'header';
2015-10-17 wenzelm 2015-10-17 added 'paragraph', 'subparagraph';
2015-08-17 wenzelm 2015-08-17 support for ML files with/without debugger information;
2015-04-06 wenzelm 2015-04-06 more position information and PIDE markup for command keywords;
2015-03-17 wenzelm 2015-03-17 misc tuning and simplification;
2015-03-14 wenzelm 2015-03-14 misc tuning -- more uniform ML vs. Scala;
2015-03-14 wenzelm 2015-03-14 tunes signature -- more uniform ML vs. Scala;
2014-11-13 wenzelm 2014-11-13 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
2014-11-07 wenzelm 2014-11-07 tuned;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-06 wenzelm 2014-11-06 tuned signature;
2014-11-06 wenzelm 2014-11-06 tuned signature;
2014-11-06 wenzelm 2014-11-06 simplified keyword kinds; more explicit bootstrap syntax;
2014-11-05 wenzelm 2014-11-05 tuned signature;
2014-11-05 wenzelm 2014-11-05 more uniform header_keywords in ML/Scala; tuned signature;
2014-11-05 wenzelm 2014-11-05 eliminated pointless dynamic keywords (TTY legacy);
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-11-02 wenzelm 2014-11-02 uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;
2014-11-01 wenzelm 2014-11-01 recover via scanner; tuned signature;
2014-11-01 wenzelm 2014-11-01 simplified -- scanning is never interactive;
2014-11-01 wenzelm 2014-11-01 command-line terminator ";" is no longer accepted;
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
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;