max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add temporary staging workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-08 20:11:16 -08:00
parent 01c5b0710c
commit d92e59a6fb
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Lean/Parser/Parser.lean
View file

@ -1453,8 +1453,14 @@ def mkBuiltinParsingTablesRef : IO (IO.Ref ParsingTables) := IO.mkRef {}
@[init mkBuiltinParsingTablesRef] constant builtinTermParsingTable : IO.Ref ParsingTables := arbitrary _
@[init mkBuiltinParsingTablesRef] constant builtinLevelParsingTable : IO.Ref ParsingTables := arbitrary _
@[init mkBuiltinParsingTablesRef] constant builtinCommandParsingTable : IO.Ref ParsingTables := arbitrary _
def addBuiltinLeadingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser) : IO Unit := pure ()
def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit := pure ()
def addBuiltinLeadingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser) : IO Unit :=
condM (tablesRef.ptrEq builtinTermParsingTable) (addBuiltinLeadingParserNew `term declName p) $
condM (tablesRef.ptrEq builtinLevelParsingTable) (addBuiltinLeadingParserNew `level declName p) $
(addBuiltinLeadingParserNew `command declName p)
def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit :=
condM (tablesRef.ptrEq builtinTermParsingTable) (addBuiltinTrailingParserNew `term declName p) $
condM (tablesRef.ptrEq builtinLevelParsingTable) (addBuiltinTrailingParserNew `level declName p) $
(addBuiltinTrailingParserNew `command declName p)
--- END TODO DELETE --
private def ParserExtension.addEntry (s : ParserExtensionState) (e : ParserExtensionEntry) : ParserExtensionState :=