src/Pure/Thy/thy_header.scala
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;
2012-03-15 wenzelm 2012-03-15 explicit Outer_Syntax.Decl;
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;
2012-02-26 wenzelm 2012-02-26 tuned signature; clarified check;
2011-08-30 wenzelm 2011-08-30 do not normalized extra file dependencies for now -- still loaded by prover process;
2011-08-16 wenzelm 2011-08-16 more robust Thy_Header.base_name, with minimal assumptions about path syntax; Isabelle.buffer_path: keep platform syntax;
2011-08-16 wenzelm 2011-08-16 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;
2011-08-13 wenzelm 2011-08-13 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
2011-08-12 wenzelm 2011-08-12 normalized theory dependencies wrt. file_store;
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-08-12 wenzelm 2011-08-12 simplified class Thy_Header;
2011-08-11 wenzelm 2011-08-11 uniform treatment of header edits as document edits;
2011-07-12 wenzelm 2011-07-12 tuned XML modules;
2011-07-10 wenzelm 2011-07-10 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;
2011-07-10 wenzelm 2011-07-10 more abstract signature; tuned;
2011-07-10 wenzelm 2011-07-10 simplified XML_Data;
2011-07-10 wenzelm 2011-07-10 less currying in Scala;
2011-07-10 wenzelm 2011-07-10 propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;
2011-07-08 wenzelm 2011-07-08 tuned signature;
2011-07-07 wenzelm 2011-07-07 explicit Document.Node.Header, with master_dir and thy_name; imitate ML path operations more closely;