src/Pure/Thy/thy_load.ML
Wed, 22 Aug 2012 12:47:49 +0200 wenzelm clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
Wed, 22 Aug 2012 12:17:55 +0200 wenzelm tuned;
Wed, 22 Aug 2012 11:56:13 +0200 wenzelm tuned errors;
Tue, 21 Aug 2012 22:26:34 +0200 wenzelm prefer File.full_path in accordance to check_file;
Tue, 21 Aug 2012 21:48:32 +0200 wenzelm more standard Thy_Load.check_thy for Pure.thy, relying on its header;
Tue, 21 Aug 2012 20:32:33 +0200 wenzelm refined Thy_Load.check_thy: find more uses in body text, based on keywords;
Tue, 21 Aug 2012 11:00:54 +0200 wenzelm tuned;
Mon, 20 Aug 2012 21:52:31 +0200 wenzelm more robust cleaning of "% tag" and "-- cmt";
Mon, 20 Aug 2012 17:05:53 +0200 wenzelm some support for inlining file content into outer syntax token language;
Fri, 16 Mar 2012 14:42:11 +0100 wenzelm defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
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 00:10:45 +0100 wenzelm some support for outer syntax keyword declarations within theory header;
Sun, 04 Mar 2012 16:02:14 +0100 wenzelm clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
Wed, 29 Feb 2012 23:09:06 +0100 wenzelm clarified module Thy_Load;
Thu, 25 Aug 2011 19:12:58 +0200 wenzelm tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
Sun, 21 Aug 2011 14:16:44 +0200 wenzelm discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
Sun, 21 Aug 2011 13:42:55 +0200 wenzelm discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
Sat, 13 Aug 2011 20:41:29 +0200 wenzelm simplified Toplevel.init_theory: discontinued special master argument;
Wed, 10 Aug 2011 16:05:14 +0200 wenzelm future_job: explicit indication of interrupts;
Fri, 08 Jul 2011 21:44:47 +0200 wenzelm moved Outer_Syntax.load_thy to Thy_Load.load_thy;
Fri, 08 Jul 2011 14:37:19 +0200 wenzelm more abstract Thy_Load.load_file/use_file for external theory resources;
Fri, 08 Jul 2011 11:50:58 +0200 wenzelm clarified Thy_Load.digest_file -- read ML files only once;
Sun, 20 Mar 2011 17:40:45 +0100 wenzelm replaced File.check by specific File.check_file, File.check_dir;
Sun, 20 Mar 2011 13:49:21 +0100 wenzelm tuned;
Sun, 13 Mar 2011 20:56:00 +0100 wenzelm files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
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;
Thu, 03 Mar 2011 18:10:28 +0100 wenzelm discontinued legacy load path;
Fri, 14 Jan 2011 13:58:07 +0100 wenzelm Thy_Load.begin_theory: maintain source specification of imports;
Wed, 29 Dec 2010 18:18:42 +0100 wenzelm theory loader: implicit load path is considered legacy;
Wed, 29 Dec 2010 13:51:17 +0100 wenzelm check_file: secondary load path is legacy feature;
Sat, 27 Nov 2010 14:32:08 +0100 wenzelm prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
Sat, 27 Nov 2010 14:19:04 +0100 wenzelm moved file identification to thy_load.ML (where it is actually used);
Fri, 19 Nov 2010 21:14:12 +0100 wenzelm do not export Thy_Load.required, to avoid confusion about the interface;
Thu, 26 Aug 2010 15:48:08 +0200 wenzelm renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
Tue, 03 Aug 2010 15:53:36 +0200 wenzelm simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
Tue, 27 Jul 2010 22:15:51 +0200 wenzelm simplified Thy_Header.read -- include Source.of_string_limited here;
Tue, 27 Jul 2010 22:00:26 +0200 wenzelm simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
Sun, 25 Jul 2010 12:57:29 +0200 wenzelm Thy_Load.check_loaded via Theory.at_end;
Sat, 24 Jul 2010 21:22:21 +0200 wenzelm moved basic thy file name operations from Thy_Load to Thy_Header;
Sat, 24 Jul 2010 12:14:53 +0200 wenzelm moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
Thu, 22 Jul 2010 23:29:39 +0200 wenzelm tuned message;
Thu, 22 Jul 2010 22:31:20 +0200 wenzelm discontinued special treatment of ML files -- no longer complete extensions on demand;
Thu, 22 Jul 2010 20:46:45 +0200 wenzelm eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
Thu, 22 Jul 2010 20:36:41 +0200 wenzelm tuned signature;
Wed, 21 Jul 2010 21:08:40 +0200 wenzelm replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
Wed, 21 Jul 2010 20:32:08 +0200 wenzelm deps_thy/load_thy: store compact text to reduce space by factor 12;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Tue, 27 Oct 2009 13:15:04 +0100 wenzelm tuned;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Thu, 01 Oct 2009 15:44:42 +0200 wenzelm eliminated redundant parameters;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Tue, 01 Sep 2009 14:45:06 +0200 wenzelm modernized Thy_Header;
Fri, 16 Jan 2009 15:20:05 +0100 wenzelm export check_name;
Fri, 09 Jan 2009 23:34:36 +0100 wenzelm added split_thy_path;
Wed, 14 May 2008 11:05:08 +0200 wenzelm renamed Position.path to Path.position;
Thu, 10 Apr 2008 15:04:11 +0200 wenzelm eliminated backpatching of load_thy;
Fri, 28 Mar 2008 00:02:54 +0100 wenzelm reorganized signature of ML_Context;
Wed, 08 Aug 2007 23:07:48 +0200 wenzelm simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
Sun, 29 Jul 2007 22:41:58 +0200 wenzelm load_thy: avoid reloading of text;
Mon, 23 Jul 2007 20:47:56 +0200 wenzelm marked some CRITICAL sections;
less more (0) -60 tip