Sun, 22 Jul 2007 21:20:58 +0200 |
wenzelm |
inform_file_processed: tuned msg, no state;
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 17:54:15 +0200 |
wenzelm |
simplified ThyLoad interfaces: only one additional directory;
|
file |
diff |
annotate
|
Thu, 19 Jul 2007 23:18:55 +0200 |
wenzelm |
adapted ThyLoad.deps_thy
|
file |
diff |
annotate
|
Wed, 18 Jul 2007 14:44:49 +0200 |
aspinall |
Direct priority and tracing channels properly.
|
file |
diff |
annotate
|
Tue, 17 Jul 2007 16:14:42 +0200 |
wenzelm |
avoid redundant variables in patterns (which made Alice vomit);
|
file |
diff |
annotate
|
Thu, 12 Jul 2007 00:15:39 +0200 |
wenzelm |
simplified using Markup.get_int;
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:35:17 +0200 |
aspinall |
Fix nested PGIP messages. Update for schema simplifications.
|
file |
diff |
annotate
|
Tue, 10 Jul 2007 23:29:49 +0200 |
wenzelm |
renamed XML.Rawtext to XML.Output;
|
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 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
|