src/Pure/Thy/thy_header.ML
Thu, 06 Nov 2014 11:44:41 +0100 wenzelm simplified keyword kinds;
Wed, 05 Nov 2014 22:17:05 +0100 wenzelm tuned signature;
Wed, 05 Nov 2014 21:59:21 +0100 wenzelm more uniform header_keywords in ML/Scala;
Wed, 05 Nov 2014 20:49:30 +0100 wenzelm eliminated pointless dynamic keywords (TTY legacy);
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Sun, 02 Nov 2014 15:27:37 +0100 wenzelm uniform heading commands work in any context, even in theory header;
Sat, 01 Nov 2014 19:33:51 +0100 wenzelm recover via scanner;
Sat, 01 Nov 2014 18:46:48 +0100 wenzelm simplified -- scanning is never interactive;
Sat, 01 Nov 2014 15:01:41 +0100 wenzelm command-line terminator ";" is no longer accepted;
Wed, 30 Apr 2014 22:34:11 +0200 wenzelm some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
Fri, 27 Sep 2013 21:04:57 +0200 wenzelm more robust parser: 'imports' are mandatory except for bootstrapping Pure;
Fri, 05 Apr 2013 20:54:55 +0200 wenzelm tuned signature -- agree with markup terminology;
Wed, 27 Feb 2013 16:27:44 +0100 wenzelm discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
Wed, 27 Feb 2013 12:45:19 +0100 wenzelm discontinued obsolete 'uses' within theory header;
Mon, 19 Nov 2012 22:34:17 +0100 wenzelm alternative completion for outer syntax keywords;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Wed, 22 Aug 2012 12:47:49 +0200 wenzelm clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
Tue, 21 Aug 2012 20:32:33 +0200 wenzelm refined Thy_Load.check_thy: find more uses in body text, based on keywords;
Mon, 20 Aug 2012 14:09:09 +0200 wenzelm added keyword kind "thy_load" (with optional list of file extensions);
Tue, 07 Aug 2012 15:01:48 +0200 wenzelm simplified Document.Node.Header -- internalized errors;
Wed, 01 Aug 2012 19:53:20 +0200 wenzelm more standard bootstrapping of Pure.thy;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Fri, 16 Mar 2012 13:05:30 +0100 wenzelm define keywords early when processing the theory header, before running the body commands;
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header;
Thu, 15 Mar 2012 14:22:54 +0100 wenzelm clarified syntax of prospective keywords;
Thu, 15 Mar 2012 09:55:42 +0100 wenzelm allow multiple 'keywords' as in 'fixes';
Thu, 15 Mar 2012 00:10:45 +0100 wenzelm some support for outer syntax keyword declarations within theory header;
Wed, 29 Feb 2012 23:09:06 +0100 wenzelm clarified module Thy_Load;
Sun, 21 Aug 2011 20:42:26 +0200 wenzelm tuned Parse.group: delayed failure message;
Fri, 12 Aug 2011 15:28:30 +0200 wenzelm clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
Sun, 20 Mar 2011 17:40:45 +0100 wenzelm replaced File.check by specific File.check_file, File.check_dir;
Sun, 13 Mar 2011 16:01:00 +0100 wenzelm Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
Sat, 13 Nov 2010 20:49:02 +0100 wenzelm tuned message;
Sat, 13 Nov 2010 19:21:53 +0100 wenzelm simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
Thu, 05 Aug 2010 13:41:00 +0200 wenzelm somewhat uniform Thy_Header.split_thy_path in ML and Scala;
Tue, 27 Jul 2010 22:15:51 +0200 wenzelm simplified Thy_Header.read -- include Source.of_string_limited here;
Sat, 24 Jul 2010 21:22:21 +0200 wenzelm moved basic thy file name operations from Thy_Load to Thy_Header;
Mon, 17 May 2010 15:11:25 +0200 wenzelm renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Tue, 22 Dec 2009 21:46:41 +0100 wenzelm tuned;
Tue, 01 Sep 2009 14:45:06 +0200 wenzelm modernized Thy_Header;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Fri, 15 Aug 2008 15:51:06 +0200 wenzelm args: explicit groups for file_name, theory_name;
Thu, 14 Aug 2008 19:52:37 +0200 wenzelm P.doc_source and P.ml_sorce for proper SymbolPos.text;
Tue, 12 Aug 2008 21:27:48 +0200 wenzelm Symbol.source/OuterLex.source: more explicit do_recover argument;
Thu, 27 Sep 2007 11:46:05 +0200 wenzelm read: explicit treatment of scanner failure;
Sat, 15 Sep 2007 19:25:19 +0200 wenzelm removed redundant OuterLex.make_lexicon;
Thu, 19 Jul 2007 23:18:48 +0200 wenzelm tuned signature;
Mon, 09 Jul 2007 23:12:44 +0200 wenzelm adapted OuterLex/T.source;
Fri, 19 Jan 2007 22:08:14 +0100 wenzelm renamed Isar/thy_header.ML to Thy/thy_header.ML;
less more (0) tip