Fixed a small bug in indentation + added new commands for queries with

Printing Implicit and Printing All flags.

3 files changed, 96 insertions, 8 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 538ad5ec..c279e91b 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -89,12 +89,18 @@
     ("OTHER QUERIES"
      ["Print Hint" coq-PrintHint t]
      ["Show ith goal..." coq-Show t]
+     ["Show ith goal... (show implicits)" coq-Show-with-implicits t]
+     ["Show ith goal... (show all)" coq-Show-with-all t]
      ["Show Tree" coq-show-tree t]
      ["Show Proof" coq-show-proof t]
      ["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG?
      ""
      ["Print..." coq-Print t]
+     ["Print... (show implicits)" coq-Print-with-implicits t]
+     ["Print... (show all)" coq-Print-with-all t]
      ["Check..." coq-Check t]
+     ["Check (show implicits)..." coq-Check-show-implicits t]
+     ["Check (show all)..." coq-Check-show-all t]
      ["About..." coq-About t]
      ["Search..." coq-SearchConstant t]
      ["SearchRewrite..." coq-SearchRewrite t]
diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el
index 39fcdda9..a87beb82 100644
--- a/coq/coq-smie-lexer.el
+++ b/coq/coq-smie-lexer.el
@@ -121,7 +121,9 @@ command (and inside parenthesis)."
 	  ;; The default lexer is faster and is good enough for our needs.
 	  (let* ((next (smie-default-forward-token))
 		 (parop (assoc next ignore-between)))
-	    (if parop ; if we find something to ignore, we directly
+	    ; if we find something to ignore, we directly jump to the
+	    ; corresponding closer
+	    (if parop
 		(let ((parops ; corresponding matcher may be a list
 		       (if (listp parop) (cdr parop)
 			 (cons (cdr parop) nil)))) ; go to corresponding closer
@@ -137,7 +139,8 @@ command (and inside parenthesis)."
 			(looking-at "[[:space:]]"))
 		(cond
 		 ((and (zerop (length next))
-		       (equal (char-syntax ?\)) (char-syntax (char-after))))
+		       (or (equal (point) (point-max)) ; protecting char-after next line
+			   (equal (char-syntax ?\)) (char-syntax (char-after)))))
 		  (throw 'found nil))
 		 ((zerop (length next)) ;; capture other characters than closing parent
 		  (forward-sexp 1))
@@ -162,8 +165,9 @@ command (and inside parenthesis). "
 	    (let* ((next2 (smie-default-backward-token))
 		   (next (if (member next2 coq-smie-dot-friends) "." next2))
 		   (parop (rassoc next ignore-between)))
-	      ;(message "praop = %S" parop)
-	      (if parop ; if we find something to ignore, we directly
+	      ; if we find something to ignore, we directly jump to the
+	      ; corresponding openner
+	      (if parop
 		  (let ((p (point))
 			(parops ; corresponding matcher may be a list
 			 (if (listp (car parop)) (car parop) (cons (car parop) nil))))
@@ -181,7 +185,8 @@ command (and inside parenthesis). "
 			  (looking-at ".[[:space:]]"))
 		  (cond
 		   ((and (zerop (length next))
-			 (equal (char-syntax ?\() (char-syntax (char-before))))
+			 (or (equal (point) (point-min)) ; protecting char-before next line
+			     (equal (char-syntax ?\() (char-syntax (char-before)))))
 		    (throw 'found nil))
 		   ((zerop (length next)) (forward-sexp -1))
 		   ((member next tokens) (throw 'found next))))))))
diff --git a/coq/coq.el b/coq/coq.el
index 9b7f37db..3e94b534 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -673,8 +673,55 @@ If locked span already has a state number, then do nothing. Also updates
     (proof-shell-ready-prover)
     (setq cmd (coq-guess-or-ask-for-string ask dontguess))
     (proof-shell-invisible-command
-     (format (concat do " %s . ") (funcall postform cmd))))
-  )
+     (format (concat do " %s . ") (funcall postform cmd)))))
+
+
+(defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd)
+  "Play commands SETCMD then CMD and then silently UNSETCMD."
+  (let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd)))
+    (proof-shell-invisible-command
+     (format " %s . " (funcall postform setcmd)) 'wait)
+    (proof-shell-invisible-command
+     (format " %s . " (funcall postform cmd)) 'wait)
+    (proof-shell-invisible-command-invisible-result
+     (format " %s . " (funcall postform unsetcmd)))))
+
+(defun coq-ask-do-set-unset (ask do setcmd unsetcmd
+                                 &optional dontguess postformatcmd)
+  "Ask for an ident id and execute command DO in SETCMD mode.
+More precisely it executes SETCMD, then DO id and finally silently UNSETCMD."
+  (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd)))
+    (proof-shell-ready-prover)
+    (setq cmd (coq-guess-or-ask-for-string ask dontguess))
+    (coq-command-with-set-unset setcmd (concat do " " cmd) unsetcmd postformatcmd)))
+
+
+(defun coq-ask-do-show-implicits (ask do &optional dontguess postformatcmd)
+  "Ask for an ident and print the corresponding term."
+  (coq-ask-do-set-unset ask do
+                        "Set Printing Implicit"
+                        "Unset Printing Implicit"
+                        dontguess postformatcmd))
+
+(defun coq-ask-do-show-all (ask do &optional dontguess postformatcmd)
+  "Ask for an ident and print the corresponding term."
+  (coq-ask-do-set-unset ask do
+                        "Set Printing All"
+                        "Unset Printing All"
+                        dontguess postformatcmd))
+
+
+  ;; (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd)))
+    
+
+  ;;   (proof-shell-ready-prover)
+  ;;   (setq cmd (coq-guess-or-ask-for-string ask dontguess))
+  ;;   (coq-command-with-set-unset
+  ;;    "Set Printing Implicit"
+  ;;    (format (concat do " %s . ") cmd)
+  ;;    "Unset Printing Implicit" )
+  ;;   ))
+
 
 (defsubst coq-put-into-brackets (s)
   (concat "[ " s " ]"))
@@ -715,6 +762,16 @@ This is specific to `coq-mode'."
   (interactive)
   (coq-ask-do "Print" "Print"))
 
+(defun coq-Print-with-implicits ()
+  "Ask for an ident and print the corresponding term."
+  (interactive)
+  (coq-ask-do-show-implicits "Print" "Print"))
+
+(defun coq-Print-with-all ()
+  "Ask for an ident and print the corresponding term."
+  (interactive)
+  (coq-ask-do-show-all "Print" "Print"))
+
 (defun coq-About ()
   "Ask for an ident and print information on it."
   (interactive)
@@ -761,11 +818,31 @@ This is specific to `coq-mode'."
   (interactive)
   (coq-ask-do "Check" "Check"))
 
+(defun coq-Check-show-implicits ()
+  "Ask for a term and print its type."
+  (interactive)
+  (coq-ask-do-show-implicits "Check" "Check"))
+
+(defun coq-Check-show-all ()
+  "Ask for a term and print its type."
+  (interactive)
+  (coq-ask-do-show-all "Check" "Check"))
+
 (defun coq-Show ()
   "Ask for a number i and show the ith goal."
   (interactive)
   (coq-ask-do "Show goal number" "Show" t))
 
+(defun coq-Show-with-implicits ()
+  "Ask for a number i and show the ith goal."
+  (interactive)
+  (coq-ask-do-show-implicits "Show goal number" "Show" t))
+
+(defun coq-Show-with-all ()
+  "Ask for a number i and show the ith goal."
+  (interactive)
+  (coq-ask-do-show-all "Show goal number" "Show" t))
+
 
 (proof-definvisible coq-PrintHint "Print Hint. ")
 
@@ -2147,7 +2224,7 @@ Based on idea mentioned in Coq reference manual."
   (interactive)
   (add-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook)
   (proof-assert-next-command-interactive)
-  (remove-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook);as soone as possible
+  (remove-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook);as soon as possible
   (proof-shell-wait)
   (let
       ((str (string-match "<info type=\"infoH\">\\([^<]*\\)</info>"