src/Pure/Thy/thy_header.scala
19 months ago wenzelm 2017-11-01 init only once (see also c0f776b661fa);
20 months ago wenzelm 2017-10-25 more robust treatment of UTF8 in raw byte sources;
20 months ago wenzelm 2017-09-29 tuned;
24 months ago wenzelm 2017-06-26 proper bootstrap_name (amending b42743f5b595);
2017-04-21 wenzelm 2017-04-21 more precise position information;
2017-04-20 wenzelm 2017-04-20 actual update_imports operations;
2017-04-17 wenzelm 2017-04-17 special theories are always global;
2017-04-10 wenzelm 2017-04-10 clarified signature;
2017-04-05 wenzelm 2017-04-05 uniform import_name, with treatment of global and qualified theories;
2017-04-04 wenzelm 2017-04-04 more explicit types;
2017-04-03 wenzelm 2017-04-03 clarified imports;
2017-01-09 wenzelm 2017-01-09 tuned signature;
2017-01-07 wenzelm 2017-01-07 more uniform node_header (non-strict); removed dead code;
2017-01-07 wenzelm 2017-01-07 tuned signature;
2017-01-04 wenzelm 2017-01-04 clarified Document.Node.Name (again): canonical platform file; identify document models by native java.io.File;
2017-01-03 wenzelm 2017-01-03 clarified master_dir: file-URL;
2016-12-26 wenzelm 2016-12-26 more uniform treatment of file name vs. theory name and special header;
2016-12-26 wenzelm 2016-12-26 clarified header text;
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-10 wenzelm 2016-04-10 tuned;
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-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-03-17 wenzelm 2015-03-17 tight span for theory header, which is relevant for error positions (including semantic completion);
2015-03-15 wenzelm 2015-03-15 clarified span position;
2015-03-14 wenzelm 2015-03-14 clarified positions of theory imports;
2015-03-14 wenzelm 2015-03-14 misc tuning -- 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 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-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 explicit type Keyword.keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.Keywords;
2014-11-05 wenzelm 2014-11-05 clarified minor/major lexicon (like ML version);
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 command-line terminator ";" is no longer accepted;
2014-05-02 wenzelm 2014-05-02 more frugal access to theory text via Reader, reduced costs for I/O text decoding; prefer non-strict Symbol.decode, since Reader[Char] may present symbols in either way;
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;
2014-02-14 wenzelm 2014-02-14 tuned signature (in accordance to ML version);
2014-02-14 wenzelm 2014-02-14 tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
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-22 wenzelm 2012-08-22 use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader; tuned signatures;
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 tuned signature;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure.thy;
2012-07-24 wenzelm 2012-07-24 more explicit checks during parsing;
2012-07-20 wenzelm 2012-07-20 more explicit java.io.{File => JFile};
2012-03-15 wenzelm 2012-03-15 clarified syntax of prospective keywords;