| 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
|