From 3b621d71274bc62722876c7229c2e649be6cb378 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Fri, 28 Oct 2016 10:45:21 +0200 Subject: fix coq-require-command-regexp (fixes #75) --- coq/coq-compile-common.el | 4 +++- coq/coq-syntax.el | 4 ---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 8ce4b0c2..5a5b63c9 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -310,7 +310,9 @@ Note that the trailing dot in \"Require A.\" is not part of the module identifier and should therefore not be matched by this regexp.") (defconst coq-require-command-regexp - "\\(?:^From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*\\)?\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*" + (concat "^\\(?:From[ \t\n]+\\(?1:[A-Za-z0-9_']+\\(?:\\.[A-Za-z0-9_']+\\)*\\)" + "[ \t\n]*\\)?" + "\\(?2:Require[ \t\n]+\\(?:Import\\|Export\\)?\\)[ \t\n]*") "Regular expression matching Require commands in Coq. Should match \"Require\" with its import and export variants up to (but not including) the first character of the first required module. The required diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 195636a5..5aa41292 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1304,10 +1304,6 @@ It is used: ;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) ;;"\\\\|\\\\|\\" -;; (defconst coq-require-command-regexp -;; (concat "Require\\s-+\\(" coq-id "\\)") -;; "Regular expression matching Require commands in Coq. -;; Group number 1 matches the name of the library which is required.") (defconst coq-context-marker-regexp (concat (regexp-opt '("ltac" "constr" "uconstr") 'symbols) ":")) -- cgit v1.2.3