diff options
-rw-r--r-- | coq/coq-abbrev.el | 148 | ||||
-rw-r--r-- | coq/coq-syntax.el | 41 | ||||
-rw-r--r-- | coq/coq.el | 47 | ||||
-rw-r--r-- | generic/holes.el | 122 |
4 files changed, 160 insertions, 198 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 9e938a2a..14626227 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -4,64 +4,9 @@ ;(defvar coq-version-is-V7 nil) ;(defvar coq-version-is-V6 nil) +;#s are replaced by holes by holes-abbrev-complete (if (boundp 'holes-abbrev-complete) - (define-abbrev-table 'coq-mode-abbrev-table - '( - ("a" "auto" nil 0) - ("ab" "absurd" nil 0) - ("abs" "absurd" nil 0) - ("ao" "abstract omega" nil 0) - ("ap" "apply" nil 0) - ("as" "assumption" nil 0) - ("au" "auto" nil 0) - ("aw" "auto with" nil 0) - ("awa" "auto with arith" nil 0) - ("con" "constructor" nil 0) - ("dec" "decompose []" nil 0) - ("def" "Definition : :=." nil 0) - ("di" "discriminate" nil 0) - ("dis" "discriminate" nil 0) - ("e" "elim" nil 0) - ("ea" "eauto" nil 0) - ("eap" "eapply" nil 0) - ("eaw" "eauto with" nil 0) - ("eawa" "eauto with arith" nil 0) - ("el" "elim" nil 0) - ("ex" "exists" nil 0) - ("f" "forall #:#,#" nil 0) - ("f" "fun (:) => " nil 0) - ("fi" "functional induction" nil 0) - ("fix" "Fixpoint X (X : X) {struct X} : X := X." nil 0) - ("fs" "Functional Scheme xxx := Induction for yyy (opt:with ...)." nil 0) - ("g" "generalize" nil 0) - ("ge" "generalize" nil 0) - ("gen" "generalize" nil 0) - ("h" "Hints : ." nil 0) - ("hr" "Hint Resolve :." nil 0) - ("i" "intro" nil 0) - ("in" "intro" nil 0) - ("ind" "induction" nil 0) - ("indv" "Inductive" nil 0) - ("inv" "inversion" nil 0) - ("is" "intros" nil 0) - ("l" "Lemma :" nil 0) - ("o" "abstract omega" nil 0) - ("p" "Print" nil 0) - ("pr" "Print" nil 0) - ("r" "rewrite" nil 0) - ("r<" "rewrite <-" nil 0) - ("re" "rewrite" nil 0) - ("re<" "rewrite <-" nil 0) - ("s" "simpl" nil 0) - ("sc" "Scheme := Induction for Sort ." nil 0) - ("si" "simpl" nil 0) - ("sy" "symmetry" nil 0) - ("sym" "symmetry" nil 0) - ("t" "trivial" nil 0) - ("tr" "trivial" nil 0) - ("u" "unfold" nil 0) - ("un" "unfold" nil 0) - )) + () (define-abbrev-table 'coq-mode-abbrev-table '( ("a" "auto" holes-abbrev-complete 4) @@ -90,6 +35,10 @@ ("desu" "destruct # using #" holes-abbrev-complete 0) ("desa" "destruct # as #" holes-abbrev-complete 0) ("dis" "discriminate" holes-abbrev-complete 0) + ("dm" "Declare Module # : # := #." holes-abbrev-complete 0) + ("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0) + ("dmi" "Declare Module # : #.\n#\nEnd #." holes-abbrev-complete 0) + ("dmi2" "Declare Module # <: #.\n#\nEnd #." holes-abbrev-complete 0) ("e" "elim #" holes-abbrev-complete 1) ("ea" "eauto" holes-abbrev-complete 0) ("eap" "eapply #" holes-abbrev-complete 0) @@ -104,7 +53,7 @@ ("f3" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) ("f4" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) ("fi" "functional induction #" holes-abbrev-complete 0) - ("fix" "Fixpoint # (#:#) {struct #} : # :=" holes-abbrev-complete 3) + ("fix" "Fixpoint # (#:#) {struct #} : # :=\n#." holes-abbrev-complete 3) ("fo" "forall #,#" holes-abbrev-complete 0) ("fo1" "forall #:#,#" holes-abbrev-complete 0) ("fo2" "forall (#:#) (#:#), #" holes-abbrev-complete 0) @@ -125,8 +74,13 @@ ("i" "intro #" holes-abbrev-complete 10) ("if" "if # then # else #" holes-abbrev-complete 1) ("in" "intro" holes-abbrev-complete 1) + ("inf" "infix \"#\" := # (at level #) : #." holes-abbrev-complete 1) ("ind" "induction #" holes-abbrev-complete 2) ("indv" "Inductive # : # := # : #." holes-abbrev-complete 0) + ("indv2" "Inductive # : # :=\n# : #\n| # : #." holes-abbrev-complete 0) + ("indv3" "Inductive # : # :=\n # : #\n| # : #\n| # : #." holes-abbrev-complete 0) + ("indv4" "Inductive # : # :=\n # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0) + ("indv5" "Inductive # : # :=\n # : #\n| # : #\n| # : #\n| # : #\n| # : #." holes-abbrev-complete 0) ("inj" "injection #" holes-abbrev-complete 2) ("inv" "inversion #" holes-abbrev-complete 9) ("intu" "intuition #" holes-abbrev-complete 9) @@ -134,6 +88,17 @@ ("ite" "if # then # else #" holes-abbrev-complete 1) ("l" "Lemma # : #." holes-abbrev-complete 4) ("li" "let # := # in #" holes-abbrev-complete 1) + ("m" "match # with\n# => #\nend" holes-abbrev-complete 1) + ("m2" "match # with\n # => #\n| # => #\nend" holes-abbrev-complete 1) + ("m3" "match # with\n # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) + ("m4" "match # with\n# => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) + ("m5" "match # with\n # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend" holes-abbrev-complete 1) + ("mt" "Module Type # := #." holes-abbrev-complete 0) + ("mti" "Module Type #.\n#\nEnd #." holes-abbrev-complete 0) + ("mo" "Module # : # := #." holes-abbrev-complete 0) + ("mo2" "Module # <: # := #." holes-abbrev-complete 0) + ("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0) + ("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0) ("o" "omega" holes-abbrev-complete 0) ("om" "Omega" holes-abbrev-complete 0) ("p" "Print #" holes-abbrev-complete 3) @@ -166,71 +131,8 @@ ("ta" "tauto" holes-abbrev-complete 1) ("u" "unfold #" holes-abbrev-complete 1) ("un" "unfold #" holes-abbrev-complete 7) - - ("mt" "Module Type # := #." holes-abbrev-complete 0) - ("mti" "Module Type #. -# -End #." holes-abbrev-complete 0) - ("mo" "Module # : # := #." holes-abbrev-complete 0) - ("mo2" "Module # <: # := #." holes-abbrev-complete 0) - ("moi" "Module # : #. -# -End #." holes-abbrev-complete 0) - ("moi2" "Module # <: #. -# -End #." holes-abbrev-complete 0) - - - ("dm" "Declare Module # : # := #." holes-abbrev-complete 0) - ("dm2" "Declare Module # <: # := #." holes-abbrev-complete 0) - ("dmi" "Declare Module # : #. -# -End #." holes-abbrev-complete 0) - ("dmi2" "Declare Module # <: #. -# -End #." holes-abbrev-complete 0) - - - - - ("m" "match # with -# => #" holes-abbrev-complete 1) - ("m2" "match # with - # => # -| # => #" holes-abbrev-complete 1) - ("m3" "match # with - # => # -| # => # -| # => #" holes-abbrev-complete 1) - ("m4" "match # with - # => # -| # => # -| # => # -| # => #" holes-abbrev-complete 1) - ("m5" "match # with - # => # -| # => # -| # => # -| # => # -| # => #" holes-abbrev-complete 1) - ("indv2" "Inductive # : # := - # : # -| # : #." holes-abbrev-complete 0) - ("indv3" "Inductive # : # := - # : # -| # : # -| # : #." holes-abbrev-complete 0) - ("indv4" "Inductive # : # := - # : # -| # : # -| # : # -| # : #." holes-abbrev-complete 0) - ("indv5" "Inductive # : # := - # : # -| # : # -| # : # -| # : # -| # : #." holes-abbrev-complete 0) + ("v" "Variable # : #." holes-abbrev-complete 7) + ("vs" "Variables # : #." holes-abbrev-complete 7) ) ) ) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index d9f4d153..3922c7fd 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -127,19 +127,21 @@ version of coq by doing 'coqtop -v'." ) "CoInductive" "Definition" ;; careful: if not followed by :=, then it is a goal cmd "Fixpoint" + "CoInductive" "Inductive" "Inductive\\s-+Set" "Inductive\\s-+Prop" "Inductive\\s-+Type" "Mutual\\s-+Inductive" "Record" - "Functional\\s-+Scheme" "Scheme" + "Functional\\s-+Scheme" "Syntactic\\s-+Definition" - "Structure")) + "Structure" + "Ltac")) -;; Modules are like section in v74. -(if coq-version-is-V74 +;; Modules are like section in v > 7.4. +(if (or coq-version-is-V74 coq-version-is-V8) (defvar coq-keywords-goal '("Chapter" "Declare\\s-+Module";;only if not followed by:=(see coq-proof-mode-p in coq.el) @@ -169,7 +171,9 @@ version of coq by doing 'coqtop -v'." ) '("Defined" "Save" "Qed" - "End")) + "End" + "Admitted" + )) (defvar coq-keywords-kill-goal '("Abort")) @@ -201,7 +205,6 @@ Print and Check commands, put the following line in your .emacs: :group 'coq) ;; -;; Hint Rewrite/Resolve... ==> state-changing ;; Print Hint ==> state preserving (defvar coq-keywords-state-preserving-commands (append '("(*" ;;Pierre comments must not be undone @@ -217,7 +220,6 @@ Print and Check commands, put the following line in your .emacs: "Extraction Library" "Extraction Module" "Focus" ;; ??? - "Hint\\s-+Rewrite" "Inspect" "Locate" "Locate\\s-+File" @@ -225,8 +227,7 @@ Print and Check commands, put the following line in your .emacs: "Opaque" "Print" "Proof" - "Recursive\\s-+Extraction" - "Recursive\\s-+Extraction\\s-+Module" + "Recursive\\s-+Extraction\\(?:\\s-+Module\\)?" "Remove\\s-+LoadPath" "Pwd" "Qed" @@ -278,8 +279,14 @@ Print and Check commands, put the following line in your .emacs: "Extraction\\s-+Language" "Extraction\\s-+NoInline" "Grammar" - "\\`Hint" ;; Pierre fev-2003: Hack: must not match "Print Hint." - "Hints" +; "\\`Hint" ;; Pierre fev-2003: Hack: must not match "Print Hint." + "Hint\\s-+Resolve" + "Hint\\s-+Immediate" + "Hint\\s-+Rewrite" + "Hint\\s-+Unfold" + "Hint\\s-+Extern" + "Hint\\s-+Constructors" + "Hints" ;no more a keyword in v8 "Identity\\s-+Coercion" "Implicit\\s-+Arguments\\s-+Off" "Implicit\\s-+Arguments\\s-+On" @@ -403,6 +410,7 @@ Intro and Elim tactics, put the following line in your .emacs: "generalize" "hnf" "induction" + "coinduction" "injection" "instantiate" "intro[s]?" @@ -589,11 +597,16 @@ Idtac (Nop) tactic, put the following line in your .emacs: (defvar coq-reserved '("as" "ALL" - "Cases" + "True" + "False" + "Cases" + "match" "EX" "else" "end" "Fix" + "forall" + "fun" "if" "in" "into" @@ -669,7 +682,7 @@ Idtac (Nop) tactic, put the following line in your .emacs: "\\)\\s-+\\(" coq-ids "\\)\\s-*[:]")) (defconst coq-defn-with-hole-regexp (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)\\s-*[[:]")) + "\\)\\s-+\\(" coq-id "\\)\\s-*.")) (defvar coq-font-lock-keywords-1 (append coq-font-lock-terms @@ -709,6 +722,7 @@ Idtac (Nop) tactic, put the following line in your .emacs: (modify-syntax-entry ?_ "w") (modify-syntax-entry ?\' "_") (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\. "_") (condition-case nil ;; Try to use Emacs-21's nested comments. (modify-syntax-entry ?\* ". 23n") @@ -717,5 +731,6 @@ Idtac (Nop) tactic, put the following line in your .emacs: (modify-syntax-entry ?\( "()1") (modify-syntax-entry ?\) ")(4")) + (provide 'coq-syntax) ;;; coq-syntax.el ends here @@ -92,14 +92,14 @@ "COMMAND ABBREVIATION" ["Definition def<ctrl-backspace>" (insert-and-expand "def") t] ["Fixpoint fix<ctrl-backspace>" (insert-and-expand "fix") t] - ["Functional Scheme fs<ctrl-backspace>" (insert-and-expand "fs") t] - ["Functional Scheme w fsw<ctrl-backspace>" (insert-and-expand "fsw") t] + ["Lemma l<ctrl-backspace>" (insert-and-expand "l") t] + "" ["Inductive indv<ctrl-backspace>" (insert-and-expand "indv") t] ["Inductive1 indv1<ctrl-backspace>" (insert-and-expand "indv1") t] ["Inductive2 indv2<ctrl-backspace>" (insert-and-expand "indv2") t] ["Inductive3 indv3<ctrl-backspace>" (insert-and-expand "indv3") t] ["Inductive4 indv4<ctrl-backspace>" (insert-and-expand "indv4") t] - ["Lemma l<ctrl-backspace>" (insert-and-expand "l") t] + "" ["Module mo<ctrl-backspace>" (insert-and-expand "mo") t] ["Module (<:) mo2<ctrl-backspace>" (insert-and-expand "mo") t] ["Module (interactive) moi<ctrl-backspace>" (insert-and-expand "moi") t] @@ -110,13 +110,18 @@ ["Declare Module (<:) dm2<ctrl-backspace>" (insert-and-expand "dm") t] ["Declare Module (inter.) dmi<ctrl-backspace>" (insert-and-expand "dmi") t] ["Declare Module (inter. <:) dmi2<ctrl-backspace>" (insert-and-expand "dmi2") t] - + "" ["Scheme sc<ctrl-backspace>" (insert-and-expand "sc") t] + ["Functional Scheme fs<ctrl-backspace>" (insert-and-expand "fs") t] + ["Functional Scheme with fsw<ctrl-backspace>" (insert-and-expand "fsw") t] + "" ["hint Constructors hc<ctrl-backspace>" (insert-and-expand "hc") t] ["hint Immediate hi<ctrl-backspace>" (insert-and-expand "hi") t] ["hint Resolve hr<ctrl-backspace>" (insert-and-expand "hr") t] ["hint extern he<ctrl-backspace>" (insert-and-expand "he") t] ["hints hs<ctrl-backspace>" (insert-and-expand "hs") t] + "" + ["infix inf<ctrl-backspace>" (insert-and-expand "inf") t] ) ("Insert term" @@ -204,22 +209,41 @@ ["unfold u<ctrl-bacspace>" (insert-and-expand "u") t] ) + ["What are those #??" (holes-short-doc) t] + ["expand abbrev at point" expand-abbrev t] + ["list abbrevs" list-abbrevs t] + ["Insert Section..." coq-insert-section t] + ["Insert Module..." coq-insert-module t] ["Print..." coq-Print t] ["Check..." coq-Check t] ["Hints" coq-PrintHint t] ["Show ith goal..." coq-Show t] ["Search isos/pattern..." coq-SearchIsos t] - ["expand abbrev at point" expand-abbrev t] - ["What are those #??" (holes-short-doc) t] - ["list abbrevs" list-abbrevs t] ["3 buffers view" coq-three-b t] - ["Begin Section..." coq-begin-Section t] - ["End Section" coq-end-Section t] ["Compile" coq-Compile t] )) +(defun coq-insert-section (s) + (interactive "sSection name: ") + (insert "Section " s ".\n#\nEnd " s ".") +(replace-string-by-holes-backward-move-point 1 empty-hole-string) +) + +(setq-default module-kinds-table + '(("Module" 1) ("Module Type" 2) ("Declare Module" 3))) + +(defun coq-insert-module () + (interactive) + (let* ((mods (completing-read "kind of module: " module-kinds-table)) + (s (read-string "sModule name: "))) + (insert mods " " s ": #.\n#\nEnd " s ".") + (replace-string-by-holes-backward-move-point 2 empty-hole-string) + ) + ) +; (completing-read "Section name: " ) + ;; ----- outline (defvar coq-outline-regexp @@ -621,10 +645,11 @@ This is specific to coq-mode." (proof-defshortcut coq-Intros "Intros " [(control ?i)]) (proof-defshortcut coq-Apply "Apply " [(control ?a)]) -(proof-defshortcut coq-begin-Section "Section " [(control ?s)]) +;(proof-defshortcut coq-begin-Section "Section " [(control ?s)]) +(define-key coq-keymap [(control ?s)] 'coq-insert-section) +(define-key coq-keymap [(control ?m)] 'coq-insert-module) (define-key coq-keymap [(control ?e)] 'coq-end-Section) -(define-key coq-keymap [(control ?m)] 'coq-Compile) (define-key coq-keymap [(control ?o)] 'coq-SearchIsos) (define-key coq-keymap [(control ?p)] 'coq-Print) (define-key coq-keymap [(control ?c)] 'coq-Check) diff --git a/generic/holes.el b/generic/holes.el index aefa519c..f5e606b5 100644 --- a/generic/holes.el +++ b/generic/holes.el @@ -38,17 +38,16 @@ to learn how to use holes. HOLES -Holes are inspired from other interactive programs ( Pcoq ). It -allows to defines \"holes\" in your buffer. A hole is a piece of -text (highlighted) that may be replaced by another part of text -later. This feature is useful to build complicated expressions by -copy pasting several peaces of text from different parts of a -buffer (even from different buffers). +A hole is a piece of (highlighted) text that may be replaced by +another part of text later. This feature is useful to build +complicated expressions by copy pasting several peaces of text from +different parts of a buffer (or even from different buffers). USE -Holes are highlighted, there is always one or zero active hole, -highlighted with a different color. +At any time only one particular hole, called \"active\", can be +\"filled\". Holes can be in several buffers but there is always one or +zero active hole globally. It is highlighted with a different color. TO DEFINE A HOLE, two methods: @@ -63,6 +62,12 @@ TO ACTIVATE A HOLE, click on it with the button 1 of your mouse. You can also hit meta-space, it will activate the first hole following the point. The previous active hole will be deactivated. +TO JUMP TO THE ACTIVE HOLE, just hit meta-return. You must be in the +buffer containing the active hole. the point will move to the active +hole, and the active hole will be destroyed so you can type something +to put at its place. The following hole is automatically made active, +so you can hit meta-return again. + TO FORGET A HOLE without deleting its text, click on it with the button 2 (middle) of your mouse. @@ -86,27 +91,26 @@ active hole, destroy it (allowing you to type its replacement) and make the next hole active so you can hit meta-return again once you have filled the current one. -It is useful in combination with abbreviations, for example in -coq-mode \"f\" is an abbreviation for -Fixpoint # (# : #) {struct #} : # := #, where each # is a hole then -hitting meta-return goes from one hole to the following and you can -fill-in each hole very quickly. +It is useful in combination with abbreviations. For example in +coq-mode \"f\" is an abbreviation for Fixpoint # (# : #) {struct #} : +# := #, where each # is a hole. Then hitting meta-return goes from one +hole to the following and you can fill-in each hole very quickly. BUGS - o replace holes with mouse in fsf emacs works but it seems that one + o Replacing holes with mouse in fsf emacs works but it seems that one more click is needed to really see the replacement o Don't try to make overlapping holes, it doesn't work. (what would it mean anyway?) o With FSF emacs, cutting or pasting a hole wil not produce new -holes, and undoing on holes cannot make reappear holes. With Xemacs it -will, but if you copy paste the active hole, you will get several +holes, and undoing on holes cannot make holes re-appear. With Xemacs +it will, but if you copy paste the active hole, you will get several holes highlighted as the active one (whereas only one of them really is), which is annoying. - o tell me (Pierre.Courtieu@univ-orleans.fr) + o Tell me (Pierre.Courtieu@univ-orleans.fr) ") (goto-char (point-min)) @@ -288,9 +292,7 @@ is), which is annoying. (assert (is-hole-p HOLE) t "highlight-hole-as-active: given span is not a hole") -; (message "debug: highlight as active avant") (set-span-face HOLE 'active-hole-face) -; (message "debug: highlight as active avant") ) (defun highlight-hole (HOLE) @@ -334,7 +336,7 @@ is), which is annoying. ) -(defun is-in-hole (&optional pos) +(defun is-in-hole-p (&optional pos) "Returns t if pos (default: point) is in a hole, nil otherwise." @@ -347,22 +349,21 @@ is), which is annoying. (defun make-hole (start end) "Makes and returns an (span) hole from start to end." (let ((ext (make-span start end))) - (set-span-properties ext `( - hole ,hole-counter - mouse-face highlight - priority 5 ; what should I put here, I want holes to have big priority - face secondary-selection - start-open nil - end-open t - duplicable t + hole ,hole-counter + mouse-face highlight + priority 5 ; what should I put here? I want holes to have big priority + face secondary-selection + start-open nil + end-open t + duplicable t ; unique t - detachable t ;really disappear if empty; doesn't work with overlays + detachable t ;really disappear if empty; doesn't work with gnu emacs ; pointer frame-icon-glyph - help-echo "this is a \"hole\", button 2 to forget, button 3 to destroy, button 1 to make active" - 'balloon-help "this is a \"hole\", button 2 to forget, button 3 to destroy, button 1 to make active" - )) + help-echo "this is a \"hole\", button 2 to forget, button 3 to destroy, button 1 to make active" + 'balloon-help "this is a \"hole\", button 2 to forget, button 3 to destroy, button 1 to make active" + )) (set-span-keymap ext hole-map) (setq hole-counter (+ hole-counter 1)) @@ -377,12 +378,12 @@ is), which is annoying. (interactive) (let* ((rstart (or start (region-beginning-or-nil) (point))) - (rend (or end (region-end-or-nil) (point)))) + (rend (or end (region-end-or-nil) (point)))) (if (eq rstart rend) - (progn - (insert-string empty-hole-string) - (setq rend (point)) - ) + (progn + (insert-string empty-hole-string) + (setq rend (point)) + ) ) (make-hole rstart rend) ) @@ -391,7 +392,7 @@ is), which is annoying. (defun clear-hole (HOLE) (assert (is-hole-p HOLE) t - "clear-hole: given span is not a hole") + "clear-hole: given span is not a hole") (if (and (active-hole-exist-p) (eq active-hole HOLE)) (disable-active-hole) @@ -400,11 +401,9 @@ is), which is annoying. ) (defun clear-hole-at (&optional pos) - "Clears hole at pos (default=point)." - (interactive) - (if (not (is-in-hole (or pos (point)))) + (if (not (is-in-hole-p (or pos (point)))) (error "clear-hole-at: no hole here")) (clear-hole (hole-at (or pos (point)))) ) @@ -417,9 +416,7 @@ is), which is annoying. (defun mapcar-holes (FUNCTION &optional BUFFER-OR-STRING FROM TO) - (mapcar-spans FUNCTION nil - BUFFER-OR-STRING FROM - TO nil 'hole) + (mapcar-spans FUNCTION nil BUFFER-OR-STRING FROM TO nil 'hole) ) (defun clear-all-buffer-holes (&optional start end) @@ -445,9 +442,9 @@ is), which is annoying. (defun next-after-active-hole () (assert (active-hole-exist-p) t - "next-active-hole: no active hole") + "next-active-hole: no active hole") (next-hole (active-hole-end-position) - (active-hole-buffer)) + (active-hole-buffer)) ) (defun set-active-hole-next (&optional BUFFER pos) @@ -457,13 +454,12 @@ is), which is annoying. (interactive) (let ((nxthole (next-hole (or pos (point)) - (or BUFFER (current-buffer))))) + (or BUFFER (current-buffer))))) (if nxthole - (progn + (progn (set-active-hole nxthole) - ) - (message "ici") - (disable-active-hole) + ) + (disable-active-hole) ) ) ) @@ -780,6 +776,29 @@ is), which is annoying. (count-char-in-string empty-hole-string (abbrev-expansion last-abbrev-text)) ) +(defun count-chars-in-last-expand () + (length (abbrev-expansion last-abbrev-text)) + ) + +(defun count-newlines-in-last-expand () + (count-char-in-string "\n" (abbrev-expansion last-abbrev-text)) + ) + +(defun indent-last-expand () + "Indents last abbrev expansion. Must be called when the point is at +end of last abbrev expansion. " + (setq n (count-newlines-in-last-expand)) + (save-excursion + (previous-line n) + (while (>= n 0) + (indent-according-to-mode) + (next-line 1) + (setq n (- n 1)) + ) + ) + ) + + (defun replace-string-by-holes (start end str) "make occurrence of str holes between start and end. sets the @@ -837,6 +856,7 @@ created" ) (defun holes-abbrev-complete () + (indent-last-expand) (replace-string-by-holes-backward-move-point (count-holes-in-last-expand) empty-hole-string) ) |