From 922a470ad19bb05a787fd52300a22a6a26bbeebb Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 29 Aug 2002 23:49:09 +0000 Subject: Layout/docstring improvements (based on patch from Stefan Monnier) --- coq/coq-syntax.el | 537 +++++++++++++++++++++++++----------------------------- 1 file changed, 248 insertions(+), 289 deletions(-) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 1220d5d2..69316402 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1,7 +1,7 @@ ;; coq-syntax.el Font lock expressions for Coq ;; Copyright (C) 1997, 1998 LFCS Edinburgh. ;; Authors: Thomas Kleymann and Healfdene Goguen -;; Maintainer: Patrick Loiseleur +;; Maintainer: Pierre Courtieu ;; $Id$ @@ -70,153 +70,139 @@ (defcustom coq-user-state-changing-commands nil - -"Configuration variable (default to nil). List of strings containing -the user defined Coq commands that need to be backtracked (like -Require, Definition, etc). + "List of user-defined Coq commands that need to be backtracked; +like Require, Definition, etc... For example if MyHint and MyRequire are user defined variants of the Hint and Require commands, put the following line in your .emacs: - (setq coq-user-state-changing-commands - '(\"MyHint\" \"MyRequire\")) -" -) - -(defvar coq-user-state-preserving-commands nil + (setq coq-user-state-changing-commands '(\"MyHint\" \"MyRequire\"))" + :type '(repeat regexp) + :group 'coq) -"Configuration variable (default to nil). List of strings containing -the user defined Coq commands that do not need to be backtracked (like -Print, Check, Show etc). + +(defcustom coq-user-state-preserving-commands nil + "List of user defined Coq commands that do not need to be backtracked; +like Print, Check, Show etc... For example if MyPrint and MyCheck are user defined variants of the Print and Check commands, put the following line in your .emacs: - (setq coq-user-state-preserving-commands - '(\"MyPrint\" \"MyCheck\")) -" -) + (setq coq-user-state-preserving-commands '(\"MyPrint\" \"MyCheck\"))" + :type '(repeat regexp) + :group 'coq) ;; (defvar coq-keywords-state-preserving-commands - (append '( -"(*" ;;Pierre comments must not be undone -"Add\\s-+LoadPath" -"Add\\s-+ML\\s-+Path" -"Add\\s-+Rec\\s-+ML\\s-+Path" -"Add\\s-+Rec\\s-+LoadPath" -"Cd" -"Check" -"DelPath" -"Eval" -"Extraction" -"Extraction Module" -"Focus" ;; ??? -"Hint\\-+Rewrite" -"Inspect" -"Locate" -"Locate\\s-+File" -"Locate\\s-+Library" -"Opaque" -"Print" -"Proof" -"Recursive\\-+Extraction" -"Recursive\\-+Extraction\\-+Module" -"Remove\\-+LoadPath" -"Pwd" -"Qed" -"Reset" -"Save" -"Search" -"SearchIsos" -"SearchPattern" -"SearchRewrite" -"Set\\-+Hyps_limit" -"Set\\-+Undo" -"Set\\-+Set\\-+Printing\\-+Coercion[^s]" -"Show" -"Test\\s-+Printing\\s-+If" -"Test\\s-+Printing\\s-+Let" -"Test\\s-+Printing\\s-+Synth" -"Test\\s-+Printing\\s-+Wildcard" -"Unfocus" ; ??? -"Unset\\s-+Hyps_limit" -"Unset\\s-+Undo" -"Unset\\s-+Printing\\s-+Coercion[^s]" -"Transparent" -"Write\\s-+State") - coq-user-state-preserving-commands - ) - ) - - - + (append '("(*" ;;Pierre comments must not be undone + "Add\\s-+LoadPath" + "Add\\s-+ML\\s-+Path" + "Add\\s-+Rec\\s-+ML\\s-+Path" + "Add\\s-+Rec\\s-+LoadPath" + "Cd" + "Check" + "DelPath" + "Eval" + "Extraction" + "Extraction Module" + "Focus" ;; ??? + "Hint\\-+Rewrite" + "Inspect" + "Locate" + "Locate\\s-+File" + "Locate\\s-+Library" + "Opaque" + "Print" + "Proof" + "Recursive\\-+Extraction" + "Recursive\\-+Extraction\\-+Module" + "Remove\\-+LoadPath" + "Pwd" + "Qed" + "Reset" + "Save" + "Search" + "SearchIsos" + "SearchPattern" + "SearchRewrite" + "Set\\-+Hyps_limit" + "Set\\-+Undo" + "Set\\-+Set\\-+Printing\\-+Coercion[^s]" + "Show" + "Test\\s-+Printing\\s-+If" + "Test\\s-+Printing\\s-+Let" + "Test\\s-+Printing\\s-+Synth" + "Test\\s-+Printing\\s-+Wildcard" + "Unfocus" ; ??? + "Unset\\s-+Hyps_limit" + "Unset\\s-+Undo" + "Unset\\s-+Printing\\s-+Coercion[^s]" + "Transparent" + "Write\\s-+State") + coq-user-state-preserving-commands)) (defvar coq-keywords-state-changing-misc-commands - '( -"Add\\s-+Abstract\\s-+Ring" -"Add\\s-+Abstract\\s-+Semi\\s-+Ring" -"Add\\s-+Field" -"Add\\s-+Morphism" -"Add\\s-+Printing" -"Add\\s-+Ring" -"Add\\s-+Semi\\s-+Ring" -"Add\\s-+Setoid" -"Begin\\s-+Silent" -"Canonical\\s-+Structure" -"CoFixpoint" -"CoInductive" -"Coercion" -"Declare\\s-+ML\\s-+Module" -"End\\s-+Silent" -"Derive\\s-+Dependent\\s-+Inversion" -"Derive\\s-+Dependent\\s-+Inversion_clear" -"Derive\\s-+Inversion" -"Derive\\s-+Inversion_clear" -"Extract\\s-+Constant" -"Extract\\s-+Inductive" -"Extraction\\s-+Inline" -"Extraction\\s-+Language" -"Extraction\\s-+NoInline" -"Grammar" -"Hint" -"Hints" -"Identity\\s-+Coercion" -"Implicit\\s-+Arguments\\s-+Off" -"Implicit\\s-+Arguments\\s-+On" -"Implicits" -"Infix" -"Load" -"Read\\s-+Module" -"Remove\\s-+LoadPath" -"Remove\\s-+Printing\\s-+If\\s-+ident" -"Remove\\s-+Printing\\s-+Let\\s-+ident" -"Require" -"Require\\s-+Export" -"Reset\\s-+Extraction\\s-+Inline" -"Reset\\s-+Initial" -"Restart" -"Restore\\s-+State" -"Remove\\s-+Printing\\s-+If\\s-+ident" -"Remove\\s-+Printing\\s-+Let\\s-+ident" -"Restore\\s-+State" -"Set\\s-+Extraction\\s-+AutoInline" -"Set\\s-+Extraction\\s-+Optimize" -"Set\\s-+Implicit\\s-+Arguments" -"Set\\s-+Printing\\s-+Coercions" -"Set\\s-+Printing\\s-+Synth" -"Set\\s-+Printing\\s-+Wildcard" -"Unset\\s-+Extraction\\s-+AutoInline" -"Unset\\s-+Extraction\\s-+Optimize" -"Unset\\s-+Implicit\\s-+Arguments" -"Unset\\s-+Printing\\s-+Coercions" -"Unset\\s-+Printing\\s-+Synth" -"Unset\\s-+Printing\\s-+Wildcard" -"Syntax" -"Transparent" -) - ) + '("Add\\s-+Abstract\\s-+Ring" + "Add\\s-+Abstract\\s-+Semi\\s-+Ring" + "Add\\s-+Field" + "Add\\s-+Morphism" + "Add\\s-+Printing" + "Add\\s-+Ring" + "Add\\s-+Semi\\s-+Ring" + "Add\\s-+Setoid" + "Begin\\s-+Silent" + "Canonical\\s-+Structure" + "CoFixpoint" + "CoInductive" + "Coercion" + "Declare\\s-+ML\\s-+Module" + "End\\s-+Silent" + "Derive\\s-+Dependent\\s-+Inversion" + "Derive\\s-+Dependent\\s-+Inversion_clear" + "Derive\\s-+Inversion" + "Derive\\s-+Inversion_clear" + "Extract\\s-+Constant" + "Extract\\s-+Inductive" + "Extraction\\s-+Inline" + "Extraction\\s-+Language" + "Extraction\\s-+NoInline" + "Grammar" + "Hint" + "Hints" + "Identity\\s-+Coercion" + "Implicit\\s-+Arguments\\s-+Off" + "Implicit\\s-+Arguments\\s-+On" + "Implicits" + "Infix" + "Load" + "Read\\s-+Module" + "Remove\\s-+LoadPath" + "Remove\\s-+Printing\\s-+If\\s-+ident" + "Remove\\s-+Printing\\s-+Let\\s-+ident" + "Require" + "Require\\s-+Export" + "Reset\\s-+Extraction\\s-+Inline" + "Reset\\s-+Initial" + "Restart" + "Restore\\s-+State" + "Remove\\s-+Printing\\s-+If\\s-+ident" + "Remove\\s-+Printing\\s-+Let\\s-+ident" + "Restore\\s-+State" + "Set\\s-+Extraction\\s-+AutoInline" + "Set\\s-+Extraction\\s-+Optimize" + "Set\\s-+Implicit\\s-+Arguments" + "Set\\s-+Printing\\s-+Coercions" + "Set\\s-+Printing\\s-+Synth" + "Set\\s-+Printing\\s-+Wildcard" + "Unset\\s-+Extraction\\s-+AutoInline" + "Unset\\s-+Extraction\\s-+Optimize" + "Unset\\s-+Implicit\\s-+Arguments" + "Unset\\s-+Printing\\s-+Coercions" + "Unset\\s-+Printing\\s-+Synth" + "Unset\\s-+Printing\\s-+Wildcard" + "Syntax" + "Transparent")) @@ -234,174 +220,154 @@ Print and Check commands, put the following line in your .emacs: (defvar coq-keywords-commands (append coq-keywords-state-changing-commands coq-keywords-state-preserving-commands) - "All commands keyword") + "All commands keyword.") (defcustom coq-user-state-changing-tactics nil - -"Configuration variable (default to nil). List of strings containing -the user defined Coq tactics that need to be backtracked (like almost -all tactics, but \"Idtac\" (\"Proof\" is a command actually)). + "List of user defined Coq tactics that need to be backtracked; +like almost all tactics, but \"Idtac\" (\"Proof\" is a command actually). For example if MyIntro and MyElim are user defined variants of the Intro and Elim tactics, put the following line in your .emacs: - (setq coq-user-state-changing-tactics - '(\"MyIntro\" \"MyElim\")) -" -) + (setq coq-user-state-changing-tactics '(\"MyIntro\" \"MyElim\"))" + :type '(repeat regexp) + :group 'coq) (defvar coq-state-changing-tactics - (append '( -"Absurd" -"Apply" -"Assert" -"Assumption" -"Auto" -"AutoRewrite" -"Case" -"Cbv" -"Change" -"Clear" -"ClearBody" -"Cofix" -"Compare" -"Compute" -"Constructor" -"Contradiction" -"Cut" -"CutRewrite" -;"DHyp" -;"DInd" -"Decide Equality" -"Decompose" -"Dependent Inversion" -"Dependent Inversion_clear" -"Dependent Rewrite ->" -"Dependent Rewrite <-" -"Dependent\\s-+Inversion" -"Dependent\\s-+Inversion_clear" -"Destruct" -"DiscrR" -"Discriminate" -"Double\\-+Induction" -"EApply" -"EAuto" -"Elim" -"ElimType" -"Exact" -"Exists" -"Field" -"Fix" -"Fold" -"Fourier" -"Generalize" -"Hnf" -"Induction" -"Injection" -"Intro[s]?" -"Intuition" -"Inversion" -"Inversion_clear" -"LApply" -"Lazy" -"Left" -"LetTac" -"Linear" -"Load" -"Move" -"NewDestruct" -"NewInduction" -"Omega " -"Pattern" -"Pose" -"Program" -"Program_all" -"Prolog" -"Quote" -"Realizer" -"Red" -"Refine" -"Reflexivity" -"Rename" -"Replace" -"Resume" -"Rewrite" -"Right" -"Ring" -"Setoid_replace" -"Simpl" -"Simple Inversion" -"Simplify_eq" -"Specialize" -"Split" -"SplitAbsolu" -"SplitRmult" -"Suspend" -"Symmetry" -"Tauto" -"Transitivity" -"Trivial" -"Unfold" -) -coq-user-state-changing-tactics -) - -) + (append '("Absurd" + "Apply" + "Assert" + "Assumption" + "Auto" + "AutoRewrite" + "Case" + "Cbv" + "Change" + "Clear" + "ClearBody" + "Cofix" + "Compare" + "Compute" + "Constructor" + "Contradiction" + "Cut" + "CutRewrite" + ;;"DHyp" + ;;"DInd" + "Decide Equality" + "Decompose" + "Dependent Inversion" + "Dependent Inversion_clear" + "Dependent Rewrite ->" + "Dependent Rewrite <-" + "Dependent\\s-+Inversion" + "Dependent\\s-+Inversion_clear" + "Destruct" + "DiscrR" + "Discriminate" + "Double\\-+Induction" + "EApply" + "EAuto" + "Elim" + "ElimType" + "Exact" + "Exists" + "Field" + "Fix" + "Fold" + "Fourier" + "Generalize" + "Hnf" + "Induction" + "Injection" + "Intro[s]?" + "Intuition" + "Inversion" + "Inversion_clear" + "LApply" + "Lazy" + "Left" + "LetTac" + "Linear" + "Load" + "Move" + "NewDestruct" + "NewInduction" + "Omega " + "Pattern" + "Pose" + "Program" + "Program_all" + "Prolog" + "Quote" + "Realizer" + "Red" + "Refine" + "Reflexivity" + "Rename" + "Replace" + "Resume" + "Rewrite" + "Right" + "Ring" + "Setoid_replace" + "Simpl" + "Simple Inversion" + "Simplify_eq" + "Specialize" + "Split" + "SplitAbsolu" + "SplitRmult" + "Suspend" + "Symmetry" + "Tauto" + "Transitivity" + "Trivial" + "Unfold") + coq-user-state-changing-tactics)) (defcustom coq-user-state-preserving-tactics nil - -"Configuration variable (default to nil). List of strings containing -the user defined Coq tactics that do not need to be backtracked (like -\"Idtac\" (no other one to my knowledge ?)). + "List of user defined Coq tactics that do not need to be backtracked; +like \"Idtac\" (no other one to my knowledge ?). For example if MyIdtac and Do_nthing are user defined variants of the Idtac (Nop) tactic, put the following line in your .emacs: - (setq coq-user-state-preserving-tactics - '(\"MyIdtac\" \"Do_nthing\")) -" -) + (setq coq-user-state-preserving-tactics '(\"MyIdtac\" \"Do_nthing\"))" + :type '(repeat regexp) + :group 'coq) -(defvar coq-state-preserving-tactics - (append '( -"Idtac" -) - coq-user-state-preserving-tactics -) -) +(defvar coq-state-preserving-tactics + (append '("Idtac") + coq-user-state-preserving-tactics)) -(defvar coq-tactics +(defvar coq-tactics (append coq-state-changing-tactics coq-state-preserving-tactics)) - (defvar coq-retractable-instruct - (append coq-state-changing-tactics coq-keywords-state-changing-commands) - ) + (append coq-state-changing-tactics coq-keywords-state-changing-commands)) (defvar coq-non-retractable-instruct (append coq-state-preserving-tactics - coq-keywords-state-preserving-commands) - ) + coq-keywords-state-preserving-commands)) (defvar coq-keywords (append coq-keywords-goal coq-keywords-save coq-keywords-decl coq-keywords-defn coq-keywords-commands) - "All keywords in a Coq script") + "All keywords in a Coq script.") -(defvar coq-tacticals - '( - "Abstract" +(defvar coq-tacticals + '("Abstract" "Do" "Idtac" ; also in state-preserving-tactic "Orelse" "Repeat" "Try") - "Keywords for tacticals in a Coq script") + "Keywords for tacticals in a Coq script.") (defvar coq-reserved - '( - "as" + '("as" "ALL" "Cases" "EX" @@ -410,18 +376,16 @@ Idtac (Nop) tactic, put the following line in your .emacs: "Fix" "if" "in" - "into" + "into" "let" "of" "then" "using" - "with" - ) - "Reserved keyworkds of Coq") + "with") + "Reserved keyworkds of Coq.") (defvar coq-symbols - '( - "|" + '("|" ":" ";" "," @@ -434,14 +398,12 @@ Idtac (Nop) tactic, put the following line in your .emacs: ":=" "=>" "->" - "." - ) - "Punctuation Symbols used by Coq") + ".") + "Punctuation Symbols used by Coq.") ;; ----- regular expressions (defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\|Uncaught exception\\|Toplevel input\\)" - "A regular expression indicating that the Coq process has identified - an error.") + "A regexp indicating that the Coq process has identified an error.") (defvar coq-id proof-id) @@ -455,19 +417,14 @@ Idtac (Nop) tactic, put the following line in your .emacs: (defvar coq-font-lock-terms (list - ;; lambda binders - (list (coq-first-abstr-regexp "\\[") 1 'proof-declaration-name-face) - + (list (coq-first-abstr-regexp "\\[") 1 'font-lock-variable-name-face) ;; Pi binders - (list (coq-first-abstr-regexp "(") 1 'proof-declaration-name-face) - + (list (coq-first-abstr-regexp "(") 1 'font-lock-variable-name-face) ;; second, third, etc. abstraction for Lambda of Pi binders - (list (coq-next-abstr-regexp) 1 'proof-declaration-name-face) - + (list (coq-next-abstr-regexp) 1 'font-lock-variable-name-face) ;; Kinds (cons "\\\\|\\\\|\\" 'font-lock-type-face)) - "*Font-lock table for Coq terms.") ;; According to Coq, "Definition" is both a declaration and a goal. @@ -482,8 +439,8 @@ Idtac (Nop) tactic, put the following line in your .emacs: (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) (defconst coq-goal-with-hole-regexp (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) - "\\)\\s-+\\(" coq-id "\\)\\s-*[:]?")) - ;; Papageno : ce serait plus propre d'omettre le `:' + "\\)\\s-+\\(" coq-id "\\)\\s-*[:]?")) + ;; Papageno : ce serait plus propre d'omettre le `:' ;; uniquement pour Correctness ;; et pour Definition f [x,y:nat] := body (defconst coq-decl-with-hole-regexp @@ -503,14 +460,15 @@ Idtac (Nop) tactic, put the following line in your .emacs: (cons "============================" 'font-lock-keyword-face) (cons "Subtree proved!" 'font-lock-keyword-face) (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) - (list "^\\([^ \n]+\\) \\(is defined\\)" + (list "^\\([^ \n]+\\) \\(is defined\\)" (list 2 'font-lock-keyword-face t) (list 1 'font-lock-function-name-face t)) (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-decl-with-hole-regexp 2 'proof-declaration-name-face) + (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face) (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) (list coq-save-with-hole-regexp 2 'font-lock-function-name-face)))) +(defvar coq-font-lock-keywords coq-font-lock-keywords-1) (defun coq-init-syntax-table () "Set appropriate values for syntax table in current buffer." @@ -537,3 +495,4 @@ Idtac (Nop) tactic, put the following line in your .emacs: (modify-syntax-entry ?\) ")(4")) (provide 'coq-syntax) +;;; coq-syntax.el ends here -- cgit v1.2.3