From dd1f3e5f8caa334dd8e64b3dcc17f8b28dc908f2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 25 Apr 2017 14:33:57 +0200 Subject: [PATCH] fix(frontends/lean/structure_cmd): reject internal field names Fixes #1539 --- src/frontends/lean/structure_cmd.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 1083b86005..d88e3d1861 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -800,7 +800,10 @@ struct structure_cmd_fn { auto start_pos = m_p.pos(); while (m_p.curr_is_identifier()) { auto p = m_p.pos(); - names.emplace_back(p, m_p.check_atomic_id_next("invalid field, atomic identifier expected")); + auto n = m_p.check_atomic_id_next("invalid field, atomic identifier expected"); + if (is_internal_subobject_field(n)) + throw parser_error(sstream() << "invalid field name '" << n << "', identifiers starting with '_' are reserved to the system", p); + names.emplace_back(p, n); } if (names.empty()) throw parser_error("invalid field, identifier expected", m_p.pos());