src/Pure/ProofGeneral/proof_general_pgip.ML
2008-06-25 wenzelm 2008-06-25 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-12 wenzelm 2008-06-12 sane versions of (qualified_)thms_of_thy;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-18 wenzelm 2008-04-18 removed dead code;
2008-04-17 wenzelm 2008-04-17 replaced token translations by common markup;
2008-04-10 wenzelm 2008-04-10 simplified isarcmd;
2008-04-10 wenzelm 2008-04-10 ThyInfo.get_names;
2008-04-10 wenzelm 2008-04-10 moved global Toplevel state to structure Isar;
2008-04-03 wenzelm 2008-04-03 renamed XML.parse_comment_whspc to XML.parse_comments;
2008-04-03 wenzelm 2008-04-03 further cleanup of XML signature;
2008-04-03 wenzelm 2008-04-03 XML.string_of, XML.parse;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-02-21 wenzelm 2008-02-21 more elaborate structure Distribution (filled-in by makedist);
2008-01-06 wenzelm 2008-01-06 removed obsolete prompt markup;
2007-11-19 aspinall 2007-11-19 Init outer syntax after message setup to avoid spurious output.
2007-11-04 wenzelm 2007-11-04 removed obsolete ProofGeneral/parsing.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.