diff options
| author | Makarius Wenzel | 1999-09-30 13:39:28 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-09-30 13:39:28 +0000 |
| commit | 60c38f7adc882dc845ce19caa862355a095de142 (patch) | |
| tree | 8f931a9f73facb496a0d75d9249508168c01454a | |
| parent | 660718457f3e99150b281504f9bfdaaeff5fcc33 (diff) | |
proof-find-theorems-command "thms_containing %s;";
proof-shell-leave-annotations-in-output t;
replaced isar-output-font-lock-terms by isar-output-font-lock-keywords-1;
| -rw-r--r-- | isar/isar.el | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/isar/isar.el b/isar/isar.el index fc971fa2..0b01bd34 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -164,6 +164,7 @@ proof-ctxt-string "print_context" proof-help-string "help" proof-kill-goal-command "kill_proof;" + proof-find-theorems-command "thms_containing %s;" ;; command hooks proof-goal-command-p 'isar-goal-command-p proof-really-save-command-p 'isar-global-save-command-p @@ -224,6 +225,10 @@ ;; "^---\\|^\\[opening " ;; could be last bracket on end of line, or with ### and ***. + ;; Dirty hack to allow font-locking for output based on hidden + ;; annotations, see isar-output-font-lock-keywords-1 + proof-shell-leave-annotations-in-output t + ;; === ANNOTATIONS === ones below here are broken proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" @@ -521,13 +526,13 @@ proof-shell-retract-files-regexp." (defun isar-shell-mode-config () "Configure Proof General proof shell for Isabelle/Isar." (isar-init-output-syntax-table) - (setq font-lock-keywords isar-output-font-lock-terms) + (setq font-lock-keywords isar-output-font-lock-keywords-1) (isar-shell-mode-config-set-variables) (proof-shell-config-done) (isar-outline-setup)) (defun isar-response-mode-config () - (setq font-lock-keywords isar-output-font-lock-terms) + (setq font-lock-keywords isar-output-font-lock-keywords-1) (isar-init-output-syntax-table) (isar-outline-setup) (proof-response-config-done)) @@ -537,7 +542,7 @@ proof-shell-retract-files-regexp." (setq pbp-change-goal "Show %s.") (setq pbp-error-regexp proof-shell-error-regexp) (isar-init-output-syntax-table) - (setq font-lock-keywords isar-output-font-lock-terms) + (setq font-lock-keywords isar-output-font-lock-keywords-1) (isar-outline-setup) (proof-goals-config-done)) |