diff options
Diffstat (limited to 'doc/tools/coqrst/notations')
-rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.g | 6 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/TacticNotations.tokens | 7 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/TacticNotationsLexer.py | 45 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/TacticNotationsLexer.tokens | 7 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/TacticNotationsParser.py | 181 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/TacticNotationsVisitor.py | 7 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/html.py | 3 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/parsing.py | 2 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/plain.py | 3 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/regexp.py | 3 | ||||
-rw-r--r-- | doc/tools/coqrst/notations/sphinx.py | 8 |
11 files changed, 176 insertions, 96 deletions
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g index 72ae8eb6b..5176c51d2 100644 --- a/doc/tools/coqrst/notations/TacticNotations.g +++ b/doc/tools/coqrst/notations/TacticNotations.g @@ -15,16 +15,18 @@ grammar TacticNotations; top: blocks EOF; blocks: block ((whitespace)? block)*; -block: atomic | hole | repeat | curlies; +block: atomic | meta | hole | repeat | curlies; repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE; curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE; whitespace: WHITESPACE; +meta: METACHAR; atomic: ATOM; hole: ID; LGROUP: '{' [+*?]; LBRACE: '{'; RBRACE: '}'; -ATOM: ~[@{} ]+; +METACHAR: '%' [|()]; +ATOM: '@' | ~[@{} ]+; ID: '@' [a-zA-Z0-9_]+; WHITESPACE: ' '+; diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens index 4d41a3883..76ed2b065 100644 --- a/doc/tools/coqrst/notations/TacticNotations.tokens +++ b/doc/tools/coqrst/notations/TacticNotations.tokens @@ -1,8 +1,9 @@ LGROUP=1 LBRACE=2 RBRACE=3 -ATOM=4 -ID=5 -WHITESPACE=6 +METACHAR=4 +ATOM=5 +ID=6 +WHITESPACE=7 '{'=2 '}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py index 4cac071ac..ffa774b9b 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.py +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py @@ -7,21 +7,24 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\b") - buf.write("&\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") - buf.write("\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\6\5\30\n\5\r\5\16\5\31") - buf.write("\3\6\3\6\6\6\36\n\6\r\6\16\6\37\3\7\6\7#\n\7\r\7\16\7") - buf.write("$\2\2\b\3\3\5\4\7\5\t\6\13\7\r\b\3\2\5\4\2,-AA\6\2\"\"") - buf.write("BB}}\177\177\6\2\62;C\\aac|\2(\2\3\3\2\2\2\2\5\3\2\2\2") - buf.write("\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\3\17") - buf.write("\3\2\2\2\5\22\3\2\2\2\7\24\3\2\2\2\t\27\3\2\2\2\13\33") - buf.write("\3\2\2\2\r\"\3\2\2\2\17\20\7}\2\2\20\21\t\2\2\2\21\4\3") - buf.write("\2\2\2\22\23\7}\2\2\23\6\3\2\2\2\24\25\7\177\2\2\25\b") - buf.write("\3\2\2\2\26\30\n\3\2\2\27\26\3\2\2\2\30\31\3\2\2\2\31") - buf.write("\27\3\2\2\2\31\32\3\2\2\2\32\n\3\2\2\2\33\35\7B\2\2\34") - buf.write("\36\t\4\2\2\35\34\3\2\2\2\36\37\3\2\2\2\37\35\3\2\2\2") - buf.write("\37 \3\2\2\2 \f\3\2\2\2!#\7\"\2\2\"!\3\2\2\2#$\3\2\2\2") - buf.write("$\"\3\2\2\2$%\3\2\2\2%\16\3\2\2\2\6\2\31\37$\2") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\t") + buf.write(".\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("\4\b\t\b\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\6\3") + buf.write("\6\6\6\36\n\6\r\6\16\6\37\5\6\"\n\6\3\7\3\7\6\7&\n\7\r") + buf.write("\7\16\7\'\3\b\6\b+\n\b\r\b\16\b,\2\2\t\3\3\5\4\7\5\t\6") + buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+~~\6\2\"\"BB}}\177\177") + buf.write("\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2") + buf.write("\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\3") + buf.write("\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2\13") + buf.write("!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23\t") + buf.write("\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27\7") + buf.write("\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32\n") + buf.write("\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36\37") + buf.write("\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3\2") + buf.write("\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3\2") + buf.write("\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+\7") + buf.write("\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3\2") + buf.write("\2\2\7\2\37!\',\2") return buf.getvalue() @@ -34,9 +37,10 @@ class TacticNotationsLexer(Lexer): LGROUP = 1 LBRACE = 2 RBRACE = 3 - ATOM = 4 - ID = 5 - WHITESPACE = 6 + METACHAR = 4 + ATOM = 5 + ID = 6 + WHITESPACE = 7 channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ] @@ -46,9 +50,10 @@ class TacticNotationsLexer(Lexer): "'{'", "'}'" ] symbolicNames = [ "<INVALID>", - "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ] + "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "WHITESPACE" ] - ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "ATOM", "ID", "WHITESPACE" ] + ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", + "WHITESPACE" ] grammarFileName = "TacticNotations.g" diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens index 4d41a3883..76ed2b065 100644 --- a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens +++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens @@ -1,8 +1,9 @@ LGROUP=1 LBRACE=2 RBRACE=3 -ATOM=4 -ID=5 -WHITESPACE=6 +METACHAR=4 +ATOM=5 +ID=6 +WHITESPACE=7 '{'=2 '}'=3 diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py index 357902ddb..c7e28af52 100644 --- a/doc/tools/coqrst/notations/TacticNotationsParser.py +++ b/doc/tools/coqrst/notations/TacticNotationsParser.py @@ -7,28 +7,29 @@ import sys def serializedATN(): with StringIO() as buf: - buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\b") - buf.write("A\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b") - buf.write("\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\5\3\30\n\3\3\3\7\3\33") - buf.write("\n\3\f\3\16\3\36\13\3\3\4\3\4\3\4\3\4\5\4$\n\4\3\5\3\5") - buf.write("\5\5(\n\5\3\5\3\5\3\5\5\5-\n\5\3\5\3\5\3\6\3\6\5\6\63") - buf.write("\n\6\3\6\3\6\5\6\67\n\6\3\6\3\6\3\7\3\7\3\b\3\b\3\t\3") - buf.write("\t\3\t\2\2\n\2\4\6\b\n\f\16\20\2\2\2A\2\22\3\2\2\2\4\25") - buf.write("\3\2\2\2\6#\3\2\2\2\b%\3\2\2\2\n\60\3\2\2\2\f:\3\2\2\2") - buf.write("\16<\3\2\2\2\20>\3\2\2\2\22\23\5\4\3\2\23\24\7\2\2\3\24") - buf.write("\3\3\2\2\2\25\34\5\6\4\2\26\30\5\f\7\2\27\26\3\2\2\2\27") - buf.write("\30\3\2\2\2\30\31\3\2\2\2\31\33\5\6\4\2\32\27\3\2\2\2") - buf.write("\33\36\3\2\2\2\34\32\3\2\2\2\34\35\3\2\2\2\35\5\3\2\2") - buf.write("\2\36\34\3\2\2\2\37$\5\16\b\2 $\5\20\t\2!$\5\b\5\2\"$") - buf.write("\5\n\6\2#\37\3\2\2\2# \3\2\2\2#!\3\2\2\2#\"\3\2\2\2$\7") - buf.write("\3\2\2\2%\'\7\3\2\2&(\7\6\2\2\'&\3\2\2\2\'(\3\2\2\2()") - buf.write("\3\2\2\2)*\7\b\2\2*,\5\4\3\2+-\7\b\2\2,+\3\2\2\2,-\3\2") - buf.write("\2\2-.\3\2\2\2./\7\5\2\2/\t\3\2\2\2\60\62\7\4\2\2\61\63") - buf.write("\5\f\7\2\62\61\3\2\2\2\62\63\3\2\2\2\63\64\3\2\2\2\64") - buf.write("\66\5\4\3\2\65\67\5\f\7\2\66\65\3\2\2\2\66\67\3\2\2\2") - buf.write("\678\3\2\2\289\7\5\2\29\13\3\2\2\2:;\7\b\2\2;\r\3\2\2") - buf.write("\2<=\7\6\2\2=\17\3\2\2\2>?\7\7\2\2?\21\3\2\2\2\t\27\34") - buf.write("#\',\62\66") + buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\t") + buf.write("F\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b") + buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3") + buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'") + buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3") + buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b") + buf.write("\3\b\3\t\3\t\3\n\3\n\3\n\2\2\13\2\4\6\b\n\f\16\20\22\2") + buf.write("\2\2F\2\24\3\2\2\2\4\27\3\2\2\2\6&\3\2\2\2\b(\3\2\2\2") + buf.write("\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2\2\20A\3\2\2\2\22C\3") + buf.write("\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3\26\3\3\2\2\2\27\36") + buf.write("\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2\2\31\32\3\2\2\2\32") + buf.write("\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2\2\2\35 \3\2\2\2\36") + buf.write("\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2\2\2 \36\3\2\2\2!\'") + buf.write("\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2$\'\5\b\5\2%\'\5\n\6") + buf.write("\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2&$\3\2\2\2&%\3\2\2\2") + buf.write("\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*)\3\2\2\2*+\3\2\2\2+") + buf.write(",\3\2\2\2,-\7\t\2\2-/\5\4\3\2.\60\7\t\2\2/.\3\2\2\2/\60") + buf.write("\3\2\2\2\60\61\3\2\2\2\61\62\7\5\2\2\62\t\3\2\2\2\63\65") + buf.write("\7\4\2\2\64\66\5\f\7\2\65\64\3\2\2\2\65\66\3\2\2\2\66") + buf.write("\67\3\2\2\2\679\5\4\3\28:\5\f\7\298\3\2\2\29:\3\2\2\2") + buf.write(":;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2=>\7\t\2\2>\r\3\2\2\2") + buf.write("?@\7\6\2\2@\17\3\2\2\2AB\7\7\2\2B\21\3\2\2\2CD\7\b\2\2") + buf.write("D\23\3\2\2\2\t\31\36&*/\659") return buf.getvalue() @@ -44,8 +45,8 @@ class TacticNotationsParser ( Parser ): literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ] - symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "ATOM", - "ID", "WHITESPACE" ] + symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR", + "ATOM", "ID", "WHITESPACE" ] RULE_top = 0 RULE_blocks = 1 @@ -53,19 +54,21 @@ class TacticNotationsParser ( Parser ): RULE_repeat = 3 RULE_curlies = 4 RULE_whitespace = 5 - RULE_atomic = 6 - RULE_hole = 7 + RULE_meta = 6 + RULE_atomic = 7 + RULE_hole = 8 ruleNames = [ "top", "blocks", "block", "repeat", "curlies", "whitespace", - "atomic", "hole" ] + "meta", "atomic", "hole" ] EOF = Token.EOF LGROUP=1 LBRACE=2 RBRACE=3 - ATOM=4 - ID=5 - WHITESPACE=6 + METACHAR=4 + ATOM=5 + ID=6 + WHITESPACE=7 def __init__(self, input:TokenStream, output:TextIO = sys.stdout): super().__init__(input, output) @@ -106,9 +109,9 @@ class TacticNotationsParser ( Parser ): self.enterRule(localctx, 0, self.RULE_top) try: self.enterOuterAlt(localctx, 1) - self.state = 16 + self.state = 18 self.blocks() - self.state = 17 + self.state = 19 self.match(TacticNotationsParser.EOF) except RecognitionException as re: localctx.exception = re @@ -157,24 +160,24 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 19 + self.state = 21 self.block() - self.state = 26 + self.state = 28 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER: if _alt==1: - self.state = 21 + self.state = 23 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 20 + self.state = 22 self.whitespace() - self.state = 23 + self.state = 25 self.block() - self.state = 28 + self.state = 30 self._errHandler.sync(self) _alt = self._interp.adaptivePredict(self._input,1,self._ctx) @@ -196,6 +199,10 @@ class TacticNotationsParser ( Parser ): return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0) + def meta(self): + return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0) + + def hole(self): return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0) @@ -225,27 +232,32 @@ class TacticNotationsParser ( Parser ): localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state) self.enterRule(localctx, 4, self.RULE_block) try: - self.state = 33 + self.state = 36 self._errHandler.sync(self) token = self._input.LA(1) if token in [TacticNotationsParser.ATOM]: self.enterOuterAlt(localctx, 1) - self.state = 29 + self.state = 31 self.atomic() pass - elif token in [TacticNotationsParser.ID]: + elif token in [TacticNotationsParser.METACHAR]: self.enterOuterAlt(localctx, 2) - self.state = 30 + self.state = 32 + self.meta() + pass + elif token in [TacticNotationsParser.ID]: + self.enterOuterAlt(localctx, 3) + self.state = 33 self.hole() pass elif token in [TacticNotationsParser.LGROUP]: - self.enterOuterAlt(localctx, 3) - self.state = 31 + self.enterOuterAlt(localctx, 4) + self.state = 34 self.repeat() pass elif token in [TacticNotationsParser.LBRACE]: - self.enterOuterAlt(localctx, 4) - self.state = 32 + self.enterOuterAlt(localctx, 5) + self.state = 35 self.curlies() pass else: @@ -303,29 +315,29 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 35 + self.state = 38 self.match(TacticNotationsParser.LGROUP) - self.state = 37 + self.state = 40 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.ATOM: - self.state = 36 + self.state = 39 self.match(TacticNotationsParser.ATOM) - self.state = 39 + self.state = 42 self.match(TacticNotationsParser.WHITESPACE) - self.state = 40 + self.state = 43 self.blocks() - self.state = 42 + self.state = 45 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 41 + self.state = 44 self.match(TacticNotationsParser.WHITESPACE) - self.state = 44 + self.state = 47 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -377,27 +389,27 @@ class TacticNotationsParser ( Parser ): self._la = 0 # Token type try: self.enterOuterAlt(localctx, 1) - self.state = 46 + self.state = 49 self.match(TacticNotationsParser.LBRACE) - self.state = 48 + self.state = 51 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 47 + self.state = 50 self.whitespace() - self.state = 50 + self.state = 53 self.blocks() - self.state = 52 + self.state = 55 self._errHandler.sync(self) _la = self._input.LA(1) if _la==TacticNotationsParser.WHITESPACE: - self.state = 51 + self.state = 54 self.whitespace() - self.state = 54 + self.state = 57 self.match(TacticNotationsParser.RBRACE) except RecognitionException as re: localctx.exception = re @@ -434,7 +446,7 @@ class TacticNotationsParser ( Parser ): self.enterRule(localctx, 10, self.RULE_whitespace) try: self.enterOuterAlt(localctx, 1) - self.state = 56 + self.state = 59 self.match(TacticNotationsParser.WHITESPACE) except RecognitionException as re: localctx.exception = re @@ -444,6 +456,43 @@ class TacticNotationsParser ( Parser ): self.exitRule() return localctx + class MetaContext(ParserRuleContext): + + def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): + super().__init__(parent, invokingState) + self.parser = parser + + def METACHAR(self): + return self.getToken(TacticNotationsParser.METACHAR, 0) + + def getRuleIndex(self): + return TacticNotationsParser.RULE_meta + + def accept(self, visitor:ParseTreeVisitor): + if hasattr( visitor, "visitMeta" ): + return visitor.visitMeta(self) + else: + return visitor.visitChildren(self) + + + + + def meta(self): + + localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state) + self.enterRule(localctx, 12, self.RULE_meta) + try: + self.enterOuterAlt(localctx, 1) + self.state = 61 + self.match(TacticNotationsParser.METACHAR) + except RecognitionException as re: + localctx.exception = re + self._errHandler.reportError(self, re) + self._errHandler.recover(self, re) + finally: + self.exitRule() + return localctx + class AtomicContext(ParserRuleContext): def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1): @@ -468,10 +517,10 @@ class TacticNotationsParser ( Parser ): def atomic(self): localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state) - self.enterRule(localctx, 12, self.RULE_atomic) + self.enterRule(localctx, 14, self.RULE_atomic) try: self.enterOuterAlt(localctx, 1) - self.state = 58 + self.state = 63 self.match(TacticNotationsParser.ATOM) except RecognitionException as re: localctx.exception = re @@ -505,10 +554,10 @@ class TacticNotationsParser ( Parser ): def hole(self): localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state) - self.enterRule(localctx, 14, self.RULE_hole) + self.enterRule(localctx, 16, self.RULE_hole) try: self.enterOuterAlt(localctx, 1) - self.state = 60 + self.state = 65 self.match(TacticNotationsParser.ID) except RecognitionException as re: localctx.exception = re diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py index 80e69d433..c0bcc4af3 100644 --- a/doc/tools/coqrst/notations/TacticNotationsVisitor.py +++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py @@ -39,6 +39,11 @@ class TacticNotationsVisitor(ParseTreeVisitor): return self.visitChildren(ctx) + # Visit a parse tree produced by TacticNotationsParser#meta. + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + return self.visitChildren(ctx) + + # Visit a parse tree produced by TacticNotationsParser#atomic. def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext): return self.visitChildren(ctx) @@ -50,4 +55,4 @@ class TacticNotationsVisitor(ParseTreeVisitor): -del TacticNotationsParser
\ No newline at end of file +del TacticNotationsParser diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py index d91bbb64c..44212d788 100644 --- a/doc/tools/coqrst/notations/html.py +++ b/doc/tools/coqrst/notations/html.py @@ -42,6 +42,9 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor): def visitHole(self, ctx:TacticNotationsParser.HoleContext): tags.span(ctx.ID().getText()[1:], _class="hole") + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + tags.span(ctx.METACHAR().getText()[1:], _class="meta") + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): tags.span(" ") # TODO: no need for a <span> here diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py index 73be6f26e..506240d90 100644 --- a/doc/tools/coqrst/notations/parsing.py +++ b/doc/tools/coqrst/notations/parsing.py @@ -12,7 +12,7 @@ from .TacticNotationsParser import TacticNotationsParser from antlr4 import CommonTokenStream, InputStream -SUBSTITUTIONS = [("@bindings_list", "{+ (@id := @val) }"), +SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"), ("@qualid_or_string", "@id|@string")] def substitute(notation): diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index 5d4501892..f6e82fc68 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -41,6 +41,9 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor): def visitHole(self, ctx:TacticNotationsParser.HoleContext): self.buffer.write("‘{}’".format(ctx.ID().getText()[1:])) + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + self.buffer.write(ctx.METACHAR().getText()[1:]) + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): self.buffer.write(" ") diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py index cac6aaecb..ea820c719 100644 --- a/doc/tools/coqrst/notations/regexp.py +++ b/doc/tools/coqrst/notations/regexp.py @@ -47,6 +47,9 @@ class TacticNotationsToRegexpVisitor(TacticNotationsVisitor): def visitHole(self, ctx:TacticNotationsParser.HoleContext): self.buffer.write("([^();. \n]+)") # FIXME could allow more things + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + self.buffer.write(re.escape(ctx.METACHAR().getText()[1:])) + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): self.buffer.write(r"\s+") diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index 889bf70a4..26a5f6968 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -20,6 +20,8 @@ from .TacticNotationsVisitor import TacticNotationsVisitor from docutils import nodes from sphinx import addnodes +import sys + class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): def defaultResult(self): return [] @@ -62,6 +64,12 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): node = nodes.inline(hole, token_name, classes=["hole"]) return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)] + def visitMeta(self, ctx:TacticNotationsParser.MetaContext): + meta = ctx.METACHAR().getText() + metachar = meta[1:] # remove escape char + token_name = metachar + return [nodes.inline(metachar, token_name, classes=["meta"])] + def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): return [nodes.Text(" ")] |