src/Pure/ProofGeneral/proof_general_pgip.ML
Thu, 03 Mar 2011 15:56:17 +0100 wenzelm re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;
Mon, 10 Jan 2011 15:45:46 +0100 wenzelm eliminated Int.toString;
Wed, 29 Dec 2010 18:18:42 +0100 wenzelm theory loader: implicit load path is considered legacy;
Mon, 25 Oct 2010 21:23:09 +0200 wenzelm more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Mon, 27 Sep 2010 20:26:10 +0200 wenzelm renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Mon, 20 Sep 2010 15:08:51 +0200 wenzelm added XML.content_of convenience -- cover XML.body, which is the general situation;
Fri, 17 Sep 2010 22:17:57 +0200 wenzelm discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
Thu, 09 Sep 2010 17:20:27 +0200 wenzelm more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
Sun, 05 Sep 2010 23:31:12 +0200 wenzelm use setmp_noncritical for PGIP, which is presumably sequential (PG clone);
Fri, 27 Aug 2010 22:09:51 +0200 wenzelm discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
Fri, 27 Aug 2010 20:28:58 +0200 wenzelm eliminated obsolete Output.no_warnings, where no warnings were produced anyway;
Fri, 27 Aug 2010 14:07:09 +0200 wenzelm expanded some aliases from structure Unsynchronized;
Mon, 09 Aug 2010 18:18:32 +0200 wenzelm Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
Sat, 07 Aug 2010 21:03:06 +0200 wenzelm simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
Tue, 27 Jul 2010 23:01:42 +0200 wenzelm theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
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 21:42:39 +0200 wenzelm simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
Sun, 25 Jul 2010 14:41:48 +0200 wenzelm simplified handling of theory begin/end wrt. toplevel and theory loader;
Tue, 20 Jul 2010 14:44:33 +0200 wenzelm eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sat, 15 May 2010 23:40:00 +0200 wenzelm renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Thu, 06 May 2010 23:52:20 +0200 wenzelm replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
Thu, 15 Apr 2010 15:38:58 +0200 wenzelm spelling;
Mon, 02 Nov 2009 20:57:48 +0100 wenzelm modernized structure Proof_Display;
Tue, 20 Oct 2009 21:22:37 +0200 wenzelm tuned;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 23 Jul 2009 16:43:31 +0200 wenzelm use regular Display.string_of_thm_global;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Sat, 06 Jun 2009 21:11:23 +0200 wenzelm ML_Compiler.exn_message;
Thu, 26 Mar 2009 15:18:50 +0100 wenzelm pretty_thm_aux etc.: explicit show_status flag;
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name;
Tue, 27 Jan 2009 00:29:37 +0100 wenzelm proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Mon, 05 Jan 2009 00:13:11 +0100 wenzelm Isar.init;
Sun, 16 Nov 2008 22:12:44 +0100 wenzelm proof_body/pthm: removed redundant types field;
Sun, 16 Nov 2008 20:03:42 +0100 wenzelm clarified Thm.proof_body_of vs. Thm.proof_of;
Sat, 15 Nov 2008 21:31:35 +0100 wenzelm retrieve thm deps from proof_body;
Tue, 14 Oct 2008 15:16:13 +0200 wenzelm CRITICAL access to preferences;
Sat, 04 Oct 2008 17:40:56 +0200 wenzelm simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
Wed, 01 Oct 2008 12:00:02 +0200 wenzelm more robust treatment of Interrupt (cf. exn.ML);
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Wed, 03 Sep 2008 11:09:08 +0200 wenzelm simplified Toplevel.add_hook: cover successful transactions only;
Tue, 02 Sep 2008 23:27:44 +0200 wenzelm refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
Tue, 02 Sep 2008 22:20:27 +0200 wenzelm added new_thms_deps (operates on global facts, some name_hint approximation);
Mon, 01 Sep 2008 10:20:14 +0200 nipkow extended interface to preferences to allow adding new ones
Thu, 28 Aug 2008 00:33:17 +0200 wenzelm changed Markup print mode to YXML -- explicitly decode messages before being issued;
Wed, 27 Aug 2008 12:00:28 +0200 wenzelm get rid of tabs;
Thu, 14 Aug 2008 16:52:46 +0200 wenzelm moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
Wed, 13 Aug 2008 20:57:35 +0200 wenzelm ProofDisplay.add_hook;
Mon, 11 Aug 2008 18:37:49 +0200 wenzelm renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
Tue, 15 Jul 2008 14:15:43 +0200 wenzelm added status channel;
Mon, 14 Jul 2008 17:51:47 +0200 wenzelm removed obsolete Toplevel.RESTART;
Mon, 14 Jul 2008 11:19:42 +0200 wenzelm command 'redo' no longer available;
Wed, 25 Jun 2008 17:38:32 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
less more (0) -100 -60 tip