diff options
-rw-r--r-- | generic/proof-syntax.el | 19 | ||||
-rw-r--r-- | generic/proof.el | 83 | ||||
-rw-r--r-- | lego/lego-syntax.el | 5 | ||||
-rw-r--r-- | lego/lego.el | 10 |
4 files changed, 69 insertions, 48 deletions
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 651c3578..cfaae0c4 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -71,12 +71,19 @@ (copy-face 'bold 'font-lock-tacticals-name-face))) (defvar font-lock-error-face -(if (proof-have-color) - (let ((face (make-face 'font-lock-error-face))) - (dont-compile - (set-face-foreground face "red")) - face) - (copy-face 'bold 'font-lock-error-face))) + (let ((face (make-face 'font-lock-error-face))) + (copy-face 'bold 'font-lock-error-face) + (and (proof-have-color) (set-face-background face "salmon1")) + face) + "*The face for error messages.") + +(defvar font-lock-eager-annotation-face + (let ((face (make-face 'font-lock-eager-annotation-face))) + (if (proof-have-color) + (set-face-background face "lemon chiffon") + (copy-face 'italic face)) + face) + "*The face for urgent messages.") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; A big hack to unfontify commas in declarations and definitions. ;; diff --git a/generic/proof.el b/generic/proof.el index f125bfce..08826da5 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -264,6 +264,10 @@ an error.") ;; A couple of small utilities ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun proof-message (str) + "Output STR in minibuffer." + (message (concat "[Proof] " str))) + ;; append-element in tl-list (defun proof-append-element (ls elt) "Append ELT to last of LS if ELT is not nil. [proof.el] @@ -332,7 +336,6 @@ an error.") (span-read-only proof-queue-span) (make-face 'proof-queue-face) - ;; Whether display has color or not (cond ((proof-have-color) (set-face-background 'proof-queue-face "mistyrose")) (t (progn @@ -350,7 +353,6 @@ an error.") (span-read-only proof-locked-span) (make-face 'proof-locked-face) - ;; Whether display has color or not (cond ((proof-have-color) (set-face-background 'proof-locked-face "lavender")) (t (set-face-property 'proof-locked-face 'underline t))) @@ -777,6 +779,28 @@ Set to nil if the proof to disable this feature.") (incf ip)) (substring out 0 op))) +(defun proof-shell-handle-output (start-regexp end-regexp append-face) + "Pretty print output in PROCESS buffer in specified region. +Removes any annotations in the region. +Appends APPEND-FACE to the text property of the region . +Returns the string in the specified region." + (let ((string)) + (save-excursion + (set-buffer proof-shell-buffer) + (goto-char (point-max)) + (let* ((end (search-backward-regexp end-regexp)) + (start (search-backward-regexp start-regexp))) + (setq string + (proof-shell-strip-annotations (buffer-substring start end))) + (delete-region start end) + (insert string) + (setq end (+ start (length string))) + (font-lock-fontify-region start end) + (font-lock-append-text-property start end 'face append-face) + + ;;FIXME: Why are faces not preserved? + (buffer-substring start end))))) + (defun proof-shell-handle-delayed-output () (let ((ins (car proof-shell-delayed-output)) (str (cdr proof-shell-delayed-output))) @@ -799,30 +823,19 @@ Set to nil if the proof to disable this feature.") "React on an error message triggered by the prover. [proof.el] We display the process buffer, scroll to the end, beep and fontify the error message. At the end it calls `proof-shell-handle-error-hook'. " - (save-excursion - (display-buffer (set-buffer proof-shell-buffer)) - - (goto-char (point-max)) - (let* ((end (search-backward-regexp proof-shell-annotated-prompt-regexp)) - (start (search-backward-regexp proof-shell-error-regexp)) - (string - (proof-shell-strip-annotations (buffer-substring start end)))) - - - - (beep) - - ;; fontification - - ;; remove annotations (otherwise font-lock expressions do not match) - - (delete-region start end) - (insert string) - (setq end (+ start (length string))) - (font-lock-fontify-region start end) - (font-lock-fillin-text-property start end 'face 'font-lock - 'font-lock-error-face) - )) + ;; We extract all text between text matching + ;; `proof-shell-error-regexp' and the following prompt. + ;; Alternatively one could higlight all output between the + ;; previous and the current prompt. + ;; +/- of our approach + ;; + Previous not so relevent output is not highlighted + ;; - Proof systems have to conform to error messages whose start can be + ;; detected by a regular expression. + (proof-shell-handle-output + proof-shell-error-regexp proof-shell-annotated-prompt-regexp + 'font-lock-error-face) + (save-excursion (display-buffer proof-shell-buffer)) + (beep) ;; unwind script buffer (set-buffer proof-script-buffer) @@ -1054,16 +1067,14 @@ at the end of locked region (after inserting a newline and indenting)." while it's doing something (e.g. loading libraries) to say how much progress it's made. Obviously we need to display these as soon as they arrive." - (let (mrk str file module) - (save-excursion - (goto-char (point-max)) - (search-backward proof-shell-eager-annotation-start) - (setq mrk (+ 1 (point))) - (search-forward proof-shell-eager-annotation-end) - (setq str (buffer-substring mrk (- (point) 1))) - (display-buffer (set-buffer proof-pbp-buffer)) - (goto-char (point-max)) - (insert str "\n")) + (let ((str (proof-shell-handle-output + proof-shell-eager-annotation-start + proof-shell-eager-annotation-end + 'font-lock-eager-annotation-face)) + file module) + (proof-message str) + ;;FIXME: LEGO specific regular expression to detect that LEGO is + ;;processing a new module (if (string-match "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" str) (progn (setq file (match-string 2 str) diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index f9fb52d2..9d770a43 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -34,9 +34,8 @@ (defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) ;; ----- regular expressions for font-lock -(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" - "A regular expression indicating that the LEGO process has - identified an error.") +(defconst lego-error-regexp "^\\(Error\\|Lego parser\\)" + "A regular expression indicating that the LEGO process has identified an error.") (defvar lego-id proof-id) diff --git a/lego/lego.el b/lego/lego.el index 2b83e51a..aed76bdf 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -427,8 +427,6 @@ ("lego" . lego-tags)) tag-table-alist))) - (setq font-lock-keywords lego-font-lock-keywords-1) - ;; where to find files (setq compilation-search-path (cons nil (lego-get-path))) @@ -437,6 +435,8 @@ ;; font-lock + (setq font-lock-keywords lego-font-lock-keywords-1) + ;; if we don't have the following in xemacs, zap-commas fails to work. (and (boundp 'font-lock-always-fontify-immediately) @@ -475,7 +475,11 @@ proof-shell-init-cmd lego-process-config proof-analyse-using-stack nil proof-shell-process-output-system-specific lego-shell-process-output - lego-shell-current-line-width nil) + lego-shell-current-line-width nil + + ;;FIXME: we ought to set up separate font-lock instructions for + ;;the shell, the goal buffer and the script + font-lock-keywords lego-font-lock-keywords-1) (lego-init-syntax-table) |