Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | -w false implies -x false; | Makarius Wenzel | 2000-08-28 |
| | | | | do not load proof-site.el here; | ||
* | isar-keywords-proof-improper; | Makarius Wenzel | 2000-08-16 |
| | |||
* | added isar-keywords-proof-improper; | Makarius Wenzel | 2000-08-16 |
| | | | | tuned; | ||
* | added outline mode setup (still not quite working as expected); | Makarius Wenzel | 2000-08-07 |
| | |||
* | cleaned up outline stuff; | Makarius Wenzel | 2000-08-07 |
| | |||
* | new category isar-keywords-proof-heading; | Makarius Wenzel | 2000-08-07 |
| | |||
* | ** B make help key bindings appear in "Show me ..." menu; | Makarius Wenzel | 2000-08-03 |
| | |||
* | added isar-help functions / keys (how do I get keys into menus?); | Makarius Wenzel | 2000-08-03 |
| | |||
* | fixed isar-goals-font-lock-keywords; | Makarius Wenzel | 2000-07-29 |
| | |||
* | added "thm_deps", "overloaded"; | Makarius Wenzel | 2000-07-29 |
| | |||
* | use ML_command to avoid unwanted output; | Makarius Wenzel | 2000-07-19 |
| | |||
* | proof-prog-name: use isabelle-command-line; | Makarius Wenzel | 2000-07-08 |
| | | | | removed misc junk; | ||
* | tuned help-menu-entries; | Makarius Wenzel | 2000-07-06 |
| | |||
* | improved help menu; | Makarius Wenzel | 2000-07-01 |
| | | | | replaced "help" by "welcome"; | ||
* | removed 'help'; | Makarius Wenzel | 2000-07-01 |
| | | | | added 'print_antiquotations', 'print_commands', 'print_trans_rules'; | ||
* | added method_setup; | Makarius Wenzel | 2000-06-30 |
| | |||
* | Note about typing in shell buffer | David Aspinall | 2000-06-27 |
| | |||
* | Tidy | David Aspinall | 2000-06-27 |
| | |||
* | Extra note. | David Aspinall | 2000-06-22 |
| | |||
* | proper function-menu (fume) setup; | Makarius Wenzel | 2000-06-16 |
| | |||
* | Tuned x-symbol config, moved settings to isabelle-system.el | David Aspinall | 2000-06-16 |
| | |||
* | Deleted files. | David Aspinall | 2000-06-16 |
| | |||
* | Note to merge | David Aspinall | 2000-06-15 |
| | |||
* | new indentation setup; | Makarius Wenzel | 2000-06-10 |
| | |||
* | proof-shell-error-regexp; | Makarius Wenzel | 2000-06-09 |
| | |||
* | new indentation setup; | Makarius Wenzel | 2000-06-08 |
| | | | | completion-table: use isar-keywords-major; | ||
* | new indentation setup; | Makarius Wenzel | 2000-06-08 |
| | |||
* | isar-keywords-proof-open/close; | Makarius Wenzel | 2000-06-08 |
| | |||
* | proper indentation; | Makarius Wenzel | 2000-06-08 |
| | |||
* | Failed attempted hack to support ML files in isar mode (see comments in ↵ | David Aspinall | 2000-06-07 |
| | | | | isar-preprocessing). | ||
* | Allowed ; to terminate a command by including it in regexp for cmdstart | David Aspinall | 2000-06-06 |
| | | | | Added completion for Isar keywords and X-symbol token names. | ||
* | isar-save-with-hole-regexp: proof-no-regexp; | Makarius Wenzel | 2000-06-05 |
| | |||
* | proof-indent-commands-regexp: use proof-no-regexp; | Makarius Wenzel | 2000-06-05 |
| | | | | | isar-global-save-command-p: more robust wrt. empty prev span (malformed!?); isar-preprocessing: fixed terminator regexp; | ||
* | Removed defunct comments | David Aspinall | 2000-06-05 |
| | |||
* | Temporary bug fix to solve nil span error message | David Aspinall | 2000-06-05 |
| | |||
* | replaced isar-verbatim by isabelle-verbatim; | Makarius Wenzel | 2000-06-04 |
| | | | | added isar-strip-terminators; | ||
* | updated; | Makarius Wenzel | 2000-06-04 |
| | |||
* | replaced isar-verbatim by isabelle-verbatim; | Makarius Wenzel | 2000-06-04 |
| | | | | fixed output syntax table; | ||
* | { } are back; | Makarius Wenzel | 2000-06-03 |
| | |||
* | Removed now spurious semicolons, 8-). | David Aspinall | 2000-06-01 |
| | |||
* | Temporarily removed keywords { and } for new parsing mechanism | David Aspinall | 2000-06-01 |
| | |||
* | Remove setting of proof-segment-up-to | David Aspinall | 2000-06-01 |
| | |||
* | improved isar-goals-font-lock-keywords; | Makarius Wenzel | 2000-05-30 |
| | |||
* | isar-preprocessing inserts final terminator if none there. | David Aspinall | 2000-05-30 |
| | | | | | Added (defpgdefault script-indent t) to turn on indentation. Added proof-script-command-start-regexp setting. | ||
* | Tweak font lock exprs enough for Example.thy | David Aspinall | 2000-05-29 |
| | |||
* | Font lock exprs for goals buffer like those in Isabelle | David Aspinall | 2000-05-29 |
| | |||
* | Set settings format function before calculating initial command. Add hilit ↵ | David Aspinall | 2000-05-29 |
| | | | | for goals buffer | ||
* | Use generic default setting mechanism now. Add isar-markup-ml here. | David Aspinall | 2000-05-29 |
| | |||
* | Add -*- isar -*- tag to force mode, and comment to explain. | David Aspinall | 2000-05-29 |
| | |||
* | isar-any-command-regexp; | Makarius Wenzel | 2000-05-26 |
| |