src/Pure/Thy/thy_info.ML
Wed, 19 Aug 2015 16:21:10 +0200 wenzelm avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
Sat, 15 Aug 2015 19:42:35 +0200 wenzelm clarified context;
Wed, 14 Jan 2015 16:27:19 +0100 wenzelm clarified build_theories: proper protocol handler;
Wed, 14 Jan 2015 14:28:52 +0100 wenzelm clarified build_theories;
Tue, 13 Jan 2015 21:46:09 +0100 wenzelm some support for PIDE batch session;
Mon, 22 Dec 2014 20:40:37 +0100 wenzelm discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
Mon, 22 Dec 2014 18:10:54 +0100 wenzelm proper Synchronized.var;
Mon, 22 Dec 2014 17:17:00 +0100 wenzelm removed remains from Proof General;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Fri, 31 Oct 2014 22:37:22 +0100 wenzelm provide explicit theory (amending 621c052789b4);
Fri, 31 Oct 2014 21:35:11 +0100 wenzelm obsolete;
Fri, 31 Oct 2014 21:20:06 +0100 wenzelm obsolete;
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message;
Tue, 12 Aug 2014 20:18:27 +0200 wenzelm tuned signature according to Scala version -- prefer explicit argument;
Wed, 23 Jul 2014 21:02:45 +0200 wenzelm more official Thy_Info.script_thy;
Mon, 31 Mar 2014 10:28:08 +0200 wenzelm support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Fri, 28 Feb 2014 11:13:25 +0100 wenzelm tuned errors -- in accordance to Scala version;
Fri, 14 Feb 2014 14:39:44 +0100 wenzelm more integrity checks of theory names vs. full node names;
Thu, 13 Feb 2014 22:35:38 +0100 wenzelm more integrity checks of theory names vs. full node names -- at least for the scope of a single use_thys (or "theories" section in ROOT);
Thu, 12 Dec 2013 13:23:23 +0100 wenzelm tuned message;
Fri, 22 Nov 2013 20:36:57 +0100 wenzelm tuned messages;
Sat, 16 Nov 2013 22:17:45 +0100 wenzelm prefer explicit "document" flag -- eliminated stateful Present.no_document;
Sat, 16 Nov 2013 13:12:02 +0100 wenzelm tuned signature;
Wed, 06 Nov 2013 20:58:11 +0100 wenzelm join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
Tue, 03 Sep 2013 11:29:01 +0200 wenzelm Execution.fork formally requires registered Execution.running;
Sun, 25 Aug 2013 20:32:26 +0200 wenzelm maintain goal forks as part of global execution;
Sun, 25 Aug 2013 17:04:22 +0200 wenzelm simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
Tue, 09 Apr 2013 15:59:02 +0200 wenzelm clarified protocol_message undefinedness;
Wed, 13 Mar 2013 21:25:08 +0100 wenzelm clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
Mon, 04 Mar 2013 11:36:16 +0100 wenzelm join all proofs before scheduling present phase (ordered according to weight);
Mon, 04 Mar 2013 10:02:58 +0100 wenzelm more explicit datatype result;
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;
Tue, 26 Feb 2013 19:44:26 +0100 wenzelm fork diagnostic commands (theory loader and PIDE interaction);
Wed, 20 Feb 2013 15:22:22 +0100 wenzelm more tight representation of command timing;
Tue, 19 Feb 2013 12:58:32 +0100 wenzelm support for prescient timing information within command transactions;
Sun, 13 Jan 2013 19:45:32 +0100 wenzelm more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
Sat, 12 Jan 2013 15:00:48 +0100 wenzelm immediate theory progress for build_dialog;
Thu, 30 Aug 2012 19:18:49 +0200 wenzelm some support for registering forked proofs within Proof.state, using its bottom context;
Thu, 30 Aug 2012 16:39:50 +0200 wenzelm tuned signature;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sun, 26 Aug 2012 22:10:27 +0200 wenzelm more accurate defining position of theory;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Thu, 23 Aug 2012 12:33:42 +0200 wenzelm simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
Wed, 22 Aug 2012 21:28:33 +0200 wenzelm tuned;
Wed, 22 Aug 2012 21:02:02 +0200 wenzelm discontinued separate list of required files -- maintain only provided files as they occur at runtime;
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, 07 Aug 2012 17:08:22 +0200 wenzelm prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
Wed, 01 Aug 2012 19:53:20 +0200 wenzelm more standard bootstrapping of Pure.thy;
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;
Sat, 03 Mar 2012 18:18:39 +0100 wenzelm clarified terminology of raw protocol messages;
Sat, 25 Feb 2012 12:34:56 +0100 wenzelm discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
Thu, 05 Jan 2012 14:34:18 +0100 wenzelm prefer raw_message for protocol implementation;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Sat, 20 Aug 2011 22:46:19 +0200 wenzelm clarified get_imports -- should not rely on accidental order within graph;
Fri, 19 Aug 2011 18:01:23 +0200 wenzelm tuned;
Wed, 17 Aug 2011 22:14:22 +0200 wenzelm more systematic handling of parallel exceptions;
less more (0) -100 -60 tip