src/Pure/ProofGeneral/proof_general_pgip.ML
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-09-05 ago use setmp_noncritical for PGIP, which is presumably sequential (PG clone);
2010-08-27 ago discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
2010-08-27 ago eliminated obsolete Output.no_warnings, where no warnings were produced anyway;
2010-08-27 ago expanded some aliases from structure Unsynchronized;
2010-08-09 ago Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
2010-08-08 ago explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-07 ago simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
2010-07-27 ago theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
2010-07-27 ago 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;
2010-07-25 ago simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
2010-07-25 ago simplified handling of theory begin/end wrt. toplevel and theory loader;
2010-07-20 ago 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;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-15 ago renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-05-06 ago replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
2010-04-15 ago spelling;
2009-11-02 ago modernized structure Proof_Display;
2009-10-20 ago tuned;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-23 ago use regular Display.string_of_thm_global;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-06 ago ML_Compiler.exn_message;
2009-03-26 ago pretty_thm_aux etc.: explicit show_status flag;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-01-27 ago proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
2009-01-21 ago removed Ids;
2009-01-05 ago Isar.init;
2008-11-16 ago proof_body/pthm: removed redundant types field;
2008-11-16 ago clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 ago retrieve thm deps from proof_body;
2008-10-14 ago CRITICAL access to preferences;
2008-10-04 ago simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
2008-10-01 ago more robust treatment of Interrupt (cf. exn.ML);
2008-09-26 ago eliminated polymorphic equality;
2008-09-03 ago simplified Toplevel.add_hook: cover successful transactions only;
2008-09-02 ago refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
2008-09-02 ago added new_thms_deps (operates on global facts, some name_hint approximation);
2008-09-01 ago extended interface to preferences to allow adding new ones
2008-08-28 ago changed Markup print mode to YXML -- explicitly decode messages before being issued;
2008-08-27 ago get rid of tabs;
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-13 ago ProofDisplay.add_hook;
2008-08-11 ago renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-07-15 ago added status channel;
2008-07-14 ago removed obsolete Toplevel.RESTART;
2008-07-14 ago command 'redo' no longer available;
2008-06-25 ago moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-12 ago sane versions of (qualified_)thms_of_thy;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-04-18 ago removed dead code;
2008-04-17 ago replaced token translations by common markup;
2008-04-10 ago simplified isarcmd;
2008-04-10 ago ThyInfo.get_names;
2008-04-10 ago moved global Toplevel state to structure Isar;
2008-04-03 ago renamed XML.parse_comment_whspc to XML.parse_comments;
2008-04-03 ago further cleanup of XML signature;
2008-04-03 ago XML.string_of, XML.parse;