elpasync pushed a change to branch elpa/proof-general.
from 5169627 Test that the Proof General prelude is correct
new b550e90 Fix #574 indent of ltac "letins" pattern.
new 20028f7 New smie grammar + indentation rules + tests.
new e2138d0 Indentation testing CI ready (hopefully).
new 32b15ff Adding the CI for indentation.
Summary of changes:
.github/workflows/test.yml | 29 ++
CHANGES | 10 +
ci/test-indent/.gitignore | 1 +
ci/test-indent/Makefile | 22 +
ci/test-indent/coq-test-indent.el | 96 ++++
ci/test-indent/coq-test-indent.sh | 43 ++
ci/test-indent/indent-commands-boxed.v | 268 ++++++++++
ci/test-indent/indent-commands.v | 265 ++++++++++
.../test-indent/indent-equations.v | 20 +-
ci/test-indent/indent-inside-command-boxed.v | 104 ++++
ci/test-indent/indent-inside-command.v | 93 ++++
.../test-indent/indent-monadic.v | 26 +-
ci/test-indent/indent-tac-boxed.v | 164 ++++++
coq/ex/indent.v => ci/test-indent/indent-tac.v | 454 ++++++++++------
ci/test-indent/tests.sh | 9 +
coq/coq-indent.el | 2 +-
coq/coq-smie.el | 569 +++++++++++----------
coq/coq-syntax.el | 9 +
coq/ex/indent.v | 5 +
19 files changed, 1753 insertions(+), 436 deletions(-)
create mode 100644 ci/test-indent/.gitignore
create mode 100644 ci/test-indent/Makefile
create mode 100644 ci/test-indent/coq-test-indent.el
create mode 100755 ci/test-indent/coq-test-indent.sh
create mode 100644 ci/test-indent/indent-commands-boxed.v
create mode 100644 ci/test-indent/indent-commands.v
copy coq/ex/indent_equations.v => ci/test-indent/indent-equations.v (83%)
create mode 100644 ci/test-indent/indent-inside-command-boxed.v
create mode 100644 ci/test-indent/indent-inside-command.v
copy coq/ex/indent_monadic.v => ci/test-indent/indent-monadic.v (64%)
create mode 100644 ci/test-indent/indent-tac-boxed.v
copy coq/ex/indent.v => ci/test-indent/indent-tac.v (57%)
create mode 100755 ci/test-indent/tests.sh
