src/Pure/proof_general.ML
2005-09-30 aspinall 2005-09-30 Move welcomemsg and helpdoc to pgip_isar.xml
2005-09-30 aspinall 2005-09-30 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
2005-09-20 webertj 2005-09-20 undone the previous change: show_hyps not supported anymore
2005-09-20 webertj 2005-09-20 new menu item show-sort-hypotheses to toggle show_hyps
2005-09-17 wenzelm 2005-09-17 tuned comments;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update; nat_option trace_simp_depth_limit;
2005-09-15 aspinall 2005-09-15 Revert previous attribute name change, problem can be avoided in JAXB.
2005-09-15 aspinall 2005-09-15 Change PGIP attribute name class->messageclass to avoid Java keyword clash.
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-09-01 wenzelm 2005-09-01 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z; tuned;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-03 berghofe 2005-08-03 Adapted to new interface of thms_of_proof.
2005-07-29 wenzelm 2005-07-29 P.opt_locale_target;
2005-07-20 aspinall 2005-07-20 Ressurect seq attribute accidently removed
2005-07-14 haftmann 2005-07-14 (fix for smlnj)
2005-07-13 aspinall 2005-07-13 Update PGIP packet handling, fixing unique session identifier.
2005-07-13 wenzelm 2005-07-13 tuned msg;
2005-07-13 aspinall 2005-07-13 Add acceptedpgipelems message
2005-07-13 aspinall 2005-07-13 Add management for current working directory
2005-07-13 aspinall 2005-07-13 Note about theorem dependencies including themselves.
2005-07-13 aspinall 2005-07-13 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
2005-06-22 wenzelm 2005-06-22 tuned;
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 Context.theory_name; tuned;
2005-06-05 wenzelm 2005-06-05 File.platform_path;
2005-05-22 wenzelm 2005-05-22 FindTheorems.print_theorems;
2005-05-17 wenzelm 2005-05-17 var_or_skolem: always print question mark for vars stemming from skolems;
2005-05-17 wenzelm 2005-05-17 renamed show_var_qmarks to show_question_marks; var_or_skolem: proper treatment of show_question_marks via Syntax.read_variable;
2005-05-16 kleing 2005-05-16 searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-03-25 aspinall 2005-03-25 Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
2005-03-25 aspinall 2005-03-25 Support new PGIP commands redostep, redoitem
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-27 berghofe 2005-01-27 Added show_var_qmarks flag.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-12-13 aspinall 2004-12-13 Fix pgmlsymbolson/off.
2004-12-10 aspinall 2004-12-10 Support PGIP <whitespace>, <dostep>, <doitem> elements as input
2004-12-10 aspinall 2004-12-10 Insert pgmltext element into responses in PGIP mode
2004-11-16 aspinall 2004-11-16 Markup obtain as introducing a nested goal.
2004-11-15 aspinall 2004-11-15 Add <undoitem> for theory-state undos.
2004-10-28 aspinall 2004-10-28 Make <undostep> call undos_proof to display resulting proofstate.
2004-10-27 aspinall 2004-10-27 Revert change to pgml_sym
2004-10-24 aspinall 2004-10-24 Simplification to symbol processing; put quotes around theory name in message.
2004-10-21 aspinall 2004-10-21 Fix <closetheory>
2004-10-11 berghofe 2004-10-11 Added entry in Settings menu for Toplevel.skip_proofs flag.
2004-10-02 aspinall 2004-10-02 Add openblock/closeblock to other opengoal/closegoal elements
2004-10-01 aspinall 2004-10-01 Comments
2004-09-28 aspinall 2004-09-28 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
2004-09-27 aspinall 2004-09-27 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
2004-09-08 aspinall 2004-09-08 Tweak parentnames attribute on opentheory
2004-09-08 aspinall 2004-09-08 Support parsing of -- {* comments *}. Add extra output channels.
2004-09-03 aspinall 2004-09-03 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
2004-08-23 berghofe 2004-08-23 Adapted to new interface of function ThyLoad.check_file
2004-08-19 aspinall 2004-08-19 Add systemcmd.
2004-08-19 aspinall 2004-08-19 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
2004-08-18 aspinall 2004-08-18 Version for PGIP 2.X, with greatly improved parsing and XML handling.
2004-08-16 aspinall 2004-08-16 Experimental version supporting PGIP, merged with main branch with help from Makarius.
2004-06-29 kleing 2004-06-29 license change to BSD