From acc622e1fcca27be821f9acf03fdfb8adc42dcd3 Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Thu, 28 Dec 2000 17:49:32 +0000 Subject: include x-symbol-isabelle-font-lock-keywords in shell/goals/response buffers; more robust \<^sync>; --- isar/isar.el | 26 +++++++++++--------------- 1 file changed, 11 insertions(+), 15 deletions(-) (limited to 'isar/isar.el') diff --git a/isar/isar.el b/isar/isar.el index d9e7e7a2..a1356705 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -25,9 +25,13 @@ (require 'proof) (require 'isar-syntax) +;; Completion table for Isabelle/Isar identifiers +(defpgdefault completion-table isar-keywords-major) + ;; Add generic code for Isabelle and Isabelle/Isar (setq load-path (cons (concat proof-home-directory "isa/") load-path)) (require 'isabelle-system) +(require 'x-symbol-isabelle) (defcustom isar-web-page "http://isabelle.in.tum.de/Isar/" @@ -489,7 +493,7 @@ proof-shell-retract-files-regexp." ;; (format "ML_command {* %s *};" string) ;; string) string - "\\<^sync>;")))) + " \\<^sync>;")))) (defun isar-mode-config () (isar-mode-config-set-variables) @@ -502,16 +506,17 @@ proof-shell-retract-files-regexp." (add-hook 'proof-pre-shell-start-hook 'isar-pre-shell-start nil t) (add-hook 'proof-shell-insert-hook 'isar-preprocessing)) - (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-keywords-1) + (setq font-lock-keywords ;FIXME handle x-symbol stuff by generic code!? + (append isar-output-font-lock-keywords-1 x-symbol-isabelle-font-lock-keywords)) (isar-shell-mode-config-set-variables) (proof-shell-config-done)) (defun isar-response-mode-config () - (setq font-lock-keywords isar-output-font-lock-keywords-1) + (setq font-lock-keywords ;FIXME handle x-symbol stuff by generic code!? + (append isar-output-font-lock-keywords-1 x-symbol-isabelle-font-lock-keywords)) (isar-init-output-syntax-table) (proof-response-config-done)) @@ -520,7 +525,8 @@ 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-goals-font-lock-keywords) + (setq font-lock-keywords ;FIXME handle x-symbol stuff by generic code!? + (append isar-goals-font-lock-keywords x-symbol-isabelle-font-lock-keywords)) (proof-goals-config-done)) @@ -538,14 +544,4 @@ proof-shell-retract-files-regexp." (isar-markup-ml "print_mode := (! print_mode \\\\ [\"xsymbols\",\"symbols\"])")) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Completion table for Isabelle/Isar identifiers -;; -;; Ideally this could be set and adjusted automatically from the -;; running process. - -(defpgdefault completion-table isar-keywords-major) - - (provide 'isar) -- cgit v1.2.3