diff --git a/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md b/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md index 5ca4b6f000f..09a135fd322 100644 --- a/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md +++ b/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md @@ -200,12 +200,12 @@ will express the exact same grammar as `lesson-04-b.k` ```k module LESSON-04-D - syntax Boolean ::= "true" [literal] | "false" [literal] - | "(" Boolean ")" [atom, bracket] - | "!" Boolean [not, function] - | Boolean "&&" Boolean [and, function] - | Boolean "^" Boolean [xor, function] - | Boolean "||" Boolean [or, function] + syntax Boolean ::= "true" [group(literal)] | "false" [group(literal)] + | "(" Boolean ")" [group(atom), bracket] + | "!" Boolean [group(not), function] + | Boolean "&&" Boolean [group(and), function] + | Boolean "^" Boolean [group(xor), function] + | Boolean "||" Boolean [group(or), function] syntax priorities literal atom > not > and > xor > or syntax left and diff --git a/k-distribution/k-tutorial/1_basic/11_casts/README.md b/k-distribution/k-tutorial/1_basic/11_casts/README.md index 8ed50ff4399..e2f8efeb354 100644 --- a/k-distribution/k-tutorial/1_basic/11_casts/README.md +++ b/k-distribution/k-tutorial/1_basic/11_casts/README.md @@ -94,8 +94,8 @@ example, consider the following definition: module LESSON-11-C imports INT - syntax Exp ::= Int | Exp "+" Exp [exp] - syntax Exp2 ::= Exp | Exp2 "+" Exp2 [exp2] + syntax Exp ::= Int | Exp "+" Exp [group(exp)] + syntax Exp2 ::= Exp | Exp2 "+" Exp2 [group(exp2)] endmodule ``` diff --git a/k-distribution/tests/regression-new/group/Makefile b/k-distribution/tests/regression-new/group/Makefile index 2d7de94a866..5f4c4d95692 100644 --- a/k-distribution/tests/regression-new/group/Makefile +++ b/k-distribution/tests/regression-new/group/Makefile @@ -2,6 +2,5 @@ DEF=test EXT=test TESTDIR=. KOMPILE_BACKEND=llvm -KOMPILE_FLAGS=--pedantic-attributes include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/issue-1169/Makefile b/k-distribution/tests/regression-new/issue-1169/Makefile index 96e416ddb87..bc1d28c231d 100644 --- a/k-distribution/tests/regression-new/issue-1169/Makefile +++ b/k-distribution/tests/regression-new/issue-1169/Makefile @@ -7,7 +7,7 @@ include ../../../include/kframework/ktest.mak $(KOMPILED_DIR)/timestamp: $(DEF).k $(KOMPILE) $(DEF).k -E > $(DEF2).k - $(KOMPILE) $(DEF2).k --no-prelude --main-module TEST --syntax-module TEST + $(KOMPILE) $(DEF2).k --no-pedantic-attributes --no-prelude --main-module TEST --syntax-module TEST rm -rf $(KOMPILED_DIR) mv test2-kompiled $(KOMPILED_DIR) diff --git a/k-distribution/tests/regression-new/pedanticAttributes/Makefile b/k-distribution/tests/regression-new/pedanticAttributes/Makefile index e367d48834a..cc7bdd31d1f 100644 --- a/k-distribution/tests/regression-new/pedanticAttributes/Makefile +++ b/k-distribution/tests/regression-new/pedanticAttributes/Makefile @@ -1,3 +1,2 @@ -KOMPILE_FLAGS=-w none --syntax-module TEST --pedantic-attributes - +KOMPILE_FLAGS=-w none --syntax-module TEST include ../../../include/kframework/ktest-fail.mak diff --git a/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java b/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java index aeadf660e4a..8ad2fe18cb9 100644 --- a/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java @@ -52,7 +52,7 @@ public synchronized File mainDefinitionFile(FileUtil files) { @Parameter(names="--md-selector", description="Preprocessor: for .md files, select only the md code blocks that match the selector expression. Ex:'k&(!a|b)'.") public String mdSelector = "k"; - @Parameter(names="--pedantic-attributes", description="Require that all attributes are known built-ins. " + - "User-defined groups must be added through the group(_) attribute.") - public boolean pedanticAttributes = false; + @Parameter(names="--no-pedantic-attributes", description="Do not enforce that all attributes are known built-ins.", + hidden = true) + public boolean pedanticAttributes = true; }