src/Pure/ProofGeneral/proof_general_emacs.ML
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Wed, 29 Feb 2012 23:09:06 +0100 wenzelm clarified module Thy_Load;
Mon, 28 Nov 2011 22:05:32 +0100 wenzelm separate module for concrete Isabelle markup;
Tue, 23 Aug 2011 16:53:05 +0200 wenzelm tuned signature -- contrast physical output primitives versus Output.raw_message;
Thu, 18 Aug 2011 17:53:32 +0200 wenzelm more careful treatment of exception serial numbers, with propagation to message channel;
Fri, 15 Jul 2011 13:29:00 +0200 wenzelm less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp;
Tue, 12 Jul 2011 15:32:16 +0200 wenzelm tuned signature -- less cryptic ASCII names;
Mon, 27 Jun 2011 14:38:58 +0200 wenzelm markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
Sat, 25 Jun 2011 18:15:36 +0200 wenzelm type classes: entity markup instead of old-style token markup;
Sat, 25 Jun 2011 17:17:49 +0200 wenzelm clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
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;
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);
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;
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;
Tue, 01 Jun 2010 13:32:05 +0200 wenzelm uniform ML environment setup for Isar and PG;
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;
Mon, 23 Nov 2009 22:35:54 +0100 wenzelm added command 'ProofGeneral.pr' for PG 4.0;
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;
Mon, 23 Mar 2009 17:21:42 +0100 wenzelm suppress status output for traditional tty modes (including Proof General);
Thu, 05 Mar 2009 23:12:59 +0100 wenzelm render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;
Mon, 05 Jan 2009 00:13:11 +0100 wenzelm Isar.init;
Fri, 02 Jan 2009 23:01:37 +0100 wenzelm xsymbols: use plain Symbol.output;
Fri, 02 Jan 2009 19:59:26 +0100 wenzelm removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;
Tue, 30 Sep 2008 14:19:27 +0200 wenzelm Toplevel.commit_exit: position;
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Wed, 03 Sep 2008 11:27:15 +0200 wenzelm theorem dependency hook: check previous state;
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:25 +0200 wenzelm theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
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 15:46:43 +0200 wenzelm refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
Tue, 15 Jul 2008 14:15:43 +0200 wenzelm added status channel;
Tue, 15 Jul 2008 11:50:04 +0200 wenzelm simplified commit_exit;
Mon, 14 Jul 2008 22:55:48 +0200 wenzelm print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
Mon, 14 Jul 2008 22:26:53 +0200 wenzelm tuned message;
Mon, 14 Jul 2008 21:39:08 +0200 wenzelm inform_file_processed: Isar.init_point last!
Mon, 14 Jul 2008 19:57:13 +0200 wenzelm inform_file_processed: try harder not to fail, ensure
Mon, 14 Jul 2008 17:51:44 +0200 wenzelm proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
Thu, 10 Jul 2008 21:12:34 +0200 wenzelm restart: Isar.init_point;
Thu, 10 Jul 2008 21:03:47 +0200 wenzelm proper_inform_file_processed: Isar.init_point starts fresh command sequence;
Thu, 10 Jul 2008 20:54:00 +0200 wenzelm activated new versions of undo, kill_proof;
Thu, 10 Jul 2008 20:03:30 +0200 wenzelm added ProofGeneral.isar_kill_proof;
Thu, 17 Apr 2008 16:30:52 +0200 wenzelm replaced token translations by common markup;
Mon, 14 Apr 2008 14:28:47 +0200 wenzelm Isar.toplevel_loop: separate init/welcome flag;
Thu, 10 Apr 2008 14:53:29 +0200 wenzelm ThyInfo.get_names;
Thu, 10 Apr 2008 13:44:43 +0200 wenzelm replaced Isar loop variants by generic toplevel_loop;
Thu, 03 Apr 2008 21:23:41 +0200 wenzelm moved test_markup here;
Thu, 03 Apr 2008 18:42:40 +0200 wenzelm XML.output_markup;
Thu, 03 Apr 2008 16:03:56 +0200 wenzelm Symbol.SOH;
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Wed, 05 Mar 2008 22:58:12 +0100 wenzelm IsabelleProcess.output_markup;
Sun, 06 Jan 2008 15:57:56 +0100 wenzelm replaced prompt markup by prompt channel setup;
Sun, 30 Dec 2007 23:07:31 +0100 wenzelm tuned;
Fri, 14 Dec 2007 21:15:36 +0100 wenzelm tuned;
Thu, 06 Dec 2007 00:21:32 +0100 wenzelm moved basic test_markup to isabelle_process.ML;
Mon, 19 Nov 2007 11:09:09 +0100 wenzelm inform_file_processed: made even more robust against bad file specs;
Sun, 18 Nov 2007 16:10:12 +0100 wenzelm removed unused inform_file_processed;
Thu, 15 Nov 2007 11:49:04 +0100 wenzelm thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
Thu, 25 Oct 2007 16:57:57 +0200 wenzelm made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
Sat, 06 Oct 2007 22:31:57 +0200 wenzelm removed obsolete write_keywords;
Sat, 06 Oct 2007 21:21:45 +0200 wenzelm export init_outer_syntax;
Sat, 06 Oct 2007 17:53:45 +0200 wenzelm tuned;
Sat, 06 Oct 2007 16:50:04 +0200 wenzelm simplified interfaces for outer syntax;
Tue, 25 Sep 2007 17:06:14 +0200 wenzelm proper Sign operations instead of Theory aliases;
Fri, 07 Sep 2007 22:13:45 +0200 wenzelm added hilite markup;
Sun, 19 Aug 2007 12:43:05 +0200 aspinall Use 376/377 specials for sendback markup
Wed, 15 Aug 2007 19:24:23 +0200 wenzelm added sendback;
Mon, 13 Aug 2007 18:10:22 +0200 wenzelm Lexicon.read_indexname/nat/variable;
Tue, 31 Jul 2007 00:56:32 +0200 wenzelm ThyInfo.register_thy;
Sun, 22 Jul 2007 21:20:58 +0200 wenzelm inform_file_processed: tuned msg, no state;
Tue, 10 Jul 2007 16:45:05 +0200 wenzelm removed no_state markup -- produce empty state;
Mon, 09 Jul 2007 11:44:23 +0200 wenzelm simplified writeln_fn;
Sat, 07 Jul 2007 18:39:21 +0200 wenzelm toplevel prompt/print_state: proper markup, removed hooks;
Sat, 07 Jul 2007 00:15:02 +0200 wenzelm simplified pretty token metric: type int;
Sun, 15 Apr 2007 14:31:59 +0200 wenzelm removed unused Output.panic hook -- internal to PG wrapper;
Sat, 14 Apr 2007 17:36:05 +0200 wenzelm Term.string_of_vname;
Wed, 04 Apr 2007 00:11:23 +0200 wenzelm removed unused info channel;
Thu, 01 Feb 2007 20:40:34 +0100 wenzelm proper use of PureThy.has_name_hint instead of hard-wired string'';
Wed, 31 Jan 2007 20:07:40 +0100 aspinall Fix tell_thm_deps to match changse in PureThy.
Mon, 22 Jan 2007 15:34:15 +0100 aspinall Comment
Thu, 04 Jan 2007 19:27:08 +0100 wenzelm broken error handling for command syntax -- reverted to revision 1.9;
Thu, 04 Jan 2007 11:56:53 +0100 haftmann eliminated Option.app
Wed, 03 Jan 2007 22:59:30 +0100 aspinall Fix error reporting in Emacs to also match Isar command failure exactly.
Sat, 30 Dec 2006 16:20:32 +0100 wenzelm removed dead code;
Sat, 30 Dec 2006 16:08:09 +0100 wenzelm removed conditional combinator;
Sat, 30 Dec 2006 12:33:29 +0100 wenzelm inform_file_processed: Toplevel.init_empty;
Fri, 29 Dec 2006 19:50:50 +0100 wenzelm removed obsolete init_pgip;
Fri, 29 Dec 2006 18:46:06 +0100 wenzelm tuned;
Fri, 29 Dec 2006 18:25:46 +0100 wenzelm minor tuning;
Fri, 15 Dec 2006 00:08:06 +0100 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
Tue, 05 Dec 2006 13:56:43 +0100 aspinall Support PGIP communication for preferences in Emacs mode.
Mon, 04 Dec 2006 22:12:08 +0100 aspinall Add separate PG Emacs configuration
less more (0) tip