Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
Wed, 29 Feb 2012 23:09:06 +0100 |
wenzelm |
clarified module Thy_Load;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
Tue, 23 Aug 2011 16:53:05 +0200 |
wenzelm |
tuned signature -- contrast physical output primitives versus Output.raw_message;
|
file |
diff |
annotate
|
Thu, 18 Aug 2011 17:53:32 +0200 |
wenzelm |
more careful treatment of exception serial numbers, with propagation to message channel;
|
file |
diff |
annotate
|
Fri, 15 Jul 2011 13:29:00 +0200 |
wenzelm |
less ambitious ProofGeneral markup, which occasionally breaks plain-old regexps in elisp;
|
file |
diff |
annotate
|
Tue, 12 Jul 2011 15:32:16 +0200 |
wenzelm |
tuned signature -- less cryptic ASCII names;
|
file |
diff |
annotate
|
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";
|
file |
diff |
annotate
|
Sat, 25 Jun 2011 18:15:36 +0200 |
wenzelm |
type classes: entity markup instead of old-style token markup;
|
file |
diff |
annotate
|
Sat, 25 Jun 2011 17:17:49 +0200 |
wenzelm |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
Mon, 27 Sep 2010 20:26:10 +0200 |
wenzelm |
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 22:09:51 +0200 |
wenzelm |
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 20:28:58 +0200 |
wenzelm |
eliminated obsolete Output.no_warnings, where no warnings were produced anyway;
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 14:07:09 +0200 |
wenzelm |
expanded some aliases from structure Unsynchronized;
|
file |
diff |
annotate
|
Mon, 09 Aug 2010 18:18:32 +0200 |
wenzelm |
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
|
file |
diff |
annotate
|
Sun, 08 Aug 2010 19:36:31 +0200 |
wenzelm |
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
|
file |
diff |
annotate
|
Sat, 07 Aug 2010 21:03:06 +0200 |
wenzelm |
simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
|
file |
diff |
annotate
|
Tue, 27 Jul 2010 23:01:42 +0200 |
wenzelm |
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Sun, 25 Jul 2010 21:42:39 +0200 |
wenzelm |
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
|
file |
diff |
annotate
|
Sun, 25 Jul 2010 14:41:48 +0200 |
wenzelm |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
file |
diff |
annotate
|
Sat, 24 Jul 2010 21:22:21 +0200 |
wenzelm |
moved basic thy file name operations from Thy_Load to Thy_Header;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 01 Jun 2010 13:32:05 +0200 |
wenzelm |
uniform ML environment setup for Isar and PG;
|
file |
diff |
annotate
|
Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|
Sat, 15 May 2010 23:16:32 +0200 |
wenzelm |
refer directly to structure Keyword and Parse;
|
file |
diff |
annotate
|
Mon, 23 Nov 2009 22:35:54 +0100 |
wenzelm |
added command 'ProofGeneral.pr' for PG 4.0;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Mon, 23 Mar 2009 17:21:42 +0100 |
wenzelm |
suppress status output for traditional tty modes (including Proof General);
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Mon, 05 Jan 2009 00:13:11 +0100 |
wenzelm |
Isar.init;
|
file |
diff |
annotate
|
Fri, 02 Jan 2009 23:01:37 +0100 |
wenzelm |
xsymbols: use plain Symbol.output;
|
file |
diff |
annotate
|
Fri, 02 Jan 2009 19:59:26 +0100 |
wenzelm |
removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;
|
file |
diff |
annotate
|
Tue, 30 Sep 2008 14:19:27 +0200 |
wenzelm |
Toplevel.commit_exit: position;
|
file |
diff |
annotate
|
Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
Wed, 03 Sep 2008 11:27:15 +0200 |
wenzelm |
theorem dependency hook: check previous state;
|
file |
diff |
annotate
|
Wed, 03 Sep 2008 11:09:08 +0200 |
wenzelm |
simplified Toplevel.add_hook: cover successful transactions only;
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 23:27:44 +0200 |
wenzelm |
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 22:20:25 +0200 |
wenzelm |
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
|
file |
diff |
annotate
|
Wed, 27 Aug 2008 12:00:28 +0200 |
wenzelm |
get rid of tabs;
|
file |
diff |
annotate
|
Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
Wed, 13 Aug 2008 20:57:35 +0200 |
wenzelm |
ProofDisplay.add_hook;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
Tue, 15 Jul 2008 14:15:43 +0200 |
wenzelm |
added status channel;
|
file |
diff |
annotate
|
Tue, 15 Jul 2008 11:50:04 +0200 |
wenzelm |
simplified commit_exit;
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 22:55:48 +0200 |
wenzelm |
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 22:26:53 +0200 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 21:39:08 +0200 |
wenzelm |
inform_file_processed: Isar.init_point last!
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 19:57:13 +0200 |
wenzelm |
inform_file_processed: try harder not to fail, ensure
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 17:51:44 +0200 |
wenzelm |
proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
|
file |
diff |
annotate
|
Thu, 10 Jul 2008 21:12:34 +0200 |
wenzelm |
restart: Isar.init_point;
|
file |
diff |
annotate
|
Thu, 10 Jul 2008 21:03:47 +0200 |
wenzelm |
proper_inform_file_processed: Isar.init_point starts fresh command sequence;
|
file |
diff |
annotate
|
Thu, 10 Jul 2008 20:54:00 +0200 |
wenzelm |
activated new versions of undo, kill_proof;
|
file |
diff |
annotate
|
Thu, 10 Jul 2008 20:03:30 +0200 |
wenzelm |
added ProofGeneral.isar_kill_proof;
|
file |
diff |
annotate
|
Thu, 17 Apr 2008 16:30:52 +0200 |
wenzelm |
replaced token translations by common markup;
|
file |
diff |
annotate
|
Mon, 14 Apr 2008 14:28:47 +0200 |
wenzelm |
Isar.toplevel_loop: separate init/welcome flag;
|
file |
diff |
annotate
|
Thu, 10 Apr 2008 14:53:29 +0200 |
wenzelm |
ThyInfo.get_names;
|
file |
diff |
annotate
|
Thu, 10 Apr 2008 13:44:43 +0200 |
wenzelm |
replaced Isar loop variants by generic toplevel_loop;
|
file |
diff |
annotate
|
Thu, 03 Apr 2008 21:23:41 +0200 |
wenzelm |
moved test_markup here;
|
file |
diff |
annotate
|
Thu, 03 Apr 2008 18:42:40 +0200 |
wenzelm |
XML.output_markup;
|
file |
diff |
annotate
|
Thu, 03 Apr 2008 16:03:56 +0200 |
wenzelm |
Symbol.SOH;
|
file |
diff |
annotate
|
Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
Wed, 05 Mar 2008 22:58:12 +0100 |
wenzelm |
IsabelleProcess.output_markup;
|
file |
diff |
annotate
|
Sun, 06 Jan 2008 15:57:56 +0100 |
wenzelm |
replaced prompt markup by prompt channel setup;
|
file |
diff |
annotate
|
Sun, 30 Dec 2007 23:07:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 14 Dec 2007 21:15:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 06 Dec 2007 00:21:32 +0100 |
wenzelm |
moved basic test_markup to isabelle_process.ML;
|
file |
diff |
annotate
|
Mon, 19 Nov 2007 11:09:09 +0100 |
wenzelm |
inform_file_processed: made even more robust against bad file specs;
|
file |
diff |
annotate
|
Sun, 18 Nov 2007 16:10:12 +0100 |
wenzelm |
removed unused inform_file_processed;
|
file |
diff |
annotate
|
Thu, 15 Nov 2007 11:49:04 +0100 |
wenzelm |
thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
|
file |
diff |
annotate
|
Thu, 25 Oct 2007 16:57:57 +0200 |
wenzelm |
made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);
|
file |
diff |
annotate
|
Sat, 06 Oct 2007 22:31:57 +0200 |
wenzelm |
removed obsolete write_keywords;
|
file |
diff |
annotate
|
Sat, 06 Oct 2007 21:21:45 +0200 |
wenzelm |
export init_outer_syntax;
|
file |
diff |
annotate
|
Sat, 06 Oct 2007 17:53:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
Fri, 07 Sep 2007 22:13:45 +0200 |
wenzelm |
added hilite markup;
|
file |
diff |
annotate
|
Sun, 19 Aug 2007 12:43:05 +0200 |
aspinall |
Use 376/377 specials for sendback markup
|
file |
diff |
annotate
|
Wed, 15 Aug 2007 19:24:23 +0200 |
wenzelm |
added sendback;
|
file |
diff |
annotate
|
Mon, 13 Aug 2007 18:10:22 +0200 |
wenzelm |
Lexicon.read_indexname/nat/variable;
|
file |
diff |
annotate
|
Tue, 31 Jul 2007 00:56:32 +0200 |
wenzelm |
ThyInfo.register_thy;
|
file |
diff |
annotate
|
Sun, 22 Jul 2007 21:20:58 +0200 |
wenzelm |
inform_file_processed: tuned msg, no state;
|
file |
diff |
annotate
|
Tue, 10 Jul 2007 16:45:05 +0200 |
wenzelm |
removed no_state markup -- produce empty state;
|
file |
diff |
annotate
|
Mon, 09 Jul 2007 11:44:23 +0200 |
wenzelm |
simplified writeln_fn;
|
file |
diff |
annotate
|
Sat, 07 Jul 2007 18:39:21 +0200 |
wenzelm |
toplevel prompt/print_state: proper markup, removed hooks;
|
file |
diff |
annotate
|
Sat, 07 Jul 2007 00:15:02 +0200 |
wenzelm |
simplified pretty token metric: type int;
|
file |
diff |
annotate
|
Sun, 15 Apr 2007 14:31:59 +0200 |
wenzelm |
removed unused Output.panic hook -- internal to PG wrapper;
|
file |
diff |
annotate
|
Sat, 14 Apr 2007 17:36:05 +0200 |
wenzelm |
Term.string_of_vname;
|
file |
diff |
annotate
|
Wed, 04 Apr 2007 00:11:23 +0200 |
wenzelm |
removed unused info channel;
|
file |
diff |
annotate
|
Thu, 01 Feb 2007 20:40:34 +0100 |
wenzelm |
proper use of PureThy.has_name_hint instead of hard-wired string'';
|
file |
diff |
annotate
|
Wed, 31 Jan 2007 20:07:40 +0100 |
aspinall |
Fix tell_thm_deps to match changse in PureThy.
|
file |
diff |
annotate
|
Mon, 22 Jan 2007 15:34:15 +0100 |
aspinall |
Comment
|
file |
diff |
annotate
|
Thu, 04 Jan 2007 19:27:08 +0100 |
wenzelm |
broken error handling for command syntax -- reverted to revision 1.9;
|
file |
diff |
annotate
|
Thu, 04 Jan 2007 11:56:53 +0100 |
haftmann |
eliminated Option.app
|
file |
diff |
annotate
|
Wed, 03 Jan 2007 22:59:30 +0100 |
aspinall |
Fix error reporting in Emacs to also match Isar command failure exactly.
|
file |
diff |
annotate
|
Sat, 30 Dec 2006 16:20:32 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
Sat, 30 Dec 2006 16:08:09 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
Sat, 30 Dec 2006 12:33:29 +0100 |
wenzelm |
inform_file_processed: Toplevel.init_empty;
|
file |
diff |
annotate
|
Fri, 29 Dec 2006 19:50:50 +0100 |
wenzelm |
removed obsolete init_pgip;
|
file |
diff |
annotate
|
Fri, 29 Dec 2006 18:46:06 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 29 Dec 2006 18:25:46 +0100 |
wenzelm |
minor tuning;
|
file |
diff |
annotate
|
Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
Tue, 05 Dec 2006 13:56:43 +0100 |
aspinall |
Support PGIP communication for preferences in Emacs mode.
|
file |
diff |
annotate
|
Mon, 04 Dec 2006 22:12:08 +0100 |
aspinall |
Add separate PG Emacs configuration
|
file |
diff |
annotate
|