TextEditor EBNF

EBNF for the TextEditor's syntax

parse_unit =
   comment?
   'machine' identifier_literal
   ('refines' identifier_literal (',' identifier_literal)*)?
   ('sees' identifier_literal (',' identifier_literal)*)?
   ('variables' identifier_list)?
   ('invariants' labeled_predicate_with_theorem+)?
   ('variant' variant)?
   ('events' event+)?
   end |
   
   comment?
   'context' identifier_literal
   ('extends' identifier_literal (',' identifier_literal)*)?
   ('sets' identifier_list)?
   ('constants' identifier_list)?
   ('axioms' labeled_predicate_with_theorem+)?
   end ;

variant = comment? expression ;

event =
   comment?
   convergence? 'event' identifier_literal
   event_refinement?
   ('any' identifier_list)?
   ('where' labeled_predicate+)?
   ('with' labeled_predicate+)?
   ('then' labeled_action+)? ;

convergence = 'ordinary' | 'convergent' | 'anticipated' ;

event_refinement =
   'refines' identifier_literal (',' identifier_literal)* |
   'extends' identifier_literal ;

labeled_action = comment? '@' identifier_literal action ;

labeled_predicate = comment? '@' identifier_literal predicate ;

labeled_predicate_with_theorem =
   comment? '@' identifier_literal predicate |
   comment? 'theorem' '@' identifier_literal predicate ;

identifier = comment? identifier_literal ;

identifier_list = identifier (',' identifier)* ;