src/Pure/ProofGeneral/proof_general_pgip.ML
2007-11-04 wenzelm 2007-11-04 activated new script parser;
2007-10-29 wenzelm 2007-10-29 qualified Proofterm.proofs;
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-17 wenzelm 2007-09-17 change print_mode: CRITICAL;
2007-08-13 wenzelm 2007-08-13 Lexicon.read_indexname/nat/variable;
2007-08-08 wenzelm 2007-08-08 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
2007-07-31 wenzelm 2007-07-31 ThyInfo.register_thy;
2007-07-29 wenzelm 2007-07-29 adapted ThyLoad.deps_thy;
2007-07-22 wenzelm 2007-07-22 inform_file_processed: tuned msg, no state;
2007-07-20 wenzelm 2007-07-20 simplified ThyLoad interfaces: only one additional directory;
2007-07-19 wenzelm 2007-07-19 adapted ThyLoad.deps_thy
2007-07-18 aspinall 2007-07-18 Direct priority and tracing channels properly.
2007-07-17 wenzelm 2007-07-17 avoid redundant variables in patterns (which made Alice vomit);
2007-07-12 wenzelm 2007-07-12 simplified using Markup.get_int; renamed PgipParser to OldPgipParser;
2007-07-11 aspinall 2007-07-11 Fix nested PGIP messages. Update for schema simplifications.
2007-07-10 wenzelm 2007-07-10 renamed XML.Rawtext to XML.Output;
2007-07-10 wenzelm 2007-07-10 removed no_state markup -- produce empty state; Markup.add_mode;
2007-07-09 wenzelm 2007-07-09 tuned dead code;
2007-07-07 wenzelm 2007-07-07 toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07 wenzelm 2007-07-07 simplified pretty token metric: type int; separate print_mode setup for Output/Pretty;
2007-07-06 aspinall 2007-07-06 Produce good PGML 2.0
2007-06-20 aspinall 2007-06-20 Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
2007-06-03 wenzelm 2007-06-03 removed obsolete Library.seq;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-04-15 wenzelm 2007-04-15 removed unused Output.panic hook -- internal to PG wrapper;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-04-04 wenzelm 2007-04-04 removed unused info channel; renamed Output.has_mode to print_mode_active; cleaned-up Output functions;
2007-03-03 aspinall 2007-03-03 Simplify print mode. Support setproverflag.
2007-03-03 aspinall 2007-03-03 Fix idvalue output and PGML print mode raw encode/decode.
2007-02-17 aspinall 2007-02-17 Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
2007-02-06 aspinall 2007-02-06 askids/qualified_thms_of_thy: version which returns names in domain of get_thm
2007-02-05 wenzelm 2007-02-05 proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);
2007-02-01 wenzelm 2007-02-01 proper use of PureThy.has_name_hint instead of hard-wired string'';
2007-01-31 aspinall 2007-01-31 Fix tell_thm_deps to match changse in PureThy.
2007-01-30 aspinall 2007-01-30 Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
2007-01-24 aspinall 2007-01-24 Let <loadfile> execute even while a file is open interactively.
2007-01-22 aspinall 2007-01-22 Expose currently open file
2007-01-22 aspinall 2007-01-22 Comment
2007-01-09 aspinall 2007-01-09 Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
2007-01-07 aspinall 2007-01-07 Be more chatty in PGIP file operations.
2007-01-05 wenzelm 2007-01-05 removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
2007-01-04 aspinall 2007-01-04 Use warning fatality
2007-01-04 haftmann 2007-01-04 eliminated Option.app
2007-01-03 aspinall 2007-01-03 Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
2006-12-31 aspinall 2006-12-31 Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
2006-12-30 wenzelm 2006-12-30 removed dead code;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator; avoid handle _; showctxt: print_context (cf. local theory context); searchtheorems: proper find_theorems; refrain from setting ml_prompts again; tuned init_pgip;
2006-12-30 wenzelm 2006-12-30 inform_file_processed: Toplevel.init_empty;
2006-12-29 wenzelm 2006-12-29 removed obsolete context_thy etc.;
2006-12-29 wenzelm 2006-12-29 minor tuning;
2006-12-27 haftmann 2006-12-27 made SML/NJ happy
2006-12-19 aspinall 2006-12-19 Remove obsolete prefixes from error and warning messages.
2006-12-17 aspinall 2006-12-17 Add abstraction for objtypes and documents.
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 aspinall 2006-12-05 Document structure in pgip_markup.ML. Minor fixes.
2006-12-05 aspinall 2006-12-05 Support PGIP communication for preferences in Emacs mode.
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-12-04 aspinall 2006-12-04 Add separate PG Emacs configuration
2006-12-04 aspinall 2006-12-04 Revamped Proof General interface.