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