| Tue, 10 Jul 2007 16:45:05 +0200 |
wenzelm |
removed no_state markup -- produce empty state;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 23:12:51 +0200 |
wenzelm |
tuned dead code;
|
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
|
| Fri, 06 Jul 2007 17:52:52 +0200 |
aspinall |
Produce good PGML 2.0
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 15:10:02 +0200 |
aspinall |
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:54 +0200 |
wenzelm |
removed obsolete Library.seq;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
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
|
| Sat, 03 Mar 2007 12:56:06 +0100 |
aspinall |
Simplify print mode. Support setproverflag.
|
file |
diff |
annotate
|
| Sat, 03 Mar 2007 00:16:09 +0100 |
aspinall |
Fix idvalue output and PGML print mode raw encode/decode.
|
file |
diff |
annotate
|
| Sat, 17 Feb 2007 18:00:59 +0100 |
aspinall |
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 12:54:55 +0100 |
aspinall |
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
|
file |
diff |
annotate
|
| Mon, 05 Feb 2007 12:03:52 +0100 |
wenzelm |
proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);
|
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
|
| Tue, 30 Jan 2007 13:17:02 +0100 |
aspinall |
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
|
file |
diff |
annotate
|
| Wed, 24 Jan 2007 13:15:16 +0100 |
aspinall |
Let <loadfile> execute even while a file is open interactively.
|
file |
diff |
annotate
|
| Mon, 22 Jan 2007 16:52:02 +0100 |
aspinall |
Expose currently open file
|
file |
diff |
annotate
|
| Mon, 22 Jan 2007 15:34:15 +0100 |
aspinall |
Comment
|
file |
diff |
annotate
|
| Tue, 09 Jan 2007 12:12:00 +0100 |
aspinall |
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
|
file |
diff |
annotate
|
| Sun, 07 Jan 2007 14:05:44 +0100 |
aspinall |
Be more chatty in PGIP file operations.
|
file |
diff |
annotate
|
| Fri, 05 Jan 2007 14:30:08 +0100 |
wenzelm |
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 18:09:58 +0100 |
aspinall |
Use warning fatality
|
file |
diff |
annotate
|
| Thu, 04 Jan 2007 11:56:53 +0100 |
haftmann |
eliminated Option.app
|
file |
diff |
annotate
|
| Wed, 03 Jan 2007 21:11:42 +0100 |
aspinall |
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
|
file |
diff |
annotate
|
| Sun, 31 Dec 2006 14:55:35 +0100 |
aspinall |
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:20:32 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:10 +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:51 +0100 |
wenzelm |
removed obsolete context_thy etc.;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2006 18:25:46 +0100 |
wenzelm |
minor tuning;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 16:18:07 +0100 |
haftmann |
made SML/NJ happy
|
file |
diff |
annotate
|
| Tue, 19 Dec 2006 16:58:30 +0100 |
aspinall |
Remove obsolete prefixes from error and warning messages.
|
file |
diff |
annotate
|
| Sun, 17 Dec 2006 22:43:50 +0100 |
aspinall |
Add abstraction for objtypes and documents.
|
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 22:04:24 +0100 |
aspinall |
Document structure in pgip_markup.ML. Minor fixes.
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 13:56:43 +0100 |
aspinall |
Support PGIP communication for preferences in Emacs mode.
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2006 22:12:08 +0100 |
aspinall |
Add separate PG Emacs configuration
|
file |
diff |
annotate
|
| Mon, 04 Dec 2006 20:40:11 +0100 |
aspinall |
Revamped Proof General interface.
|
file |
diff |
annotate
|