diff options
| author | Makarius Wenzel | 2011-07-06 19:21:10 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2011-07-06 19:21:10 +0000 |
| commit | 6d8943cef5aba5364adafd029b7d74a5a7f8391e (patch) | |
| tree | 073e8a53fa62f7b860b78c6fa196cdb9e092f6bf /pgshell | |
| parent | 63e733181007056be5c252e4e42b371fc3f09ac9 (diff) | |
generalized font-lock regexps: isar-text allows any non-control characters to be marked up (e.g. notation for "free" and "skolem" variables after Isabelle2011);
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions