little changes of menu/holes/abbrev in coq/pg

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
diff --git a/coq/coq.el b/coq/coq.el
index d9691d7e..2dc0440b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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)
   )