diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/bufhist.el | 20 | ||||
| -rw-r--r-- | lib/holes-load.el | 14 | ||||
| -rw-r--r-- | lib/holes.el | 55 | ||||
| -rw-r--r-- | lib/local-vars-list.el | 2 | ||||
| -rw-r--r-- | lib/maths-menu.el | 47 | ||||
| -rw-r--r-- | lib/pg-dev.el | 2 | ||||
| -rw-r--r-- | lib/pg-fontsets.el | 7 | ||||
| -rw-r--r-- | lib/proof-compat.el | 387 | ||||
| -rw-r--r-- | lib/span-extent.el | 139 | ||||
| -rw-r--r-- | lib/span-overlay.el | 222 | ||||
| -rw-r--r-- | lib/span.el | 209 | ||||
| -rw-r--r-- | lib/unicode-tokens.el | 1202 | ||||
| -rw-r--r-- | lib/xml-fixed.el | 508 |
13 files changed, 831 insertions, 1983 deletions
diff --git a/lib/bufhist.el b/lib/bufhist.el index 4917819f..c6e70c9d 100644 --- a/lib/bufhist.el +++ b/lib/bufhist.el @@ -73,18 +73,14 @@ indicator 'help-echo desc 'keymap (eval-when-compile - (cond - ((featurep 'xemacs) - nil) - (t - (let ((map (make-sparse-keymap))) - ;; FIXME: clicking can go wrong here because the - ;; current buffer can be something else which has no hist! - (define-key map [mode-line mouse-1] 'bufhist-prev) - (define-key map [mode-line mouse-3] 'bufhist-next) - ;; (define-key map [mode-line control mouse-1] 'bufhist-first) - ;; (define-key map [mode-line control mouse-3] 'bufhist-last) - map)))) + (let ((map (make-sparse-keymap))) + ;; FIXME: clicking can go wrong here because the + ;; current buffer can be something else which has no hist! + (define-key map [mode-line mouse-1] 'bufhist-prev) + (define-key map [mode-line mouse-3] 'bufhist-next) + ;; (define-key map [mode-line control mouse-1] 'bufhist-first) + ;; (define-key map [mode-line control mouse-3] 'bufhist-last) + map)) 'mouse-face 'mode-line-highlight)))) ;simple: diff --git a/lib/holes-load.el b/lib/holes-load.el deleted file mode 100644 index 0c0a8b80..00000000 --- a/lib/holes-load.el +++ /dev/null @@ -1,14 +0,0 @@ -; To use holes-mode, require this file in your .emacs and add path to -; holes.el in the load-path of emacs - -(autoload 'holes-mode "holes" - "Minor mode for using \"holes\" in your buffers." t) -(autoload 'holes-set-make-active-hole "holes" - "Makes a new hole and make it active." t) -(autoload 'holes-abbrev-complete "holes" - "Completes an abbreviation, and replace #s ans @{}s by holes.") -(autoload 'holes-insert-and-expand "holes" - "insert and expand an abbreviation, and replace #s ans @{}s by holes.") - -(provide 'holes-load) - diff --git a/lib/holes.el b/lib/holes.el index 8fe9139f..65b1cc18 100644 --- a/lib/holes.el +++ b/lib/holes.el @@ -1,6 +1,7 @@ ;;; holes.el --- a little piece of elisp to define holes in your buffer ;; ;; Copyright (C) 2001 Pierre Courtieu +;; ;; $Id$ ;; ;; This file uses spans, an interface for extent (XEmacs) and overlays @@ -29,7 +30,7 @@ ;;; History: ;; -(require 'span) +(eval-when-compile (require 'span)) (require 'cl) ;;; Help: @@ -128,19 +129,6 @@ is), which is annoying. ;;; Code: -(cond - ((featurep 'xemacs) - (defalias 'holes-region-exists-p 'region-exists-p) - (defalias 'holes-get-selection 'get-selection)) - (t - ;;Pierre: should do almost what region-exists-p does in XEmacs - (defun holes-region-exists-p nil - "Return t if the mark is active, nil otherwise." - mark-active) - (defun holes-get-selection nil "See `current-kill'." - (current-kill 0)))) - - ;;; initialization (defvar holes-default-hole (make-detached-span) "An empty detached hole used as the default hole. @@ -204,17 +192,17 @@ which should be removed when making the text into a hole.") (defun holes-region-beginning-or-nil () "Internal." - (and (holes-region-exists-p) (region-beginning)) + (and mark-active (region-beginning)) ) (defun holes-region-end-or-nil () "Internal." - (and (holes-region-exists-p) (region-end)) + (and mark-active (region-end)) ) (defun holes-copy-active-region () "Internal." - (assert (holes-region-exists-p) nil "the region is not active now.") + (assert mark-active nil "the region is not active now.") (copy-region-as-kill (region-beginning) (region-end)) (car kill-ring) ) @@ -540,7 +528,7 @@ goal(FIXME?). Use `replace-active-hole' instead." "Replace the active hole by STR, if no str is given, then put the selection instead." (if (not (holes-active-hole-exist-p)) () (holes-replace - (or str (holes-get-selection) (error "Nothing to put in hole")) + (or str (current-kill 0) (error "Nothing to put in hole")) holes-active-hole) )) @@ -557,8 +545,8 @@ following hole if it exists." (let ((nxthole (holes-next-after-active-hole))) (holes-replace-active-hole (or str - (and (holes-region-exists-p) (holes-copy-active-region)) - (holes-get-selection) (error "Nothing to put in hole"))) + (and mark-active (holes-copy-active-region)) + (current-kill 0) (error "Nothing to put in hole"))) (if nxthole (holes-set-active-hole nxthole) (setq holes-active-hole holes-default-hole)) ) @@ -573,6 +561,8 @@ Sets `holes-active-hole' to the next hole if it exists." (holes-replace-update-active-hole "") ) + +;;;###autoload (defun holes-set-make-active-hole (&optional start end) "Make a new hole between START and END or at point, and make it active." @@ -628,11 +618,11 @@ Sets `holes-active-hole' to the next hole if it exists." (save-excursion ;;HACK: nothing if one click (but a second is perhaps coming) (if (and (eq (holes-track-mouse-clicks) 1) - (not (holes-region-exists-p))) + (not mark-active)) () - (if (not (holes-region-exists-p)) + (if (not mark-active) (error "Nothing to put in hole") - (holes-replace-update-active-hole (holes-get-selection)) + (holes-replace-update-active-hole (current-kill 0)) (message "hole replaced") ) ) @@ -696,10 +686,10 @@ Sets `holes-active-hole' to the next hole if it exists." (holes-track-mouse-selection event) (if (and (eq (holes-track-mouse-clicks) 1) - (not (holes-region-exists-p))) + (not mark-active)) (holes-set-make-active-hole (point) (point)) - (if (holes-region-exists-p) + (if mark-active (holes-set-make-active-hole) (let ((ext (holes-hole-at-event event))) (if (and ext (holes-is-hole-p ext)) @@ -740,15 +730,9 @@ Destroy it and makes the next hole active if any." (defvar hole-map (let ((map (make-sparse-keymap))) - (cond - ((featurep 'xemacs) - (define-key map [(button1)] 'holes-mouse-set-active-hole) - (define-key map [(button3)] 'holes-mouse-destroy-hole) - (define-key map [(button2)] 'holes-mouse-forget-hole)) - (t - (define-key map [(mouse-1)] 'holes-mouse-set-active-hole) - (define-key map [(mouse-3)] 'holes-mouse-destroy-hole) - (define-key map [(mouse-2)] 'holes-mouse-forget-hole))) + (define-key map [(mouse-1)] 'holes-mouse-set-active-hole) + (define-key map [(mouse-3)] 'holes-mouse-destroy-hole) + (define-key map [(mouse-2)] 'holes-mouse-forget-hole) map) "Keymap to use on the holes's overlays. This keymap is used only when @@ -842,6 +826,7 @@ created. Return the number of holes created." +;;;###autoload (defun holes-abbrev-complete () "Complete abbrev by putting holes and indenting. Moves point at beginning of expanded text. Put this function as @@ -850,7 +835,7 @@ become holes." (holes-replace-string-by-holes-backward-jump last-abbrev-location)) - +;;;###autoload (defun holes-insert-and-expand (s) "Insert S, expand it and replace #s and @{]s by holes." ;; insert the expansion of abbrev s, and replace #s by holes. It was diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el index f0b6678e..c55cee44 100644 --- a/lib/local-vars-list.el +++ b/lib/local-vars-list.el @@ -29,7 +29,7 @@ "From Emacs Info: A file can contain a \"local variables list\", which specifies the values to use for -certain Emacs variables when that file is edited. See info node \"(xemacs)File +certain Emacs variables when that file is edited. See info node \"(emacs)File Variables\". local-vars-list provides two useful functions: diff --git a/lib/maths-menu.el b/lib/maths-menu.el index ab15439f..5e75eba7 100644 --- a/lib/maths-menu.el +++ b/lib/maths-menu.el @@ -5,7 +5,9 @@ ;; Author: Dave Love <fx@gnu.org> ;; Keywords: convenience -;; Version for Proof General minimally modified by David Aspinall, 2007-8. +;; Version for Proof General modified by David Aspinall, 2007-8. +;; - Hooks added to insert tokenised versions of unicode characters. +;; - Added more characters to the menus. ;; $Id$ @@ -48,6 +50,12 @@ ;;; Code: +(defvar maths-menu-filter-predicate '(lambda (char) t) + "Predicate function used to filter menu elements") + +(defvar maths-menu-tokenise-insert '(lambda (char) (insert char)) + "Function used to insert possibly formatted or escaped character.") + (defun maths-menu-build-menu (spec) (let ((map (make-sparse-keymap "Characters"))) (dolist (pane spec) @@ -57,19 +65,25 @@ (dolist (elt pane) (define-key-after pane-map (vector (intern (string (car elt)))) ; convenient unique symbol - (cons (format "%c (%s)" (car elt) (cadr elt)) - ;; Using a string here doesn't work. You get a - ;; `Wrong type argument: commandp,' error. - ;; That looks like a bug, since - ;; (commandp "a") => t + (list 'menu-item + (format "%c (%s)" (car elt) (cadr elt)) `(lambda () (interactive) - (insert ,(car elt)))))))) + (funcall maths-menu-tokenise-insert ,(car elt))) + :visible `(funcall maths-menu-filter-predicate ,(car elt))))))) map)) (defvar maths-menu-menu (maths-menu-build-menu - '(("Binops 1" + '(("Logic" + (?$A!D(B "and") + (?$A!E(B "or") + (?$,1x (B "for all") + (?$,1x#(B "there exists") + (?$,1x$(B "there does not exist") + (?$,1yd(B "down tack") + (?$,1ye(B "up tack")) + ("Binops 1" (?,A1(B "plus-minus sign") (?$,1x3(B "minus-or-plus sign") (?,AW(B "multiplication sign") @@ -175,6 +189,17 @@ (?$,1vy(B "south west arrow") (?$,1vv(B "north west arrow") (?$,1w[(B "rightwards triple arrow")) + ("Long arrows" + (?$,2'v(B "long rightwards arrow") + (?$,2'w(B "long left right arrow") + (?$,2'x(B "long left double arrow") + (?$,2'y(B "long right double arrow") + (?$,2'z(B "long left right double arrow") + (?$,2'{(B "long left arrow from bar") + (?$,2'|(B "long right arrow from bar") + (?$,2'}(B "long left double arrow bar") + (?$,2'~(B "long right double arrow from bar") + (?$,2'(B "long rightwards squiggle arrow")) ("Symbols 1" (?$,1uu(B "alef symbol") ; don't use letter alef (avoid bidi confusion) (?$,1uO(B "planck constant over two pi") @@ -189,12 +214,7 @@ (?$,1x'(B "nabla") (?$,1x:(B "square root") (?$,1x;(B "cube root") - (?$,1yd(B "down tack") - (?$,1ye(B "up tack") (?$,1x@(B "angle") - (?$,1x (B "for all") - (?$,1x#(B "there exists") - (?$,1x$(B "there does not exist") (?,A,(B "not sign") (?$,2#o(B "music sharp sign") (?$,1x"(B "partial differential") @@ -214,6 +234,7 @@ (?$,1z (B "n-ary logical and") (?$,1uU(B "double-struck capital n") (?$,1uY(B "double-struck capital p") + (?$,1uZ(B "double-struck capital q") (?$,1u](B "double-struck capital r") (?$,1ud(B "double-struck capital z") (?$,1uP(B "script capital i") diff --git a/lib/pg-dev.el b/lib/pg-dev.el index 692b4bef..ffcf3597 100644 --- a/lib/pg-dev.el +++ b/lib/pg-dev.el @@ -79,7 +79,7 @@ proof-autoloads pg-response pg-goals proof-toolbar proof-easy-config proof-config proof-mmm proof proof-utils proof-syntax pg-user pg-custom - proof-x-symbol proof-maths-menu proof-unicode-tokens + proof-maths-menu proof-unicode-tokens pg-thymodes pg-autotest ;; isar-syntax isar-find-theorems x-symbol-isar diff --git a/lib/pg-fontsets.el b/lib/pg-fontsets.el index 67d57598..a860929c 100644 --- a/lib/pg-fontsets.el +++ b/lib/pg-fontsets.el @@ -17,6 +17,11 @@ ;; ;; DejaVu LGC (Sans and Sans Mono). See http://dejavu.sourceforge.net ;; - missing Uplus, smile, frown, join +;; +;; TODO: +;; -- make a fontset which combines symbol characters from a +;; symbol-rich font +;; ;;; Code: @@ -61,5 +66,5 @@ gnu-unifont:-*-%F-medium-r-normal--%S-*-*-*-*-*-iso10646-1" (pg-fontsets-make-fontsets) - +(provide 'pg-fontsets) ;;; pg-fontsets.el ends here diff --git a/lib/proof-compat.el b/lib/proof-compat.el index 9e3a2b7c..0142364b 100644 --- a/lib/proof-compat.el +++ b/lib/proof-compat.el @@ -11,8 +11,10 @@ ;; track of them. ;; ;; The development policy for Proof General (since v3.7) is for the -;; main codebase to be written for the latest stable version of GNU -;; Emacs, following GNU Emacs advice on obsolete function calls. +;; main codebase to be written for the latest stable version of +;; GNU Emacs, following GNU Emacs advice on obsolete function calls. +;; +;; Since Proof General 4.0, XEmacs is not supported at all. ;; (eval-when-compile @@ -40,7 +42,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; -;;; Emacs and XEmacs modifications and adjustments +;;; Modifications and adjustments ;;; ;; Remove a custom setting. Needed to support dynamic reconfiguration. @@ -77,18 +79,6 @@ Done by `makunbound' and removing all properties mentioned by custom library." ;;; XEmacs compatibility ;;; -;; browse-url function isn't autoloaded in XEmacs 20.4 -(or (fboundp 'browse-url) - (autoload 'browse-url "browse-url" - "Ask a WWW browser to load URL." t)) - -;; executable-find isn't autoloaded in XEmacs 21.4.6 -(or (fboundp 'executable-find) - (autoload 'executable-find "executable" "\ -Search for COMMAND in exec-path and return the absolute file name. -Return nil if COMMAND is not found anywhere in `exec-path'." nil nil)) - - ;; Compatibility with XEmacs 20.3 (or (fboundp 'split-path) (defun split-path (path) @@ -98,158 +88,6 @@ with `path-separator'." (split-string path (regexp-quote path-separator)))) -;; Compatibility with XEmacs 21.4, API change in add-hook -(when - (and (featurep 'xemacs) - (eq emacs-major-version 21) - (<= emacs-minor-version 4)) - - (fset 'old-add-hook (symbol-function 'add-hook)) - (defun add-hook (hook function &optional append local) - "Add to the value of HOOK the function FUNCTION. -FUNCTION is not added if already present. -FUNCTION is added (if necessary) at the beginning of the hook list -unless the optional argument APPEND is non-nil, in which case -FUNCTION is added at the end. - -The optional fourth argument, LOCAL, if non-nil, says to modify -the hook's buffer-local value rather than its default value. -This makes the hook buffer-local if needed. -To make a hook variable buffer-local, always use -`make-local-hook', not `make-local-variable'. - -HOOK should be a symbol, and FUNCTION may be any valid function. If -HOOK is void, it is first set to nil. If HOOK's value is a single -function, it is changed to a list of functions. - -You can remove this hook yourself using `remove-hook'. - -See also `add-one-shot-hook'." - (if local (make-local-hook hook)) - (old-add-hook hook function append local))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; XEmacs compatibility with GNU Emacs -;;; - - -(or (fboundp 'subst-char-in-string) -;; Code is taken from Emacs 21.2.1/subr.el -(defun subst-char-in-string (fromchar tochar string &optional inplace) - "Replace FROMCHAR with TOCHAR in STRING each time it occurs. -Unless optional argument INPLACE is non-nil, return a new string." - (let ((i (length string)) - (newstr (if inplace string (copy-sequence string)))) - (while (> i 0) - (setq i (1- i)) - (if (eq (aref newstr i) fromchar) - (aset newstr i tochar))) - newstr))) - -;; Required by xmltok.el [not used at present], proof-shell.el -(or (fboundp 'replace-regexp-in-string) - -;; Code is taken from Emacs 21.1.1/subr.el. Now in XEmacs (21.5b28, at least) -(defun replace-regexp-in-string (regexp rep string &optional - fixedcase literal subexp start) - "Replace all matches for REGEXP with REP in STRING. - -Return a new string containing the replacements. - -Optional arguments FIXEDCASE, LITERAL and SUBEXP are like the -arguments with the same names of function `replace-match'. If START -is non-nil, start replacements at that index in STRING. - -REP is either a string used as the NEWTEXT arg of `replace-match' or a -function. If it is a function it is applied to each match to generate -the replacement passed to `replace-match'; the match-data at this -point are such that match 0 is the function's argument. - -To replace only the first match (if any), make REGEXP match up to \\' -and replace a sub-expression, e.g. - (replace-regexp-in-string \"\\(foo\\).*\\'\" \"bar\" \" foo foo\" nil nil 1) - => \" bar foo\" -" - - ;; To avoid excessive consing from multiple matches in long strings, - ;; don't just call `replace-match' continually. Walk down the - ;; string looking for matches of REGEXP and building up a (reversed) - ;; list MATCHES. This comprises segments of STRING which weren't - ;; matched interspersed with replacements for segments that were. - ;; [For a `large' number of replacments it's more efficient to - ;; operate in a temporary buffer; we can't tell from the function's - ;; args whether to choose the buffer-based implementation, though it - ;; might be reasonable to do so for long enough STRING.] - (let ((l (length string)) - (start (or start 0)) - matches str mb me) - (save-match-data - (while (and (< start l) (string-match regexp string start)) - (setq mb (match-beginning 0) - me (match-end 0)) - ;; If we matched the empty string, make sure we advance by one char - (when (= me mb) (setq me (min l (1+ mb)))) - ;; Generate a replacement for the matched substring. - ;; Operate only on the substring to minimize string consing. - ;; Set up match data for the substring for replacement; - ;; presumably this is likely to be faster than munging the - ;; match data directly in Lisp. - (string-match regexp (setq str (substring string mb me))) - (setq matches - (cons (replace-match (if (stringp rep) - rep - (funcall rep (match-string 0 str))) - fixedcase literal str subexp) - (cons (substring string start mb) ; unmatched prefix - matches))) - (setq start me)) - ;; Reconstruct a string from the pieces. - (setq matches (cons (substring string start l) matches)) ; leftover - (apply #'concat (nreverse matches)))))) - - -;; The GNU Emacs implementation of easy-menu-define has a very handy -;; :visible keyword. To use that when it's available, we set a -;; constant to be :visible or :active - -(defconst menuvisiblep (if (featurep 'xemacs) :active :visible) - ":visible (on GNU Emacs) or :active (otherwise). -The GNU Emacs implementation of easy-menu-define has a very handy -:visible keyword. To use that when it's available, we use this constant.") - - -(or (fboundp 'frame-parameter) - (defalias 'frame-parameter 'frame-property)) - -(or (boundp 'window-size-fixed) - (defvar window-size-fixed nil - "Fudged version of GNU Emacs' setting. Completely ignored.")) - -(or (fboundp 'window-text-height) - (defalias 'window-text-height 'window-text-area-height)) - -(or (fboundp 'set-window-text-height) -(defun set-window-text-height (window height) - "Sets the height in lines of the text display area of WINDOW to HEIGHT. -This doesn't include the mode-line (or header-line if any) or any -partial-height lines in the text display area. - -If WINDOW is nil, the selected window is used. - -Note that the current implementation of this function cannot always set -the height exactly, but attempts to be conservative, by allocating more -lines than are actually needed in the case where some error may be present." - (let ((delta (- height (window-text-height window)))) - (unless (zerop delta) - (let ((window-min-height 1)) - (if (and window (not (eq window (selected-window)))) - (save-selected-window - (select-window window) - (enlarge-window delta)) - (enlarge-window delta))))))) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; ;;; GNU Emacs compatibility with XEmacs @@ -265,46 +103,15 @@ The value returned is the value of the last form in BODY." (progn ,@body) (select-frame ,old-frame)))))) -;; Chars (borrowed from x-symbol-emacs.el compatability file) - -(unless (fboundp 'characterp) (defalias 'characterp 'integerp)) -(unless (fboundp 'int-to-char) (defalias 'int-to-char 'identity)) -(unless (fboundp 'char-to-int) (defalias 'char-to-int 'identity)) - ;; Missing function, but anyway Emacs has no datatype for events... (unless (fboundp 'events-to-keys) (defalias 'events-to-keys 'identity)) -(unless (fboundp 'region-exists-p) - (defun region-exists-p () mark-active)) - ;; completion not autoloaded in GNU 20.6.1; we must call ;; dynamic-completion-mode after loading it. (or (fboundp 'complete) (autoload 'complete "completion")) -(unless (featurep 'xemacs) - (eval-after-load "completion" - '(dynamic-completion-mode))) - - -;; These days cl is dumped with XEmacs (20.4,21.1) but not GNU Emacs -;; 20.2. Would rather it was autoloaded but the autoloads are broken -;; in GNU so we load it now. -(require 'cl) - -;; Give a warning, -(or (fboundp 'warn) -(defun warn (str &rest args) - "Issue a warning STR. Defined by PG for GNU compatibility." - (apply 'message str args) - (sit-for 2))) - -;; Modeline redrawing (actually force-mode-line-update is alias on XEmacs) -(or (fboundp 'redraw-modeline) -(defun redraw-modeline (&rest args) - "Dummy function for Proof General on GNU Emacs." - (force-mode-line-update))) ;; Replace in string: XEmacs original now in GNU Emacs as replace-regexp-in-string (or (fboundp 'replace-in-string) @@ -336,14 +143,9 @@ The returned value is one of the following symbols: ;; In case Emacs is not aware of the function read-shell-command, ;; we duplicate some code adjusted from minibuf.el distributed -;; with XEmacs 21.1.9 -;; -;; This code is still required as of GNU Emacs 20.6.1 -;; -;; da: I think bothering with this just to give completion for -;; when proof-prog-name-ask=t is rather a big overkill! -;; Still, now it's here we'll leave it in as a pleasant surprise -;; for GNU Emacs users. +;; with XEmacs 21.1.9. Bothering with this just to give completion for +;; when proof-prog-name-ask=t is a bit of an overkill! +;; Still, now it's here we'll leave it in as a pleasant surprise. ;; (or (fboundp 'read-shell-command) (defvar read-shell-command-map @@ -372,33 +174,6 @@ The returned value is one of the following symbols: nil (or history 'shell-command-history))))) -;; Emulate a useful builtin from XEmacs. - -(or (fboundp 'remassq) -;; NB: Emacs has assoc package with assq-delete-all function -(defun remassq (key alist) - "Delete any elements of ALIST whose car is `eq' to KEY. -The modified ALIST is returned." -;; The builtin version deletes by side-effect, but don't bother here. - (let (newalist) - (while alist - (unless (eq key (caar alist)) - (setq newalist (cons (car alist) newalist))) - (setq alist (cdr alist))) - (nreverse newalist)))) - -(or (fboundp 'remassoc) -(defun remassoc (key alist) - "Delete any elements of ALIST whose car is `equal' to KEY. -The modified ALIST is returned." -;; The builtin version deletes by side-effect, but don't bother here. - (let (newalist) - (while alist - (unless (equal key (caar alist)) - (setq newalist (cons (car alist) newalist))) - (setq alist (cdr alist))) - (nreverse newalist)))) - (or (fboundp 'frames-of-buffer) ;; From XEmacs 21.4.12, aliases expanded (defun frames-of-buffer (&optional buffer visible-only) @@ -438,6 +213,11 @@ is first in the list. VISIBLE-ONLY will only list non-iconified frames." (>= (nth 2 (window-edges window)) (frame-width (window-frame window))))) +(or (fboundp 'window-bottom-p) + (defun window-bottom-p (window) + (>= (nth 3 (window-edges window)) + (frame-height (window-frame window))))) + ;; with-selected-window from XEmacs 21.4.12 (or (fboundp 'with-selected-window) (defmacro with-selected-window (window &rest body) @@ -471,88 +251,18 @@ The value returned is the value of the last form in BODY." (funcall (get this-command 'completion-function))))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; Attempt to harmonise pop-to-buffer behaviour -;;; - -(or (featurep 'xemacs) - ;; NB: GNU Emacs version has fewer args - (defalias 'pg-pop-to-buffer 'pop-to-buffer)) - -(if (featurep 'xemacs) -;; Version from XEmacs 21.4.12, with args to match GNU Emacs -;; NB: GNU Emacs version has fewer args, we don't use ON-FRAME -(defun pg-pop-to-buffer (bufname &optional not-this-window-p no-record on-frame) - "Select buffer BUFNAME in some window, preferably a different one. -If BUFNAME is nil, then some other buffer is chosen. -If `pop-up-windows' is non-nil, windows can be split to do this. -If optional second arg NOT-THIS-WINDOW-P is non-nil, insist on finding -another window even if BUFNAME is already visible in the selected window. -If optional fourth arg is non-nil, it is the frame to pop to this -buffer on. -If optional third arg is non-nil, do not record this in switching history. -(addition for PG). - -If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged." - (let ((oldbuf (current-buffer)) - buf window frame) - (if (null bufname) - (setq buf (other-buffer (current-buffer))) - (setq buf (get-buffer bufname)) - (if (null buf) - (progn - (setq buf (get-buffer-create bufname)) - (set-buffer-major-mode buf)))) - (push-window-configuration) - (set-buffer buf) - (setq window (display-buffer buf not-this-window-p on-frame)) - (setq frame (window-frame window)) - ;; if the display-buffer hook decided to show this buffer in another - ;; frame, then select that frame, (unless obeying focus-follows-mouse -sb). - (if (and (not focus-follows-mouse) - (not (eq frame (selected-frame)))) - (select-frame frame)) - (unless no-record (record-buffer buf)) - (if (and focus-follows-mouse - on-frame - (not (eq on-frame (selected-frame)))) - (set-buffer oldbuf) - ;; select-window will modify the internal keyboard focus of XEmacs - (select-window window)) - buf)) -) - - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; Old Emacs version compatibility (to be gradually removed...) -;;; - -;; Create a menu from a customize group, for older/non-existent customize - (or (fboundp 'process-live-p) (defun process-live-p (obj) "Return t if OBJECT is a process that is alive" (and (processp obj) (memq (process-status obj) '(open run stop))))) -(or (fboundp 'buffer-substring-no-properties) - (defalias 'buffer-substring-no-properties 'buffer-substring)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; ;;; General Emacs version compatibility ;;; -;; Handle buggy buffer-syntactic-context workaround in XEmacs, -;; and GNU Emacs non-implementation. -;; Latest: block comment is unreliable still in XEmacs 21.5, -;; doesn't seem worth attempting to use the native function at all. - (defalias 'proof-buffer-syntactic-context 'proof-buffer-syntactic-context-emulate) @@ -562,77 +272,6 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged." ;;; Nasty: Emacs bug/problem fix section ;;; -;; NB: customize-menu-create is buggy in some versions of GNU Emacs -;; (bad in 21.1.0, good in 21.1.1, bad in 21.2.1, ...). Comment -;; these next lines out if you must use one of these versions. -;; PG 3.5.1: add hack in proof-compat.el to deal with this -(if - (and - (not (featurep 'xemacs)) - (or - (string-equal emacs-version "21.2.1") - (string-equal emacs-version "21.1.0"))) - (defun customize-menu-create (symbol &optional name) - (cons - (or name "Customize") - (list - ["Your version of Emacs is buggy; update to get this menu" - '(w3-goto-url "http://www.gnu.org/software/emacs/") - t])))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; Tweak to XEmacs buffer tabs (not really compatibility) -;;; - -;; We remove PG auxiliary buffers from tabs. -;; TODO: complain to XEmacs developers about overly generous matching -;; in this function. In XEmacs post 21.5 one can set names of buffers -;; to omit just from tabs list. - -(if (featurep 'xemacs) - (progn - - (fset 'select-buffers-tab-buffers-by-mode-old - (symbol-function 'select-buffers-tab-buffers-by-mode)) - - (defun select-buffers-tab-buffers-by-mode (buf1 buf2) - (let* ((mode1 (symbol-value-in-buffer 'major-mode buf1)) ;; candidate buf - (mode2 (symbol-value-in-buffer 'major-mode buf2)) ;; displayed buf - (auxes '(proof-goals-mode proof-shell-mode proof-response-mode)) - (mode1aux (memq (get mode1 'derived-mode-parent) auxes)) - (mode2aux (memq (get mode2 'derived-mode-parent) auxes))) - (cond - (mode1aux mode2aux) - (mode2aux nil) - (t (select-buffers-tab-buffers-by-mode-old buf1 buf2))))) - )) ;; end XEmacs featurep - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Workaround GNU Emacs problems in easymenu-add -;; - -(if (not (featurep 'xemacs)) - ;; This has a nasty side effect of removing accelerators - ;; from existing menus when easy-menu-add is called. - ;; Problem confirmed in versions: 21.4.1, OK: 22.1.1 - (or (< emacs-major-version 22) - (setq easy-menu-precalculate-equivalent-keybindings nil))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; XEmacs/x-symbol compatibility for XEmacs 21.5 -;; -;; See http://thread.gmane.org/gmane.emacs.xemacs.beta/20171/focus=20172 - -(if (and (fboundp 'valid-specifier-tag-p) - (not (valid-specifier-tag-p 'mule-fonts))) - (if (fboundp 'define-specifier-tag) - (define-specifier-tag 'mule-fonts))) - ;; End of proof-compat.el (provide 'proof-compat) diff --git a/lib/span-extent.el b/lib/span-extent.el deleted file mode 100644 index 8af787c7..00000000 --- a/lib/span-extent.el +++ /dev/null @@ -1,139 +0,0 @@ -;; This file implements spans in terms of extents, for xemacs. -;; -;; Copyright (C) 1998 LFCS Edinburgh -;; Author: Healfdene Goguen -;; Maintainer: David Aspinall <David.Aspinall@ed.ac.uk> -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ - -;; XEmacs-Emacs compatibility: define "spans" in terms of extents. - -(defsubst span-make (start end) - "Make a span for the range [START, END) in current buffer." - (make-extent start end)) - -(defsubst span-detach (span) - "Remove SPAN from its buffer." - (detach-extent span)) - -(defsubst span-set-endpoints (span start end) - "Set the endpoints of SPAN to START, END." - (set-extent-endpoints span start end)) - -(defsubst span-set-property (span name value) - "Set SPAN's property NAME to VALUE." - (set-extent-property span name value)) - -(defsubst span-read-only (span) - "Set SPAN to be read only." - (span-set-property span 'read-only t)) - -(defsubst span-read-write (span) - "Set SPAN to be writeable." - (span-set-property span 'read-only nil)) - -(defun span-give-warning (&rest args) - "Give a warning message." - (message "You should not edit here!")) - -(defun span-write-warning (span) - "Give a warning message when SPAN is changed." - ;; FIXME: implement this in XEmacs, perhaps with after-change-functions - (span-set-property span 'read-only nil)) - -(defsubst span-property (span name) - "Return SPAN's value for property PROPERTY." - (extent-property span name)) - -(defsubst span-delete (span) - "Delete SPAN." - (let ((predelfn (span-property span 'span-delete-action))) - (and predelfn (funcall predelfn))) - (delete-extent span)) - -(defsubst span-mapcar-spans (fn start end prop &optional val) - "Apply function FN to all spans between START and END with property PROP set" - (mapcar-extents fn nil (current-buffer) start end nil prop val)) - -(defsubst spans-at-region-prop (start end prop &optional val) - "Return a list of the spans in START END with PROP [set to VAL]." - (extent-list (current-buffer) start end nil prop val)) - -(defsubst span-at (pt prop) - "Return the smallest SPAN at point PT with property PROP." - (extent-at pt nil prop)) - -(defsubst span-at-before (pt prop) - "Return the smallest SPAN at before PT with property PROP. -A span is before PT if it covers the character before PT." - (extent-at pt nil prop nil 'before)) - -(defsubst span-start (span) - "Return the start position of SPAN, or nil if SPAN is detatched." - (extent-start-position span)) - -(defsubst span-end (span) - "Return the end position of SPAN, or nil if SPAN is detatched." - (extent-end-position span)) - -(defsubst prev-span (span prop) - "Return span before SPAN with property PROP." - (extent-at (extent-start-position span) nil prop nil 'before)) - -(defsubst next-span (span prop) - "Return span after SPAN with property PROP." - (extent-at (extent-end-position span) nil prop nil 'after)) - -(defsubst span-live-p (span) - "Return non-nil if SPAN is live and in a live buffer." - (and span - (extent-live-p span) - (buffer-live-p (extent-object span)) - ;; PG 3.4: add third test here to see not detached. - (not (extent-detached-p span)))) - -(defun span-raise (span) - "Function added for FSF Emacs compatibility. Do nothing here." - nil) - -(defalias 'span-object 'extent-object) -(defalias 'span-string 'extent-string) - -;Pierre: new utility functions for "holes" -(defsubst make-detached-span () - (make-extent nil nil) - ) - - -(defsubst span-buffer (span) - "Return the buffer owning span." - (extent-object span) - ) - -(defsubst span-detached-p (span) - "is this span detached? nil for no, t for yes" - (extent-detached-p span) -) - -(defsubst set-span-face (span face) - "set the face of a span" - (set-extent-face span face)) - -(defsubst fold-spans (function &optional object from to maparg flags property value) - "map on span, see map-extent on xemacs" - (map-extents function object from to maparg flags property value)) - -(defsubst set-span-properties (span plist) - "see extent-properties" - (set-extent-properties span plist)) - -(defsubst set-span-keymap (span map) - "Set the keymap of SPAN to MAP" - (set-extent-keymap span map)) - -;there are more args to extent-at-event -(defsubst span-at-event (event &optional prop) - (extent-at-event event prop)) - -(provide 'span-extent) diff --git a/lib/span-overlay.el b/lib/span-overlay.el deleted file mode 100644 index fe51ebc6..00000000 --- a/lib/span-overlay.el +++ /dev/null @@ -1,222 +0,0 @@ -;; This file implements spans in terms of extents, for emacs19. -;; -;; Copyright (C) 1998 LFCS Edinburgh -;; Author: Healfdene Goguen -;; Maintainer: David Aspinall <David.Aspinall@ed.ac.uk> -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ - -;; XEmacs-Emacs compatibility: define "spans" in terms of overlays. - -(defalias 'span-start 'overlay-start) -(defalias 'span-end 'overlay-end) -(defalias 'span-set-property 'overlay-put) -(defalias 'span-property 'overlay-get) -(defalias 'span-make 'make-overlay) -(defalias 'span-detach 'delete-overlay) -(defalias 'span-set-endpoints 'move-overlay) -(defalias 'span-buffer 'overlay-buffer) - -(defun span-read-only-hook (overlay after start end &optional len) - (unless inhibit-read-only - (error "Region is read-only"))) - -(defun span-read-only (span) - "Set SPAN to be read only." - ;; This function may be called on spans which are detached from a - ;; buffer, which gives an error here, since text-properties are - ;; associated with text in a particular buffer position. So we use - ;; our own read only hook. - ;(add-text-properties (span-start span) (span-end span) '(read-only t))) - ;; 30.8.02: tested using overlay-put as below with Emacs 21.2.1, - ;; bit this seems to have no effect when the overlay is added to - ;; the buffer. (Maybe read-only is only a text property, not an - ;; overlay property?). - ;; (overlay-put span 'read-only t)) - (span-set-property span 'modification-hooks '(span-read-only-hook)) - (span-set-property span 'insert-in-front-hooks '(span-read-only-hook))) - -(defun span-read-write (span) - "Set SPAN to be writeable." - ;; See comment above for text properties problem. - (span-set-property span 'modification-hooks nil) - (span-set-property span 'insert-in-front-hooks nil)) - -(defun span-give-warning (&rest args) - "Give a warning message." - (message "You should not edit here!")) - -(defun span-write-warning (span) - "Give a warning message when SPAN is changed." - (span-set-property span 'modification-hooks '(span-give-warning)) - (span-set-property span 'insert-in-front-hooks '(span-give-warning))) - -;; We use end first because proof-locked-queue is often changed, and -;; its starting point is always 1 -(defun span-lt (s u) - (or (< (span-end s) (span-end u)) - (and (eq (span-end s) (span-end u)) - (< (span-start s) (span-start u))))) - -(defun spans-at-point-prop (pt prop) - (let ((ols ())) - (dolist (ol (overlays-at pt)) - (if (or (null prop) (overlay-get ol prop)) (push ol ols))) - ols)) - -(defun spans-at-region-prop (start end prop &optional val) - "Return a list of the spans in START END with PROP [set to VAL]." - (let ((ols ())) - (dolist (ol (overlays-in start end)) - (if (or (null prop) - (if val (eq val (overlay-get ol prop)) (overlay-get ol prop))) - (push ol ols))) - ols)) - -(defun span-at (pt prop) - "Return the SPAN at point PT with property PROP. -For XEmacs, span-at gives smallest extent at pos. -For Emacs, we assume that spans don't overlap." - (car (spans-at-point-prop pt prop))) - -(defsubst span-delete (span) - "Delete SPAN." - (let ((predelfn (span-property span 'span-delete-action))) - (and predelfn (funcall predelfn))) - (delete-overlay span)) - -;; The next two change ordering of list of spans: -(defsubst span-mapcar-spans (fn start end prop &optional val) - "Apply function FN to all spans between START and END with property PROP set" - (mapcar fn (spans-at-region-prop start end prop (or val nil)))) - -(defun span-at-before (pt prop) - "Return the smallest SPAN at before PT with property PROP. -A span is before PT if it begins before the character before PT." - (let ((ols (if (eq (point-min) pt) - nil ;; (overlays-at pt) - (overlays-in (1- pt) pt)))) - ;; Check the PROP is set. - (when prop - (dolist (ol (prog1 ols (setq ols nil))) - (if (overlay-get ol prop) (push ol ols)))) - ;; Eliminate the case of an empty overlay at (1- pt). - (dolist (ol (prog1 ols (setq ols nil))) - (if (>= (overlay-end ol) pt) (push ol ols))) - ;; "Get the smallest". I have no idea what that means, so I just do - ;; something somewhat random but vaguely meaningful. -Stef - (car (last (sort ols 'span-lt))))) - -(defun prev-span (span prop) - "Return span before SPAN with property PROP." - (span-at-before (span-start span) prop)) - -; overlays are [start, end) - -(defun next-span (span prop) - "Return span after SPAN with property PROP." - ;; Presuming the span-extents.el is the reference, its code does the same - ;; as the code below. - (span-at (span-end span) prop) - ;; ;; 3.4 fix here: Now we do a proper search, so this should work with - ;; ;; nested overlays, after a fashion. Use overlays-in to get a list - ;; ;; for the entire buffer, this avoids repeatedly checking the same - ;; ;; overlays in an ever expanding list (see v6.1). (However, this - ;; ;; list may be huge: is it a bottleneck?) - ;; ;; [Why has this function never used the before-list ?] - ;; (let* ((start (overlay-start span)) - ;; ;; (pos start) - ;; (nextos (overlays-in (overlay-end span) - ;; (1+ start) - ;; (point-max))) - ;; (resstart (1+ (point-max))) - ;; spanres) - ;; ;; overlays are returned in an unspecified order; we - ;; ;; must search whole list for a closest-next one. - ;; (dolist (newres nextos spanres) - ;; (if (and (span-property newres prop) - ;; (< start (span-start newres)) - ;; (< (span-start newres) resstart)) - ;; (progn - ;; (setq spanres newres) - ;; (setq resstart (span-start spanres)))))) -) - -(defsubst span-live-p (span) - "Return non-nil if SPAN is in a live buffer." - (and span - (overlay-buffer span) - (buffer-live-p (overlay-buffer span)))) - -(defun span-raise (span) - "Set priority of span to make it appear above other spans. -FIXME: new hack added nov 99 because of disappearing overlays. -Behaviour is still worse than before." ;??? --Stef - (span-set-property span 'priority 100)) - -(defalias 'span-object 'overlay-buffer) - -(defun span-string (span) - (with-current-buffer (overlay-buffer span) - (buffer-substring (overlay-start span) (overlay-end span)))) - - -;Pierre: new utility functions for "holes" -(defun set-span-properties (span plist) - "Set SPAN's properties, plist is a plist." - (let ((pl plist)) - (while pl - (let* ((name (car pl)) - (value (car (cdr pl)))) - (overlay-put span name value) - (setq pl (cdr (cdr pl)))) - ) - ) - ) - -(defun span-find-span (overlay-list &optional prop) - "Returns the first overlay of overlay-list having property prop (default 'span), nil if no such overlay belong to the list." - (let ((l overlay-list)) - (while (and l (not (overlay-get (car l) (or prop 'span)))) - (setq l (cdr l))) - (car l))) - -(defsubst span-at-event (event &optional prop) - (span-find-span (overlays-at (posn-point (event-start event))) prop)) - - -(defun make-detached-span () - (let ((ol (make-overlay 0 0))) - (delete-overlay ol) - ol)) - -(defun fold-spans (f &optional buffer from to maparg ignored-flags prop val) - (with-current-buffer (or buffer (current-buffer)) - (let ((ols (overlays-in (or from (point-min)) (or to (point-max)))) - res) - ;; Check the PROP. - (when prop - (dolist (ol (prog1 ols (setq ols nil))) - (if (if val (eq val (overlay-get ol prop)) (overlay-get ol prop)) - (push ol ols)))) - ;; Iterate in order. - (setq ols (sort ols 'span-lt)) - (while (and ols (not (setq res (funcall f (pop ols) maparg))))) - res))) - - -(defsubst span-detached-p (span) - "is this span detached? nil for no, t for yes" - (null (overlay-buffer span))) - -(defsubst set-span-face (span face) - "set the face of a span" - (overlay-put span 'face face)) - -(defun set-span-keymap (span map) - "Set the keymap of SPAN to MAP" - (overlay-put span 'keymap map) - (overlay-put span 'local-map map)) - -(provide 'span-overlay) diff --git a/lib/span.el b/lib/span.el index a07da038..5f87e015 100644 --- a/lib/span.el +++ b/lib/span.el @@ -1,19 +1,204 @@ -;; span.el Datatype of "spans" for Proof General. +;;; span.el --- Datatype of "spans" for Proof General ;; -;; Copyright (C) 1998 LFCS Edinburgh -;; Author: Healfdene Goguen -;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Copyright (C) 1998-2008 LFCS Edinburgh +;; Author: Healfdene Goguen +;; Maintainer: David Aspinall <David.Aspinall@ed.ac.uk> +;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ ;; -;; Spans are our abstraction of extents/overlays. +;;; Commentary: +;; +;; Spans are our abstraction of extents/overlays. Nowadays +;; we implement them directly with overlays. +;; +;; In future this module should be used to implement the abstraction +;; for script buffers (only) more directly. ;; -(eval-and-compile - (if (featurep 'xemacs) - (require 'span-extent)) - (if (not (featurep 'xemacs)) - (require 'span-overlay))) +;;; Code: +(eval-when-compile (require 'cl)) ;For lexical-let. + +(defalias 'span-start 'overlay-start) +(defalias 'span-end 'overlay-end) +(defalias 'span-set-property 'overlay-put) +(defalias 'span-property 'overlay-get) +(defalias 'span-make 'make-overlay) +(defalias 'span-detach 'delete-overlay) +(defalias 'span-set-endpoints 'move-overlay) +(defalias 'span-buffer 'overlay-buffer) + +(defun span-read-only-hook (overlay after start end &optional len) + (unless inhibit-read-only + (error "Region is read-only"))) +(add-to-list 'debug-ignored-errors "Region is read-only") + +(defun span-read-only (span) + "Set SPAN to be read only." + ;; Note: using the standard 'read-only property does not work. + ;; (overlay-put span 'read-only t)) + (span-set-property span 'modification-hooks '(span-read-only-hook)) + (span-set-property span 'insert-in-front-hooks '(span-read-only-hook))) + +(defun span-read-write (span) + "Set SPAN to be writeable." + (span-set-property span 'modification-hooks nil) + (span-set-property span 'insert-in-front-hooks nil)) + +(defun span-give-warning (&rest args) + "Give a warning message. +Optional argument ARGS is ignored." + (message "You should not edit here!")) + +(defun span-write-warning (span &optional fun) + "Give a warning message when SPAN is changed. +Optional argument FUN is used in place of `span-give-warning'." + (unless fun (setq fun 'span-give-warning)) + (lexical-let ((fun fun)) + (let ((funs (list (lambda (span afterp beg end &rest args) + (if (not afterp) (funcall fun beg end)))))) + (span-set-property span 'modification-hooks funs) + (span-set-property span 'insert-in-front-hooks funs)))) + +;; We use end first because proof-locked-queue is often changed, and +;; its starting point is always 1 +(defun span-lt (s u) + (or (< (span-end s) (span-end u)) + (and (eq (span-end s) (span-end u)) + (< (span-start s) (span-start u))))) + +(defun spans-at-point-prop (pt prop) + (let ((ols ())) + (dolist (ol (overlays-at pt)) + (if (or (null prop) (overlay-get ol prop)) (push ol ols))) + ols)) + +(defun spans-at-region-prop (start end prop &optional val) + "Return a list of the spans in START END with PROP [set to VAL]." + (let ((ols ())) + (dolist (ol (overlays-in start end)) + (if (or (null prop) + (if val (eq val (overlay-get ol prop)) (overlay-get ol prop))) + (push ol ols))) + ols)) + +(defun span-at (pt prop) + "Return the SPAN at point PT with property PROP. +For XEmacs, `span-at' gives smallest extent at pos. +For Emacs, we assume that spans don't overlap." + (car (spans-at-point-prop pt prop))) + +(defsubst span-delete (span) + "Delete SPAN." + (let ((predelfn (span-property span 'span-delete-action))) + (and predelfn (funcall predelfn))) + (delete-overlay span)) + +;; The next two change ordering of list of spans: +(defsubst span-mapcar-spans (fn start end prop &optional val) + "Apply function FN to all spans between START and END with property PROP set. +Optional argument VAL filters value of property." + (mapcar fn (spans-at-region-prop start end prop (or val nil)))) + +(defun span-at-before (pt prop) + "Return the smallest SPAN at before PT with property PROP. +A span is before PT if it begins before the character before PT." + (let ((ols (if (eq (point-min) pt) + nil ;; (overlays-at pt) + (overlays-in (1- pt) pt)))) + ;; Check the PROP is set. + (when prop + (dolist (ol (prog1 ols (setq ols nil))) + (if (overlay-get ol prop) (push ol ols)))) + ;; Eliminate the case of an empty overlay at (1- pt). + (dolist (ol (prog1 ols (setq ols nil))) + (if (>= (overlay-end ol) pt) (push ol ols))) + ;; "Get the smallest". I have no idea what that means, so I just do + ;; something somewhat random but vaguely meaningful. -Stef + (car (last (sort ols 'span-lt))))) + +(defun prev-span (span prop) + "Return span before SPAN with property PROP." + (span-at-before (span-start span) prop)) + +; overlays are [start, end) + +(defun next-span (span prop) + "Return span after SPAN with property PROP." + ;; Presuming the span-extents.el is the reference, its code does the same + ;; as the code below. + (span-at (span-end span) prop) +) + +(defsubst span-live-p (span) + "Return non-nil if SPAN is in a live buffer." + (and span + (overlay-buffer span) + (buffer-live-p (overlay-buffer span)))) + +(defun span-raise (span) + "Set priority of SPAN to make it appear above other spans." + (span-set-property span 'priority 100)) + +(defalias 'span-object 'overlay-buffer) + +(defun span-string (span) + (with-current-buffer (overlay-buffer span) + (buffer-substring (overlay-start span) (overlay-end span)))) + + +(defun set-span-properties (span plist) + "Set SPAN's properties, PLIST is a plist." + (let ((pl plist)) + (while pl + (let* ((name (car pl)) + (value (car (cdr pl)))) + (overlay-put span name value) + (setq pl (cdr (cdr pl)))) + ))) + +(defun span-find-span (overlay-list &optional prop) + "Return the first overlay of OVERLAY-LIST having property PROP (default 'span), nil if no such overlay belong to the list." + (let ((l overlay-list)) + (while (and l (not (overlay-get (car l) (or prop 'span)))) + (setq l (cdr l))) + (car l))) + +(defsubst span-at-event (event &optional prop) + (span-find-span (overlays-at (posn-point (event-start event))) prop)) + + +(defun make-detached-span () + (let ((ol (make-overlay 0 0))) + (delete-overlay ol) + ol)) + +(defun fold-spans (f &optional buffer from to maparg ignored-flags prop val) + (with-current-buffer (or buffer (current-buffer)) + (let ((ols (overlays-in (or from (point-min)) (or to (point-max)))) + res) + ;; Check the PROP. + (when prop + (dolist (ol (prog1 ols (setq ols nil))) + (if (if val (eq val (overlay-get ol prop)) (overlay-get ol prop)) + (push ol ols)))) + ;; Iterate in order. + (setq ols (sort ols 'span-lt)) + (while (and ols (not (setq res (funcall f (pop ols) maparg))))) + res))) + +(defsubst span-detached-p (span) + "Is this SPAN detached? nil for no, t for yes." + (null (overlay-buffer span))) + +(defsubst set-span-face (span face) + "Set the FACE of a SPAN." + (overlay-put span 'face face)) + +(defun set-span-keymap (span map) + "Set the keymap of SPAN to MAP." + (overlay-put span 'keymap map) + (overlay-put span 'local-map map)) ;; ;; Generic functions built on low-level concrete ones. @@ -35,5 +220,7 @@ "Set the end point of SPAN to VALUE." (span-set-endpoints span (span-start span) value)) + (provide 'span) -;; span.el ends here. + +;;; span.el ends here diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el index b789be93..98ff325e 100644 --- a/lib/unicode-tokens.el +++ b/lib/unicode-tokens.el @@ -1,4 +1,4 @@ -;;; unicode-tokens.el --- Support for editing tokens for Unicode characters +;;; unicode-tokens.el --- Support for control and symbol tokens ;; ;; Copyright(C) 2008 David Aspinall / LFCS Edinburgh ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> @@ -6,9 +6,6 @@ ;; ;; $Id$ ;; -;; A few functions are adapted from `xmlunicode.el' by Norman Walsh. -;; Created: 2004-07-21, Version: 1.6, Copyright (C) 2003 Norman Walsh -;; ;; This is free software; you can redistribute it and/or modify ;; it under the terms of the GNU General Public License as published by ;; the Free Software Foundation; either version 2, or (at your option) @@ -26,93 +23,142 @@ ;;; Commentary: ;; -;; This is a partial replacement for X-Symbol for Proof General. -;; STATUS: experimental. +;; This is a replacement for X-Symbol for Proof General. ;; -;; Functions to help insert tokens that represent Unicode characters -;; and control code sequences for changing the layout. Character -;; tokens are useful for programs that do not understand a Unicode -;; encoding. +;; Functions to display tokens that represent Unicode characters and +;; control code sequences for changing the layout. Tokens are useful +;; for programs that do not understand a Unicode encoding. ;; ;; TODO: -;; -- saving of font-lock-face annotations unreliable, possible confusion -;; over handling of lists in format.el -;; -- add input methods for subscript/superscripts (further props in general) -;; -- after change function so inserting control sequences works? or other support -;; -- one-char subs should not be sticky so doesn't extend -;; -- make property removal more accurate/patch in font-lock -;; -- disentangle Isabelle specific code -;; -- perhaps separate out short-cut input method and don't use for tokens -;; -- cleanup insertion functions -;; -- investigate testing for an appropriate glyph +;; -- insert tokens via numeric code (extra format string) +;; -- insert unicode character as token (reverse lookup) (require 'cl) -(require 'unicode-chars) ; list of Unicode characters +(eval-when-compile + (require 'maths-menu)) ; nuke compile warnings ;; -;; Variables that should be set -;; (default settings are for XML, but configuration incomplete; -;; use xmlunicode.el instead) +;; Variables that can be overridden in instances: symbol tokens ;; -(defvar unicode-tokens-charref-format "&#x%x;" - "The format for numeric character references") +(defvar unicode-tokens-token-symbol-map nil + "Mapping of token names to compositions. +Each element is a list -(defvar unicode-tokens-token-format "&%x;" - "The format for token character references") + (TOKNAME COMPOSITION FONTSYMB ...) -(defvar unicode-tokens-token-name-alist nil - "Mapping of token names to Unicode strings.") +A composition is typically a single Unicode character string, but +can be more complex: see documentation of `compose-region'. -(defvar unicode-tokens-glyph-list nil - "List of available glyphs, as characters. -If not set, constructed to include glyphs for all tokens. ") +The list of FONTSYMB are optional. Each FONTSYMB is a symbol +indicating a set of text properties, looked up in +`unicode-tokens-fontsymb-properties'.") -(defvar unicode-tokens-token-prefix "&" - "Prefix for start of tokens to insert.") +(defvar unicode-tokens-token-format "%s" + "Format string for formatting token a name into a token. +Will be regexp quoted for matching. Not used for matching if +`unicode-tokens-token-variant-format-regexp' is set. +Also used to format shortcuts.") -(defvar unicode-tokens-token-suffix ";" - "Suffix for end of tokens to insert.") +(defvar unicode-tokens-token-variant-format-regexp nil + "A regular expression which matches a token variant. +Will not be regexp quoted, and after format is applied, must -(defvar unicode-tokens-control-token-match nil - "Regexp matching tokens") +An example would be: \\\\(%s\\\\)\\\\(:?\\w+\\\\) -(defvar unicode-tokens-token-match "&\\([A-Za-z]\\);" - "Regexp matching tokens") +which matches plain token strings optionally followed by a colon and +variant name. -(defvar unicode-tokens-hexcode-match "&#[xX]\\([0-9a-fA-F]+\\);" - "Regexp matching numeric token string") +If set, this variable is used instead of `unicode-tokens-token-format'.") +;; (setq ut-tvfr "\\(%s\\)\\(:?\\w+\\)") +;; (string-match (format ut-tvfr ".*?") "alpha:x") -(defvar unicode-tokens-next-character-regexp "&#[xX]\\([0-9a-fA-F]+\\);\\|." - "Regexp matching a logical character following a control code.") +(defvar unicode-tokens-fontsymb-properties nil + "Association list mapping a symbol to a list of text properties. +Used in `unicode-tokens-token-symbol-map', `unicode-tokens-control-regions', +and `unicode-tokens-control-characters'.") -(defvar unicode-tokens-shortcut-alist +(defvar unicode-tokens-shortcut-alist nil "An alist of keyboard shortcuts to unicode strings. The alist is added to the input mode for tokens. Behaviour is much like abbrev.") + ;; -;; Faces +;; Variables that can be overridden in instances: control tokens ;; +;; TODO: docs +(defvar unicode-tokens-control-region-format-regexp nil) +(defvar unicode-tokens-control-char-format-regexp nil) +(defvar unicode-tokens-control-regions nil) +(defvar unicode-tokens-control-characters nil) + +(defvar unicode-tokens-control-region-format-beg nil) +(defvar unicode-tokens-control-region-format-end nil) +(defvar unicode-tokens-control-char-format nil) + +;; +;; A list of the above variables +;; + +(defconst unicode-tokens-configuration-variables + '(token-symbol-map + token-format + token-variant-format-regexp + fontsymb-properties + shortcut-alist + control-region-format-regexp + control-region-format-beg + control-region-format-end + control-char-format-regexp + control-char-format + control-regions + control-characters)) + +;; +;; Variables set in the mode ;; -;; TODO: make these into faces but extract attributes -;; to use in `unicode-tokens-annotation-translations'. -;; Let that be dynamically changeable -;; TODO: choose family acccording to likely architecture and what's available -(cond - ((not (featurep 'xemacs)) + +(defvar unicode-tokens-token-list nil + "List of usable token names in order from `unicode-tokens-token-symbol-map'.") + +(defvar unicode-tokens-hash-table nil + "Hash table mapping token names (strings) to composition and properties.") + +(defvar unicode-tokens-token-match-regexp nil + "Regular expression used by font-lock to match tokens.") + +(defvar unicode-tokens-uchar-hash-table nil + "Hash table mapping unicode strings to symbolic token names. +This is used for an approximate reverse mapping, see `unicode-tokens-paste'.") + +(defvar unicode-tokens-uchar-regexp nil + "Regular expression matching converted tokens. +This is used for an approximate reverse mapping, see `unicode-tokens-paste'.") + + + +;; +;; Constants +;; + +(defgroup unicode-tokens-faces nil + "The faces used in Unicode Tokens mode." + :group 'faces) + (defface unicode-tokens-script-font-face (cond ((eq window-system 'x) ; Linux/Unix - '((t :family "URW Chancery L"))) + '((t :family "PakTypeNaqsh"))) ; ((or ; Mac (eq window-system 'ns) (eq window-system 'carbon)) '((t :family "Lucida Calligraphy")))) - "Script font face") + "Script font face" + :group 'unicode-tokens-faces) (defface unicode-tokens-fraktur-font-face (cond @@ -122,7 +168,8 @@ Behaviour is much like abbrev.") (eq window-system 'ns) (eq window-system 'carbon)) '((t :family "Lucida Blackletter")))) - "Fraktur font face") + "Fraktur font face" + :group 'unicode-tokens-faces) (defface unicode-tokens-serif-font-face (cond @@ -132,220 +179,166 @@ Behaviour is much like abbrev.") (eq window-system 'ns) (eq window-system 'carbon)) '((t :family "Lucida")))) - "Serif (roman) font face"))) + "Serif (roman) font face" + :group 'unicode-tokens-faces) +(defconst unicode-tokens-font-lock-extra-managed-props + '(composition help-echo display invisible) + "Value for `font-lock-extra-managed-props' here.") ;; -;; Variables initialised in unicode-tokens-initialise +;;; Code: ;; -(defvar unicode-tokens-max-token-length 10 - "Maximum length of a token in underlying encoding.") - -(defvar unicode-tokens-codept-charname-alist nil - "Alist mapping unicode code point to character names.") +(defun unicode-tokens-font-lock-keywords () + "Calculate and return value for `font-lock-keywords'. +This function also initialises the important tables for the mode." + ;; Credit to Stefan Monnier for much slimmer original version + (let ((hash (make-hash-table :test 'equal)) + (ucharhash (make-hash-table :test 'equal)) + toks uchars) + (dolist (x unicode-tokens-token-symbol-map) + (let ((tok (car x)) + (comp (cadr x))) + (when (unicode-tokens-usable-composition comp) + (unless (gethash tok hash) + (puthash tok (cdr x) hash) + (push tok toks) + (if (stringp comp) ;; reverse map only for string comps + (unless (or (gethash comp ucharhash) + ;; ignore plain chars for reverse map + (string-match "[a-zA-Z0-9]+" comp)) + (push comp uchars) + (puthash comp tok ucharhash))))))) + (when toks + (setq unicode-tokens-hash-table hash) + (setq unicode-tokens-uchar-hash-table ucharhash) + (setq unicode-tokens-token-list (reverse toks)) + (setq unicode-tokens-uchar-regexp (regexp-opt uchars)) + (setq unicode-tokens-token-match-regexp + (if unicode-tokens-token-variant-format-regexp + (format unicode-tokens-token-variant-format-regexp + (regexp-opt toks t)) + (regexp-opt (mapcar (lambda (tok) + (format unicode-tokens-token-format tok)) + toks) t))) + (cons + `(,unicode-tokens-token-match-regexp + (0 (unicode-tokens-help-echo) 'prepend) + (0 (unicode-tokens-font-lock-compose-symbol + ,(- (regexp-opt-depth unicode-tokens-token-match-regexp) 2)) + 'prepend)) + (unicode-tokens-control-font-lock-keywords))))) + +(defun unicode-tokens-usable-composition (comp) + (cond + ((stringp comp) + (reduce (lambda (x y) (and x (char-displayable-p y))) + comp + :initial-value t)) + ((char-valid-p comp) + (char-displayable-p comp)) + (comp ;; assume any other non-null is OK + t))) + +(defun unicode-tokens-help-echo () + "Return a help-echo text property to display the contents of match string" + (list 'face nil 'help-echo (match-string 0))) + +(defvar unicode-tokens-show-symbols nil + "Non-nil to reveal symbol (composed) tokens instead of compositions.") + +(defun unicode-tokens-font-lock-compose-symbol (match) + "Compose a sequence of chars into a symbol, maybe returning a face property. +Regexp match data number MATCH selects the token name, while 0 matches the +whole expression. +Token symbol is searched for in `unicode-tokens-hash-table'." + (let* ((start (match-beginning 0)) + (end (match-end 0)) + (compps (gethash (match-string match) + unicode-tokens-hash-table)) + (props (cdr-safe compps))) + (if (and compps (not unicode-tokens-show-symbols)) + (compose-region start end (car compps))) + (if props + (add-text-properties ;; font-lock should do this but fails? + start end (unicode-tokens-symbs-to-props props))) + nil)) + +(defun unicode-tokens-show-symbols (&optional arg) + "Toggle `unicode-tokens-show-symbols'. With ARG, turn on iff positive." + (interactive "P") + (setq unicode-tokens-show-symbols + (if (null arg) (not unicode-tokens-show-symbols) + (> (prefix-numeric-value arg) 0))) + (font-lock-fontify-buffer)) + +(defun unicode-tokens-symbs-to-props (symbs &optional facenil) + (let (props p) + (dolist (s symbs) + (setq p (car-safe + (cdr-safe (assoc s unicode-tokens-fontsymb-properties)))) + (if (consp p) + (setq props (cons (car p) (cons (cadr p) props))) + (setq props (cons p props)))) + (if (and facenil + (not (memq 'face props))) + (setq props (append '(face nil) props))) + props)) -(defvar unicode-tokens-token-alist nil - "Mapping of tokens to Unicode strings. -Also used as a flag to detect if `unicode-tokens-initialise' has been called.") +;; +;; Control tokens: as "characters" CTRL <stuff> +;; and regions BEGINCTRL <stuff> ENDCTRL +;; -(defvar unicode-tokens-ustring-alist nil - "Mapping of Unicode strings to tokens.") +(defvar unicode-tokens-show-controls nil + "Non-nil supresses hiding of control tokens.") +(defun unicode-tokens-show-controls (&optional arg) + "Toggle `unicode-tokens-show-controls'. With ARG, turn on iff positive." + (interactive "P") + (setq unicode-tokens-show-controls + (if (null arg) (not unicode-tokens-show-controls) + (> (prefix-numeric-value arg) 0))) + (when unicode-tokens-show-controls + (remove-from-invisibility-spec 'unicode-tokens-show-controls)) + (when (not unicode-tokens-show-controls) + (add-to-invisibility-spec 'unicode-tokens-show-controls))) + +(defun unicode-tokens-control-char (name s &rest props) + `(,(format unicode-tokens-control-char-format-regexp s) + (1 '(face nil invisible unicode-tokens-show-controls) prepend) + (2 ',(unicode-tokens-symbs-to-props props t) prepend))) + +(defun unicode-tokens-control-region (name start end &rest props) + `(,(format unicode-tokens-control-region-format-regexp start end) + (1 '(face nil invisible unicode-tokens-show-controls) prepend) + (2 ',(unicode-tokens-symbs-to-props props t) prepend) + (3 '(face nil invisible unicode-tokens-show-controls) prepend))) + +(defun unicode-tokens-control-font-lock-keywords () + (append + (mapcar (lambda (args) (apply 'unicode-tokens-control-char args)) + unicode-tokens-control-characters) + (mapcar (lambda (args) (apply 'unicode-tokens-control-region args)) + unicode-tokens-control-regions))) ;; -;;; Code: +;; Shortcuts for typing, using quail ;; - -(defun unicode-tokens-insert-char (arg codepoint) - "Insert the Unicode character identified by CODEPOINT. -If ARG is non-nil, ignore available glyphs." - (let ((glyph (memq codepoint unicode-tokens-glyph-list))) - (cond - ((and (decode-char 'ucs codepoint) (or arg glyph)) - (ucs-insert codepoint)) ;; glyph converted to token on save - (t - (insert (format unicode-tokens-charref-format codepoint)))))) - -(defun unicode-tokens-insert-string (arg ustring) - "Insert a Unicode string. -If a prefix is given, the string will be inserted regardless -of whether or not it has displayable glyphs; otherwise, a -numeric character reference for whichever codepoints are not -in the unicode-tokens-glyph-list." - (mapcar (lambda (char) - (unicode-tokens-insert-char arg char)) - ustring)) - -(defun unicode-tokens-character-insert (arg &optional argname) - "Insert a Unicode character by character name, with completion. -If a prefix is given, the character will be inserted regardless -of whether or not it has a displayable glyph; otherwise, a -numeric character reference is inserted if the codepoint is not -in the `unicode-tokens-glyph-list'. If argname is given, it is used for -the prompt. If argname uniquely identifies a character, that -character is inserted without the prompt." - (interactive "P") - (let* ((completion-ignore-case t) - (uniname (if (stringp argname) argname "")) - (charname - (if (eq (try-completion uniname unicode-chars-alist) t) - uniname - (completing-read - "Unicode name: " - unicode-chars-alist - nil t uniname))) - codepoint glyph) - (setq codepoint (cdr (assoc charname unicode-chars-alist))) - (unicode-tokens-insert-char arg codepoint))) - -(defun unicode-tokens-token-insert (arg &optional argname) - "Insert a Unicode string by a token name, with completion. -If a prefix is given, the string will be inserted regardless -of whether or not it has displayable glyphs; otherwise, a -numeric character reference for whichever codepoints are not -in the unicode-tokens-glyph-list. If argname is given, it is used for -the prompt. If argname uniquely identifies a character, that -character is inserted without the prompt." - (interactive "P") - (let* ((stokname (if (stringp argname) argname "")) - (tokname - (if (eq (try-completion stokname unicode-tokens-token-name-alist) t) - stokname - (completing-read - "Token name: " - unicode-tokens-token-name-alist - nil t stokname))) - charname ustring) - (setq ustring (cdr (assoc tokname unicode-tokens-token-name-alist))) - (unicode-tokens-insert-string arg ustring))) - -(defun unicode-tokens-replace-token-after (length) - (let ((bpoint (point)) ustring) - (save-excursion - (forward-char length) - (save-match-data - (while (re-search-backward - unicode-tokens-token-match - (max (- bpoint unicode-tokens-max-token-length) - (point-min)) t nil) - (setq ustring - (assoc (match-string 1) unicode-tokens-token-name-alist)) - (if ustring ;; TODO: should check on glyphs here - (progn - (let ((matchlen (- (match-end 0) (match-beginning 0)))) - (replace-match (replace-quote (cdr ustring))) - ;; was: (format "%c" (decode-char 'ucs (cadr codept))) - (setq length - (+ (- length matchlen) (length (cdr ustring))))))))))) - length) - - -;;stolen from hen.el which in turn claims to have stolen it from cxref -(defun unicode-tokens-looking-backward-at (regexp) - "Return t if text before point matches regular expression REGEXP. -This function modifies the match data that `match-beginning', -`match-end' and `match-data' access; save and restore the match -data if you want to preserve them." - (save-excursion - (let ((here (point))) - (if (re-search-backward regexp (point-min) t) - (if (re-search-forward regexp here t) - (= (point) here)))))) - -;; TODO: make this work for control tokens. -;; But it's a bit nasty and introduces font-lock style complexity again. -;; Better if we stick with dedicated input methods. -(defun unicode-tokens-electric-suffix () - "Detect tokens and replace them with the appropriate string. -This is bound to the character ending `unicode-tokens-token-suffix' -if there is such a unique character." - (interactive) - (let ((pos (point)) - (case-fold-search nil) - amppos codept ustring) - (search-backward unicode-tokens-token-prefix nil t nil) - (setq amppos (point)) - (goto-char pos) - (cond - ((unicode-tokens-looking-backward-at unicode-tokens-token-match) - (progn - (re-search-backward unicode-tokens-token-match nil t nil) - (if (= amppos (point)) - (progn - (setq ustring - (assoc (match-string 1) - unicode-tokens-token-name-alist)) - (if ustring ;; todo: check glyphs avail/use insert fn - (replace-match (replace-quote (cdr ustring))) - ;; was (format "%c" (decode-char 'ucs (cdr codept)))) - (progn - (goto-char pos) - (insert unicode-tokens-token-suffix)))) - (progn - (goto-char pos) - (insert unicode-tokens-token-suffix))))) - ((unicode-tokens-looking-backward-at unicode-tokens-hexcode-match) - (progn - (re-search-backward unicode-tokens-hexcode-match nil t nil) - (if (= amppos (point)) - (progn - (setq codept (string-to-number (match-string 1) 16)) - (if ;; todo : check glyph (memq codept unicode-tokens-glyph-list) - codept - (replace-match (format "%c" (decode-char 'ucs (cdr codept)))) - (progn - (goto-char pos) - (insert unicode-tokens-token-suffix)))) - (progn - (goto-char pos) - (insert unicode-tokens-token-suffix))))) - (t - (insert unicode-tokens-token-suffix))))) - -(defvar unicode-tokens-rotate-glyph-last-char nil) - -(defun unicode-tokens-rotate-glyph-forward (&optional n) - "Rotate the character before point in the current code page, by N steps. -If no character is found at the new codepoint, no change is made. -This function may only work reliably for GNU Emacs >= 23." - (interactive "p") - (if (> (point) (point-min)) - (let* ((codept (or (if (or (eq last-command - 'unicode-tokens-rotate-glyph-forward) - (eq last-command - 'unicode-tokens-rotate-glyph-backward)) - unicode-tokens-rotate-glyph-last-char) - (char-before (point)))) - (page (/ codept 256)) - (pt (mod codept 256)) - (newpt (mod (+ pt (or n 1)) 256)) - (newcode (+ (* 256 page) newpt)) - (newname (assoc newcode - unicode-tokens-codept-charname-alist)) - ;; NOTE: decode-char 'ucs here seems to fail on Emacs <23 - (newchar (decode-char 'ucs newcode))) - (when (and newname newchar) - (delete-char -1) - (insert-char newchar 1) - (message (cdr newname)) - (setq unicode-tokens-rotate-glyph-last-char nil)) - (unless (and newname newchar) - (message "No character at code %d" newcode) - (setq unicode-tokens-rotate-glyph-last-char newcode))))) - -(defun unicode-tokens-rotate-glyph-backward (&optional n) - "Rotate the character before point in the current code page, by -N steps. -If no character is found at the new codepoint, no change is made. -This function may only work reliably for GNU Emacs >= 23." - (interactive "p") - (unicode-tokens-rotate-glyph-forward (if n (- n) -1))) +(defvar unicode-tokens-use-shortcuts t + "Non-nil means use `unicode-tokens-shortcut-alist' if set.") - -;; -;; Setup quail for Unicode tokens mode -;; +(defun unicode-tokens-use-shortcuts (&optional arg) + "Toggle `unicode-tokens-use-shortcuts'. With ARG, turn on iff positive." + (interactive "P") + (setq unicode-tokens-use-shortcuts + (if (null arg) (not unicode-tokens-use-shortcuts) + (> (prefix-numeric-value arg) 0))) + (if unicode-tokens-use-shortcuts + (set-input-method "Unicode tokens") + (set-input-method nil))) (require 'quail) @@ -359,57 +352,12 @@ This function may only work reliably for GNU Emacs >= 23." "Ordering on (car S1, car S2): order longer strings first." (>= (length (car s1)) (length (car s2)))) -(defun unicode-tokens-propertise-after-quail (tostring) - (add-text-properties (- (point) (length tostring)) (point) - (list 'utoks tostring))) - - (defun unicode-tokens-quail-define-rules () "Define the token and shortcut input rules. Calculated from `unicode-tokens-token-name-alist' and -`unicode-tokens-shortcut-alist'. -Also sets `unicode-tokens-token-alist'." +`unicode-tokens-shortcut-alist'." (let ((unicode-tokens-quail-define-rules (list 'quail-define-rules))) -;; failed experiment (wrong place for rule/wrong type?): attempt to propertise -;; after translation -;; '((advice . unicode-tokens-propertise-after-quail -;; (face . proof-declaration-name-face))))) - (let ((ulist (copy-list unicode-tokens-token-name-alist)) - ustring tokname token) - ;; sort in case of non-terminated token syntax (empty suffix) - (setq ulist (sort ulist 'unicode-tokens-map-ordering)) - (setq unicode-tokens-token-alist nil) - (while ulist - (setq tokname (caar ulist)) - (setq ustring (cdar ulist)) - (setq token (format unicode-tokens-token-format tokname)) - (cond - ;; Some error checking (but not enough) - ((eq (length tokname) 0) - (warn "Empty token name (mapped to \"%s\") in unicode tokens list" - ustring)) - ((eq (length ustring) 0) - (warn "Empty token mapping, ignoring token \"%s\" in unicode tokens list" - token)) - ((assoc token unicode-tokens-token-alist) - (warn "Duplicated token entry, ignoring subsequent mapping of %s" token)) - ((rassoc ustring unicode-tokens-token-alist) - (warn "Duplicated target \"%s\", ignoring token %s" ustring token)) - (t - (nconc unicode-tokens-quail-define-rules - (list (list token - (vector ustring)))) - (setq unicode-tokens-token-alist - (nconc unicode-tokens-token-alist - (list (cons token ustring)))))) - (setq ulist (cdr ulist)))) - ;; make reverse map: convert longer ustring sequences first - (setq unicode-tokens-ustring-alist - (sort - (mapcar (lambda (c) (cons (cdr c) (car c))) - unicode-tokens-token-alist) - 'unicode-tokens-map-ordering)) (let ((ulist (copy-list unicode-tokens-shortcut-alist)) ustring shortcut) (setq ulist (sort ulist 'unicode-tokens-map-ordering)) @@ -423,379 +371,329 @@ Also sets `unicode-tokens-token-alist'." (eval unicode-tokens-quail-define-rules))) - ;; -;; File format for saving tokens in plain ASCII. +;; User-level functions ;; -(defvar unicode-tokens-format-entry - '(unicode-tokens "Tokens encoding unicode characters." - nil - unicode-tokens-tokens-to-unicode ; decode - unicode-tokens-unicode-to-tokens ; encode - t nil) - "Value for `format-alist'.") - -(add-to-list 'format-alist unicode-tokens-format-entry) - -(defconst unicode-tokens-ignored-properties - '(vanilla type fontified face auto-composed - rear-nonsticky field inhibit-line-move-field-capture - utoks) - "Text properties to ignore when saving files.") - -(put 'font-lock-face 'format-list-valued t) - -(defconst unicode-tokens-annotation-translations - `((font-lock-face - ;; FIXME: this is faulty; format.el makes wrong calculations with - ;; list valued properties, and sometimes loses these settings. - ((:weight bold) "bold") - ((:slant italic) "italic") - ; ,(face-all-attributes 'unicode-tokens-script-font-face) "script") - ; ,(face-all-attributes 'unicode-tokens-fraktur-font-face) "fraktur") - ; ,(face-all-attributes 'unicode-tokens-serif-font-face) "serif") - ((:family "PakTypeNaqsh") "script") - ((:family "URW Bookman L") "fraktur") - ((:family "Liberation Serif") "serif") - (proof-declaration-name-face "loc1") - (default )) - (display - ((raise 0.4) "superscript") - ((raise -0.4) "subscript") - ((raise 0.35) "superscript1") - ((raise -0.35) "subscript1") - ((raise 0.3) "idsuperscript1") - ((raise -0.3) "idsubscript1") - (default ))) - "Text property table for annotations.") - - -(defun unicode-tokens-remove-properties (start end) - "Remove text properties we manage between START and END." - (remove-text-properties - ;; NB: this is approximate and clashes with anyone else who - ;; looks after font-lock-face or display - start end (mapcar 'car unicode-tokens-annotation-translations))) - - -(defun unicode-tokens-tokens-to-unicode (&optional start end) - "Decode a tokenised file for display in Emacs." - (save-excursion - (save-restriction - (narrow-to-region start (or end (point-max))) - (let ((case-fold-search proof-case-fold-search) - (buffer-undo-list t) - (modified (buffer-modified-p)) - (inhibit-read-only t)) - (setq unicode-tokens-next-control-token-seen-token nil) - (format-replace-strings unicode-tokens-token-alist nil (point-min) - (point-max)) -;; alternative experiment: store original tokens inside text properties -;; (unicode-tokens-replace-strings-propertise unicode-tokens-token-alist) - (format-deannotate-region (point-min) - (point-max) - unicode-tokens-annotation-translations - 'unicode-tokens-next-control-token) - (set-buffer-modified-p modified)) - (goto-char (point-max))))) - -(defvar unicode-tokens-next-control-token-seen-token nil - "Records currently open single-character control token.") - -(defun unicode-tokens-next-control-token () - "Find next control token and interpret it. -If `unicode-tokens-next-control-token' is non-nil, end current control sequence -after next character (single character control sequence)." - (let (result) - (when unicode-tokens-next-control-token-seen-token - (if (re-search-forward unicode-tokens-next-character-regexp nil t) - (setq result (list (match-end 0) (match-end 0) - unicode-tokens-next-control-token-seen-token - nil))) - (setq unicode-tokens-next-control-token-seen-token nil)) - (while (and (not result) - (re-search-forward unicode-tokens-control-token-match nil t)) - (let* - ((tok (match-string 1)) - (annot - (cond - ((equal tok "bsup") '("superscript" t)) - ((equal tok "esup") '("superscript" nil)) - ((equal tok "bsub") '("subscript" t)) - ((equal tok "esub") '("subscript" nil)) - ((equal tok "bbold") '("bold" t)) - ((equal tok "ebold") '("bold" nil)) - ((equal tok "bitalic") '("italic" t)) - ((equal tok "eitalic") '("italic" nil)) - ((equal tok "bscript") '("script" t)) - ((equal tok "escript") '("script" nil)) - ((equal tok "bfrak") '("fraktur" t)) - ((equal tok "efrak") '("fraktur" nil)) - ((equal tok "bserif") '("serif" t)) - ((equal tok "eserif") '("serif" nil)) - ((equal tok "loc") - (list (setq unicode-tokens-next-control-token-seen-token - "loc1") t)) - ((equal tok "sup") - (list (setq unicode-tokens-next-control-token-seen-token - "superscript1") t)) - ((equal tok "sub") - (list (setq unicode-tokens-next-control-token-seen-token - "subscript1") t)) - ((equal tok "isup") - (list (setq unicode-tokens-next-control-token-seen-token - "idsuperscript1") t)) - ((equal tok "isub") - (list (setq unicode-tokens-next-control-token-seen-token - "idsubscript1") t))))) - (if annot - (setq result - (append - (list (match-beginning 0) (match-end 0)) - annot))))) - result)) - -;; TODO: this should be instance specific -(defconst unicode-tokens-annotation-control-token-alist - '(("bold" . ("bbold" . "ebold")) - ("subscript" . ("bsub" . "esub")) - ("superscript" . ("bsup" . "esup")) - ("subscript1" . ("sub")) - ("superscript1" . ("sup")) - ("idsubscript1" . ("isub")) - ("idsuperscript1" . ("isup")) - ("loc1" . ("loc")) - ;; non-standard - ("italic" . ("bitalic" . "eitalic")) - ("script" . ("bscript" . "escript")) - ("fraktur" . ("bfrak" . "efrak")) - ("serif" . ("bserif" . "eserif")))) - -(defun unicode-tokens-make-token-annotation (annot positive) - "Encode a text property start/end by adding an annotation in the file." - (let ((toks (cdr-safe - (assoc annot unicode-tokens-annotation-control-token-alist)))) - (cond - ((and toks positive) - (format unicode-tokens-control-token-format (car toks))) - ((and toks (cdr toks)) - (format unicode-tokens-control-token-format (cdr toks))) - (t "")))) - -(defun unicode-tokens-find-property (name) - (let ((props unicode-tokens-annotation-translations) - prop vals val vname) - (catch 'return - (while props - (setq prop (caar props)) - (setq vals (cdar props)) - (while vals - (setq val (car vals)) - (if (member name (cdr val)) - (throw 'return (list prop (car val)))) - (setq vals (cdr vals))) - (setq props (cdr props)))))) - -(defun unicode-tokens-annotate-region (beg end &optional annot) +(defun unicode-tokens-insert-token (tok) + "Insert symbolic token named TOK, giving a message." + (interactive (list + (completing-read + "Insert token: " + unicode-tokens-hash-table) t)) + (let ((ins (format unicode-tokens-token-format tok))) + (insert ins) + (message "Inserted %s" ins))) + +(defun unicode-tokens-annotate-region (name) + "Annotate region with region markup tokens for scheme NAME." + (interactive (let ((completion-ignore-case t)) + (list (completing-read + "Annotate region with: " + unicode-tokens-control-regions nil + 'requirematch)))) + (assert (assoc name unicode-tokens-control-regions)) + (let* ((entry (assoc name unicode-tokens-control-regions)) + (beg (region-beginning)) + (end (region-end)) + (begtok + (format unicode-tokens-control-region-format-end (nth 1 entry))) + (endtok + (format unicode-tokens-control-region-format-end (nth 2 entry)))) + (when (> beg end) + (setq beg end) + (setq end (region-beginning))) + (goto-char beg) + (insert begtok) + (goto-char (+ end (- (point) beg))) + (insert endtok))) + +(defun unicode-tokens-insert-control (name) + (interactive (list (completing-read + "Insert control symbol: " + unicode-tokens-control-characters))) + (insert (format unicode-tokens-control-char-format name))) + +(defun unicode-tokens-insert-uchar-as-token (char) + "Insert CHAR as a symbolic token, if possible." + (let ((tok (gethash char unicode-tokens-uchar-hash-table))) + (when tok + (unicode-tokens-insert-token tok)))) + +;;unused +(defun unicode-tokens-delete-token-at-point () + (interactive) + (when (looking-at unicode-tokens-token-match-regexp) + (kill-region (match-beginning 0) (match-end 0)))) + +(defvar unicode-tokens-rotate-token-last-token nil) + +(defun unicode-tokens-prev-token () + (let ((match (re-search-backward unicode-tokens-token-match-regexp + (save-excursion + (beginning-of-line 0) (point)) t))) + (if match + (match-string + (1- (regexp-opt-depth unicode-tokens-token-match-regexp)))))) + +(defun unicode-tokens-rotate-token-forward (&optional n) + "Rotate the token before point by N steps in the table." + (interactive "p") + (if (> (point) (point-min)) + (save-match-data + (let* ((token (or (if (or (eq last-command + 'unicode-tokens-rotate-token-forward) + (eq last-command + 'unicode-tokens-rotate-token-backward)) + unicode-tokens-rotate-token-last-token) + (unicode-tokens-prev-token))) + (tokennumber + (if token + (search (list token) unicode-tokens-token-list :test 'equal))) + (numtoks + (hash-table-count unicode-tokens-hash-table)) + (newtok + (if tokennumber + (nth (mod (+ tokennumber (or n 1)) numtoks) + unicode-tokens-token-list)))) + (when (and newtok + (looking-at unicode-tokens-token-match-regexp)) + (delete-region (match-beginning 0) (match-end 0)) + (insert (format unicode-tokens-token-format newtok))))))) + +(defun unicode-tokens-rotate-token-backward (&optional n) + "Rotate the token before point, by -N steps in the token list." + (interactive "p") + (unicode-tokens-rotate-token-forward (if n (- n) -1))) + +(defun unicode-tokens-copy-token (tokname) + (interactive "s") + (kill-new + (format unicode-tokens-token-format tokname) + (eq last-command 'unicode-tokens-copy-token))) + +(define-button-type 'unicode-tokens-list + 'help-echo "mouse-2, RET: copy this character" + 'face nil + 'action #'(lambda (button) + (unicode-tokens-copy-token (button-get button 'unicode-token)))) + +;; TODO: improve layout, can we use tabs +(defun unicode-tokens-list-tokens () + "Show a buffer of all tokens." + (interactive) + (with-output-to-temp-buffer "*Unicode Tokens List*" + (with-current-buffer standard-output + (unicode-tokens-mode) + (insert "Click or RET on a character to copy into kill ring.\n\n") + (let ((count 0) toks) + ;; display in originally given order + (dolist (tok unicode-tokens-token-list) + (insert-text-button + (format unicode-tokens-token-format tok) + :type 'unicode-tokens-list + 'unicode-token tok) + (incf count) + (if (< count 10) + (insert "\t") + (insert "\n") + (setq count 0))))))) + + +(defun unicode-tokens-copy (beg end) + "Copy presentation of region between BEG and END. +This is an approximation; it makes assumptions about the behaviour +of symbol compositions, and will lose layout information." (interactive "r") - (or annot - (if (interactive-p) - (setq annot - (completing-read "Annotate region as: " - unicode-tokens-annotation-control-token-alist - nil t)) - (error "In unicode-tokens-annotation-control-token-alist: TYPE must be given."))) - (add-text-properties beg end - (unicode-tokens-find-property annot))) - -(defun unicode-tokens-annotate-region-with (annot) - `(lambda (beg end) - (interactive "r") - (unicode-tokens-annotate-region beg end ,annot))) - -(defun unicode-tokens-annotate-string (annot string) - (add-text-properties 0 (length string) - (unicode-tokens-find-property annot) - string) - string) - -(defun unicode-tokens-unicode-to-tokens (&optional start end buffer) - "Encode a buffer to save as a tokenised file." - (let ((case-fold-search proof-case-fold-search) - (buffer-undo-list t) - (modified (buffer-modified-p))) - (save-restriction - (save-excursion - (narrow-to-region (or start (point-min)) (or end (point-max))) - (format-insert-annotations - (format-annotate-region (point-min) (point-max) - unicode-tokens-annotation-translations - 'unicode-tokens-make-token-annotation - unicode-tokens-ignored-properties)) -;; alternative experiment: store original tokens inside text properties -;; (unicode-tokens-replace-strings-unpropertise) - (format-replace-strings unicode-tokens-ustring-alist - nil (point-min) (point-max)) - (set-buffer-modified-p modified))))) - - -(defun unicode-tokens-replace-strings-propertise (alist &optional beg end) - "Do multiple replacements on the buffer. -ALIST is a list of (FROM . TO) pairs, which should be proper arguments to -`search-forward' and `replace-match', respectively. -The original contents FROM are retained in the buffer in the text property `utoks'. -Optional args BEG and END specify a region of the buffer on which to operate." - (save-excursion - (save-restriction - (or beg (setq beg (point-min))) - (if end (narrow-to-region (point-min) end)) - (while alist - (let ((from (car (car alist))) - (to (cdr (car alist))) - (case-fold-search nil)) - (goto-char beg) - (while (search-forward from nil t) - (goto-char (match-beginning 0)) - (insert to) - (set-text-properties (- (point) (length to)) (point) - (cons 'utoks - (cons from - (text-properties-at (point))))) - (delete-region (point) (+ (point) (- (match-end 0) - (match-beginning 0))))) - (setq alist (cdr alist))))))) - -;; NB: this is OK, except that now if we edit with raw symbols, we -;; don't get desired effect but instead rely on hidden annotations. -;; Also doesn't work as easily with quail. -;; Can we have a sensible mixture of both things? -(defun unicode-tokens-replace-strings-unpropertise (&optional beg end) - "Reverse the effect of `unicode-tokens-replace-strings-unpropertise'. -Replaces contiguous text with 'utoks' property with property value." - (let ((pos (or beg (point-min))) - (lim (or end (point-max))) - start to) - (save-excursion - (while (and - (setq pos (next-single-property-change pos 'utoks nil lim)) - (< pos lim)) - (if start - (progn - (setq to (get-text-property start 'utoks)) - (goto-char start) - (insert to) - (set-text-properties start (point) - (text-properties-at start)) - (delete-region (point) (+ (point) (- pos start))) - (setq start nil)) - (setq start pos)))))) - - - - + ;; cf kill-ring-save, uncode-tokens-font-lock-compose-symbol + (let ((visible + ;; actually: leave in control tokens as they can have logical meaning + ;; (proof-visible-buffer-substring beg end) + (buffer-substring-no-properties beg end)) + (match (- (regexp-opt-depth unicode-tokens-token-match-regexp) 2))) + (with-temp-buffer + (insert visible) + (goto-char (point-min)) + (while (re-search-forward unicode-tokens-token-match-regexp nil t) + ;; TODO: interpret more exotic compositions here + (let* ((tstart (match-beginning 0)) + (tend (match-end 0)) + (comp (car-safe + (gethash (match-string match) + unicode-tokens-hash-table)))) + (when comp + (delete-region tstart tend) + ;; TODO: improve this: interpret vector, strip tabs + (insert comp)))) ;; gross approximation to compose-region + (copy-region-as-kill (point-min) (point-max))))) + +(defun unicode-tokens-paste () + (interactive) + (let ((start (point)) end) + (clipboard-yank) + (setq end (point-marker)) + (while (re-search-backward unicode-tokens-uchar-regexp start t) + (let* ((useq (match-string 0)) + (token (gethash useq unicode-tokens-uchar-hash-table)) + (pos (point))) + (when token + (replace-match (format unicode-tokens-token-format token) t t) + (goto-char pos)))) + (goto-char end) + (set-marker end nil))) ;; ;; Minor mode ;; +;;;###autoload +(defun unicode-tokens-initialise () + (interactive) + (let ((flks (unicode-tokens-font-lock-keywords))) + (put 'unicode-tokens-font-lock-keywords major-mode flks) + (unicode-tokens-quail-define-rules) + flks)) + (defvar unicode-tokens-mode-map (make-sparse-keymap) "Key map used for Unicode Tokens mode.") +;;;###autoload (define-minor-mode unicode-tokens-mode "Minor mode for unicode token input." nil " Utoks" unicode-tokens-mode-map - (unless unicode-tokens-token-alist - (unicode-tokens-initialise)) - (when unicode-tokens-mode - (when (boundp 'text-property-default-nonsticky) - (make-variable-buffer-local 'text-property-default-nonsticky) - (setq text-property-default-nonsticky - ;; We want to use display property with stickyness - (delete '(display . t) text-property-default-nonsticky))) - (if (and - (fboundp 'set-buffer-multibyte) - (not (buffer-base-buffer))) - (set-buffer-multibyte t)) - (let ((inhibit-read-only t)) - ;; format is supposed to manage undo, but doesn't remap - (setq buffer-undo-list nil) - (format-decode-buffer 'unicode-tokens)) - (set-input-method "Unicode tokens")) - (unless unicode-tokens-mode - (when (boundp 'text-property-default-nonsticky) - (add-to-list 'text-property-default-nonsticky '(display . t))) - ;; leave buffer encoding as is - (let ((inhibit-read-only t) - (modified (buffer-modified-p))) - ;; format is supposed to manage undo, but doesn't remap - (setq buffer-undo-list nil) - (format-encode-buffer 'unicode-tokens) - (unicode-tokens-remove-properties (point-min) (point-max)) - (set-buffer-modified-p modified)) - (inactivate-input-method))) + (let ((flks (get 'unicode-tokens-font-lock-keywords major-mode))) + (when unicode-tokens-mode + (unless flks + (setq flks (unicode-tokens-initialise))) + (make-local-variable 'font-lock-extra-managed-props) + ;; make sure buffer can display 16 bit chars + (if (and + (fboundp 'set-buffer-multibyte) + (not (buffer-base-buffer))) + (set-buffer-multibyte t)) + + (add-to-invisibility-spec 'unicode-tokens-show-controls) + + ;; our conventions: + ;; 1. set default for font-lock-extra-managed-props + ;; as property on major mode symbol (ordinarily nil). + (font-lock-add-keywords nil flks) + + (setq font-lock-extra-managed-props + (get 'font-lock-extra-managed-props major-mode)) + (mapcar + (lambda (p) (add-to-list 'font-lock-extra-managed-props p)) + unicode-tokens-font-lock-extra-managed-props) + + (font-lock-fontify-buffer) + + (if unicode-tokens-use-shortcuts + (set-input-method "Unicode tokens")) + + ;; adjust maths menu to insert tokens + (set (make-local-variable 'maths-menu-filter-predicate) + (lambda (uchar) (gethash uchar unicode-tokens-uchar-hash-table))) + (set (make-local-variable 'maths-menu-tokenise-insert) + (lambda (uchar) + (unicode-tokens-insert-token + (gethash uchar unicode-tokens-uchar-hash-table))))) + + (when (not unicode-tokens-mode) + (when flks + (font-lock-unfontify-buffer) + (setq font-lock-extra-managed-props + (get 'font-lock-extra-managed-props major-mode)) + (setq font-lock-set-defaults nil) ; force font-lock-set-defaults to reinit + (font-lock-fontify-buffer) + (set-input-method nil)) + + ;; Remove hooks from maths menu + (kill-local-variable 'maths-menu-filter-predicate) + (kill-local-variable 'maths-menu-tokenise-insert)))) ;; -;; Initialisation +;; Key bindings ;; -(defun unicode-tokens-initialise () - "Initialise tables." - ;; Calculate max token length - (let ((tlist unicode-tokens-token-name-alist) - (len 0) tok) - (while tlist - (when (> (length (caar tlist)) 0) - (setq len (length (caar tlist))) - (setq tok (caar tlist))) - (setq tlist (cdr tlist))) - (setq unicode-tokens-max-token-length - (length (format unicode-tokens-token-format tok)))) - ;; Names from code points - (setq unicode-tokens-codept-charname-alist - (mapcar (lambda (namechar) - (cons (cdr namechar) (car namechar))) - unicode-chars-alist)) - ;; Default assumed available glyph list based on tokens; - ;; TODO: filter with what's really available, if can find out. - ;; TODO: allow altering of this when the token-name-alist is reset - ;; in proof-token-name-alist (unless test here is for specific setting) - (unless unicode-tokens-glyph-list - (setq unicode-tokens-glyph-list - (reduce (lambda (glyphs tokustring) - (append glyphs (string-to-list (cdr tokustring)))) - unicode-tokens-token-name-alist - :initial-value nil))) - (unicode-tokens-quail-define-rules) - ;; Key bindings - (if (= (length unicode-tokens-token-suffix) 1) - (define-key unicode-tokens-mode-map - (vector (string-to-char unicode-tokens-token-suffix)) - 'unicode-tokens-electric-suffix)) - (define-key unicode-tokens-mode-map [(control ?,)] - 'unicode-tokens-rotate-glyph-backward) - (define-key unicode-tokens-mode-map [(control ?.)] - 'unicode-tokens-rotate-glyph-forward) - ) +(define-key unicode-tokens-mode-map [(control ?,)] + 'unicode-tokens-rotate-token-backward) +(define-key unicode-tokens-mode-map [(control ?.)] + 'unicode-tokens-rotate-token-forward) +(define-key unicode-tokens-mode-map + [(control c) (control t) (control t)] 'unicode-tokens-insert-token) +(define-key unicode-tokens-mode-map + [(control c) (control t) (control r)] 'unicode-tokens-annotate-region) +(define-key unicode-tokens-mode-map + [(control c) (control t) (control e)] 'unicode-tokens-insert-control) +(define-key unicode-tokens-mode-map + [(control c) (control t) (control z)] 'unicode-tokens-show-symbols) +(define-key unicode-tokens-mode-map + [(control c) (control t) (control x)] 'unicode-tokens-show-controls) + ;; ;; Menu ;; (easy-menu-define unicode-tokens-menu unicode-tokens-mode-map - "Format menu" - (cons "Format" - (mapcar - (lambda (fmt) - (vector fmt - (unicode-tokens-annotate-region-with (downcase fmt)) - :active 'region-exists-p)) - '("Subscript" "Superscript" - "Supscript1" "Superscript1" - "Idsubscript1" "Idsuperscript1" - ;; don't encourage these as saving seems unreliable - ;; "Bold" "Italic" "Script" "Fraktur" "Serif" - )))) - + "Tokens menu" + (cons "Tokens" + (list + ["Insert token..." unicode-tokens-insert-token] + ["Next token" unicode-tokens-rotate-token-forward] + ["Prev token" unicode-tokens-rotate-token-backward] + ["List tokens" unicode-tokens-list-tokens] + (cons "Format char" + (mapcar + (lambda (fmt) + (vector (car fmt) + `(lambda () (interactive) + (apply 'unicode-tokens-insert-control ',(car fmt))) + :help (concat "Format next item as " + (downcase (car fmt))))) + unicode-tokens-control-characters)) + (cons "Format region" + (mapcar + (lambda (fmt) + (vector (car fmt) + `(lambda () (interactive) + (funcall 'unicode-tokens-annotate-region ',(car fmt))) + :help (concat "Format region as " + (downcase (car fmt))) + :active 'mark-active)) + unicode-tokens-control-regions)) + "---" + ["Copy as unicode" unicode-tokens-copy + :active 'mark-active + :help "Copy text from buffer, converting tokens to Unicode"] + ["Paste from unicode" unicode-tokens-paste + :active (and kill-ring (not buffer-read-only)) + :help "Paste from clipboard, converting Unicode to tokens"] + "---" + ["Show control tokens" unicode-tokens-show-controls + :style toggle + :selected unicode-tokens-show-controls + :active (or + unicode-tokens-control-region-format-regexp + unicode-tokens-control-char-format-regexp) + :help "Prevent hiding of control tokens"] + ["Show symbol tokens" unicode-tokens-show-symbols + :style toggle + :selected unicode-tokens-show-symbols + :help "Show tokens for symbols"] + ["Enable shortcuts" unicode-tokens-use-shortcuts + :style toggle + :selected unicode-tokens-use-shortcuts + :active unicode-tokens-shortcut-alist + :help "Use short cuts for typing tokens"] + ["Make fontsets" + (lambda () (interactive) (require 'pg-fontsets)) + :active (not (featurep 'pg-fontsets)) + :help "Define fontsets (for Options->Set fontsets)" + :visible (< emacs-major-version 23) ; not useful on 23 + ]))) + + + (provide 'unicode-tokens) ;;; unicode-tokens.el ends here diff --git a/lib/xml-fixed.el b/lib/xml-fixed.el deleted file mode 100644 index c79bdd64..00000000 --- a/lib/xml-fixed.el +++ /dev/null @@ -1,508 +0,0 @@ -;;; xml.el --- XML parser - -;;; !!! This version has been modified from the version distributed with -;;; XEmacs to fix a bug parsing empty elements, for Proof General. - -;; Copyright (C) 2000, 2001 Free Software Foundation, Inc. - -;; Author: Emmanuel Briot <briot@gnat.com> -;; Maintainer: Emmanuel Briot <briot@gnat.com> -;; Keywords: xml - -;; This file is part of GNU Emacs. - -;; GNU Emacs is free software; you can redistribute it and/or modify -;; it under the terms of the GNU General Public License as published by -;; the Free Software Foundation; either version 2, or (at your option) -;; any later version. - -;; GNU Emacs is distributed in the hope that it will be useful, -;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -;; GNU General Public License for more details. - -;; You should have received a copy of the GNU General Public License -;; along with GNU Emacs; see the file COPYING. If not, write to the -;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, -;; Boston, MA 02111-1307, USA. - -;;; Commentary: - -;; This file contains a full XML parser. It parses a file, and returns a list -;; that can be used internally by any other lisp file. -;; See some example in todo.el - -;;; FILE FORMAT - -;; It does not parse the DTD, if present in the XML file, but knows how to -;; ignore it. The XML file is assumed to be well-formed. In case of error, the -;; parsing stops and the XML file is shown where the parsing stopped. -;; -;; It also knows how to ignore comments, as well as the special ?xml? tag -;; in the XML file. -;; -;; The XML file should have the following format: -;; <node1 attr1="name1" attr2="name2" ...>value -;; <node2 attr3="name3" attr4="name4">value2</node2> -;; <node3 attr5="name5" attr6="name6">value3</node3> -;; </node1> -;; Of course, the name of the nodes and attributes can be anything. There can -;; be any number of attributes (or none), as well as any number of children -;; below the nodes. -;; -;; There can be only top level node, but with any number of children below. - -;;; LIST FORMAT - -;; The functions `xml-parse-file' and `xml-parse-tag' return a list with -;; the following format: -;; -;; xml-list ::= (node node ...) -;; node ::= (tag_name attribute-list . child_node_list) -;; child_node_list ::= child_node child_node ... -;; child_node ::= node | string -;; tag_name ::= string -;; attribute_list ::= (("attribute" . "value") ("attribute" . "value") ...) -;; | nil -;; string ::= "..." -;; -;; Some macros are provided to ease the parsing of this list - -;;; Code: - -(eval-and-compile - (defalias 'match-string-no-properties 'match-string)) - -;;******************************************************************* -;;** -;;** Macros to parse the list -;;** -;;******************************************************************* - -(defsubst xml-node-name (node) - "Return the tag associated with NODE. -The tag is a lower-case symbol." - (car node)) - -(defsubst xml-node-attributes (node) - "Return the list of attributes of NODE. -The list can be nil." - (nth 1 node)) - -(defsubst xml-node-children (node) - "Return the list of children of NODE. -This is a list of nodes, and it can be nil." - (cddr node)) - -(defun xml-get-children (node child-name) - "Return the children of NODE whose tag is CHILD-NAME. -CHILD-NAME should be a lower case symbol." - (let ((match ())) - (dolist (child (xml-node-children node)) - (if child - (if (equal (xml-node-name child) child-name) - (push child match)))) - (nreverse match))) - -(defun xml-get-attribute (node attribute) - "Get from NODE the value of ATTRIBUTE. -An empty string is returned if the attribute was not found." - (if (xml-node-attributes node) - (let ((value (assoc attribute (xml-node-attributes node)))) - (if value - (cdr value) - "")) - "")) - -;;******************************************************************* -;;** -;;** Creating the list -;;** -;;******************************************************************* - -(defun xml-parse-file (file &optional parse-dtd) - "Parse the well-formed XML FILE. -If FILE is already edited, this will keep the buffer alive. -Returns the top node with all its children. -If PARSE-DTD is non-nil, the DTD is parsed rather than skipped." - (let ((keep)) - (if (get-file-buffer file) - (progn - (set-buffer (get-file-buffer file)) - (setq keep (point))) - (find-file file)) - - (let ((xml (xml-parse-region (point-min) - (point-max) - (current-buffer) - parse-dtd))) - (if keep - (goto-char keep) - (kill-buffer (current-buffer))) - xml))) - -(defun xml-parse-region (beg end &optional buffer parse-dtd) - "Parse the region from BEG to END in BUFFER. -If BUFFER is nil, it defaults to the current buffer. -Returns the XML list for the region, or raises an error if the region -is not a well-formed XML file. -If PARSE-DTD is non-nil, the DTD is parsed rather than skipped, -and returned as the first element of the list" - (let (xml result dtd) - (save-excursion - (if buffer - (set-buffer buffer)) - (goto-char beg) - (while (< (point) end) - (if (search-forward "<" end t) - (progn - (forward-char -1) - (if (null xml) - (progn - (setq result (xml-parse-tag end parse-dtd)) - (cond - ((null result)) - ((listp (car result)) - (setq dtd (car result)) - (add-to-list 'xml (cdr result))) - (t - (add-to-list 'xml result)))) - - ;; translation of rule [1] of XML specifications - (error "XML files can have only one toplevel tag"))) - (goto-char end))) - (if parse-dtd - (cons dtd (nreverse xml)) - (nreverse xml))))) - - -(defun xml-parse-tag (end &optional parse-dtd) - "Parse the tag that is just in front of point. -The end tag must be found before the position END in the current buffer. -If PARSE-DTD is non-nil, the DTD of the document, if any, is parsed and -returned as the first element in the list. -Returns one of: - - a list : the matching node - - nil : the point is not looking at a tag. - - a cons cell: the first element is the DTD, the second is the node" - (cond - ;; Processing instructions (like the <?xml version="1.0"?> tag at the - ;; beginning of a document) - ((looking-at "<\\?") - (search-forward "?>" end) - (skip-chars-forward " \t\n") - (xml-parse-tag end)) - ;; Character data (CDATA) sections, in which no tag should be interpreted - ((looking-at "<!\\[CDATA\\[") - (let ((pos (match-end 0))) - (unless (search-forward "]]>" end t) - (error "CDATA section does not end anywhere in the document")) - (buffer-substring-no-properties pos (match-beginning 0)))) - ;; DTD for the document - ((looking-at "<!DOCTYPE") - (let (dtd) - (if parse-dtd - (setq dtd (xml-parse-dtd end)) - (xml-skip-dtd end)) - (skip-chars-forward " \t\n") - (if dtd - (cons dtd (xml-parse-tag end)) - (xml-parse-tag end)))) - ;; skip comments - ((looking-at "<!--") - (search-forward "-->" end) - nil) - ;; end tag - ((looking-at "</") - '()) - ;; opening tag - ((looking-at "<\\([^/> \t\n]+\\)") - (goto-char (match-end 1)) - (let* ((case-fold-search nil) ;; XML is case-sensitive. - (node-name (match-string 1)) - ;; Parse the attribute list. - (children (list (xml-parse-attlist end) (intern node-name))) - pos) - - ;; is this an empty element ? - (if (looking-at "/>") - (progn - (forward-char 2) - (nreverse children)) - - ;; is this a valid start tag ? - (if (eq (char-after) ?>) - (progn - (forward-char 1) - ;; Now check that we have the right end-tag. Note that this - ;; one might contain spaces after the tag name - (while (not (looking-at (concat "</" node-name "[ \t\n]*>"))) - (cond - ((looking-at "</") - (error (concat - "XML: invalid syntax -- invalid end tag (expecting " - node-name - ") at pos " (number-to-string (point))))) - ((= (char-after) ?<) - (let ((tag (xml-parse-tag end))) - (when tag - (push tag children)))) - (t - (setq pos (point)) - (search-forward "<" end) - (forward-char -1) - (let ((string (buffer-substring-no-properties pos (point))) - (pos 0)) - - ;; Clean up the string (no newline characters) - ;; Not done, since as per XML specifications, the XML processor - ;; should always pass the whole string to the application. - ;; (while (string-match "\\s +" string pos) - ;; (setq string (replace-match " " t t string)) - ;; (setq pos (1+ (match-beginning 0)))) - - (setq string (xml-substitute-special string)) - (setq children - (if (stringp (car children)) - ;; The two strings were separated by a comment. - (cons (concat (car children) string) - (cdr children)) - (cons string children))))))) - (goto-char (match-end 0)) - (if (> (point) end) - (error "XML: End tag for %s not found before end of region" - node-name)) - (nreverse children)) - - ;; This was an invalid start tag - (error "XML: Invalid attribute list") - )))) - (t ;; This is not a tag. - (error "XML: Invalid character")) - )) - -(defun xml-parse-attlist (end) - "Return the attribute-list that point is looking at. -The search for attributes end at the position END in the current buffer. -Leaves the point on the first non-blank character after the tag." - (let ((attlist ()) - name) - (skip-chars-forward " \t\n") - (while (looking-at "\\([a-zA-Z_:][-a-zA-Z0-9._:]*\\)[ \t\n]*=[ \t\n]*") - (setq name (intern (match-string 1))) - (goto-char (match-end 0)) - - ;; Do we have a string between quotes (or double-quotes), - ;; or a simple word ? - (unless (looking-at "\"\\([^\"]*\\)\"") - (unless (looking-at "'\\([^']*\\)'") - (error "XML: Attribute values must be given between quotes"))) - - ;; Each attribute must be unique within a given element - (if (assoc name attlist) - (error "XML: each attribute must be unique within an element")) - - (push (cons name (match-string-no-properties 1)) attlist) - (goto-char (match-end 0)) - (skip-chars-forward " \t\n") - (if (> (point) end) - (error "XML: end of attribute list not found before end of region")) - ) - (nreverse attlist))) - -;;******************************************************************* -;;** -;;** The DTD (document type declaration) -;;** The following functions know how to skip or parse the DTD of -;;** a document -;;** -;;******************************************************************* - -(defun xml-skip-dtd (end) - "Skip the DTD that point is looking at. -The DTD must end before the position END in the current buffer. -The point must be just before the starting tag of the DTD. -This follows the rule [28] in the XML specifications." - (forward-char (length "<!DOCTYPE")) - (if (looking-at "[ \t\n]*>") - (error "XML: invalid DTD (excepting name of the document)")) - (condition-case nil - (progn - (forward-word 1) ;; name of the document - (skip-chars-forward " \t\n") - (if (looking-at "\\[") - (re-search-forward "\\][ \t\n]*>" end) - (search-forward ">" end))) - (error (error "XML: No end to the DTD")))) - -(defun xml-parse-dtd (end) - "Parse the DTD that point is looking at. -The DTD must end before the position END in the current buffer." - (forward-char (length "<!DOCTYPE")) - (skip-chars-forward " \t\n") - (if (looking-at ">") - (error "XML: invalid DTD (excepting name of the document)")) - - ;; Get the name of the document - (looking-at "\\sw+") - (let ((dtd (list (match-string-no-properties 0) 'dtd)) - type element end-pos) - (goto-char (match-end 0)) - - (skip-chars-forward " \t\n") - - ;; External DTDs => don't know how to handle them yet - (if (looking-at "SYSTEM") - (error "XML: Don't know how to handle external DTDs")) - - (if (not (= (char-after) ?\[)) - (error "XML: Unknown declaration in the DTD")) - - ;; Parse the rest of the DTD - (forward-char 1) - (while (and (not (looking-at "[ \t\n]*\\]")) - (<= (point) end)) - (cond - - ;; Translation of rule [45] of XML specifications - ((looking-at - "[\t \n]*<!ELEMENT[ \t\n]+\\([a-zA-Z0-9.%;]+\\)[ \t\n]+\\([^>]+\\)>") - - (setq element (intern (match-string-no-properties 1)) - type (match-string-no-properties 2)) - (setq end-pos (match-end 0)) - - ;; Translation of rule [46] of XML specifications - (cond - ((string-match "^EMPTY[ \t\n]*$" type) ;; empty declaration - (setq type 'empty)) - ((string-match "^ANY[ \t\n]*$" type) ;; any type of contents - (setq type 'any)) - ((string-match "^(\\(.*\\))[ \t\n]*$" type) ;; children ([47]) - (setq type (xml-parse-elem-type (match-string-no-properties 1 type)))) - ((string-match "^%[^;]+;[ \t\n]*$" type) ;; substitution - nil) - (t - (error "XML: Invalid element type in the DTD"))) - - ;; rule [45]: the element declaration must be unique - (if (assoc element dtd) - (error "XML: elements declaration must be unique in a DTD (<%s>)" - (symbol-name element))) - - ;; Store the element in the DTD - (push (list element type) dtd) - (goto-char end-pos)) - - - (t - (error "XML: Invalid DTD item")) - ) - ) - - ;; Skip the end of the DTD - (search-forward ">" end) - (nreverse dtd))) - - -(defun xml-parse-elem-type (string) - "Convert a STRING for an element type into an elisp structure." - - (let (elem modifier) - (if (string-match "(\\([^)]+\\))\\([+*?]?\\)" string) - (progn - (setq elem (match-string 1 string) - modifier (match-string 2 string)) - (if (string-match "|" elem) - (setq elem (cons 'choice - (mapcar 'xml-parse-elem-type - (split-string elem "|")))) - (if (string-match "," elem) - (setq elem (cons 'seq - (mapcar 'xml-parse-elem-type - (split-string elem ",")))) - ))) - (if (string-match "[ \t\n]*\\([^+*?]+\\)\\([+*?]?\\)" string) - (setq elem (match-string 1 string) - modifier (match-string 2 string)))) - - (if (and (stringp elem) (string= elem "#PCDATA")) - (setq elem 'pcdata)) - - (cond - ((string= modifier "+") - (list '+ elem)) - ((string= modifier "*") - (list '* elem)) - ((string= modifier "?") - (list '? elem)) - (t - elem)))) - - -;;******************************************************************* -;;** -;;** Substituting special XML sequences -;;** -;;******************************************************************* - -(defun xml-substitute-special (string) - "Return STRING, after subsituting special XML sequences." - (while (string-match "&" string) - (setq string (replace-match "&" t nil string))) - (while (string-match "<" string) - (setq string (replace-match "<" t nil string))) - (while (string-match ">" string) - (setq string (replace-match ">" t nil string))) - (while (string-match "'" string) - (setq string (replace-match "'" t nil string))) - (while (string-match """ string) - (setq string (replace-match "\"" t nil string))) - string) - -;;******************************************************************* -;;** -;;** Printing a tree. -;;** This function is intended mainly for debugging purposes. -;;** -;;******************************************************************* - -(defun xml-debug-print (xml) - (dolist (node xml) - (xml-debug-print-internal node ""))) - -(defun xml-debug-print-internal (xml indent-string) - "Outputs the XML tree in the current buffer. -The first line indented with INDENT-STRING." - (let ((tree xml) - attlist) - (insert indent-string "<" (symbol-name (xml-node-name tree))) - - ;; output the attribute list - (setq attlist (xml-node-attributes tree)) - (while attlist - (insert " ") - (insert (symbol-name (caar attlist)) "=\"" (cdar attlist) "\"") - (setq attlist (cdr attlist))) - - (insert ">") - - (setq tree (xml-node-children tree)) - - ;; output the children - (dolist (node tree) - (cond - ((listp node) - (insert "\n") - (xml-debug-print-internal node (concat indent-string " "))) - ((stringp node) (insert node)) - (t - (error "Invalid XML tree")))) - - (insert "\n" indent-string - "</" (symbol-name (xml-node-name xml)) ">"))) - -(provide 'xml) -(provide 'xml-fixed) - -;;; xml.el ends here |