From 562fe97c4e506cf7f748d58c0e877359c0623b3e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 1 Jul 2002 00:27:43 +0000 Subject: Doc difference between isa and isar, fix prob with isa support. --- isa/x-symbol-isabelle.el | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el index 2c834b9b..94a5f095 100644 --- a/isa/x-symbol-isabelle.el +++ b/isa/x-symbol-isabelle.el @@ -10,6 +10,12 @@ ;; ;; NB: Part of Proof General distribution. ;; +;; This file accounts for differences between Isabelle and +;; Isabelle/Isar support of X-Symbol tokens, namely: +;; +;; Isabelle: \\ (inside ML strings) +;; Isabelle/Isar: \ +;; (defvar x-symbol-isabelle-required-fonts nil) @@ -60,12 +66,19 @@ See `x-symbol-header-groups-alist'." :encode-spec '(((id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) . ((id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]"))) :decode-spec nil - :decode-regexp "\\\\<[A-Za-z]+>\\|[A-Za-z_][A-Za-z_0-9]+\\|[<>!+-*/|&]+" + :decode-regexp + (concat + (if (eq proof-assistant-symbol 'isa) + "\\\\?") ; match an extra backquote in input strings, + ;; but not used in output strings. + ;; FIXME: is this right?? + "\\\\<[A-Za-z]+>\\|[A-Za-z_][A-Za-z_0-9]+\\|[<>!+-*/|&]+") :token-list #'x-symbol-isabelle-default-token-list)) (defvar x-symbol-isabelle-input-token-grammar '("\\(?:\\<[A-Za-z]+>\\|[A-Za-z_][A-Za-z_0-9]+\\|[<>!+-*/|&]+\\)\\'" - (id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) + (id . "[A-Za-z_0-9]") + (op . "[<>!+-*/|&]")) "Grammar of input method Token for language `isabelle'."))) (defun x-symbol-isabelle-default-token-list (tokens) -- cgit v1.2.3