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

feat: close the loop

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-11 19:32:52 +02:00 • committed by Leonardo de Moura
parent 6492fb5d80
commit aefe710caf
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Lean/Parser.lean
View file

@ -10,3 +10,14 @@ import Lean.Parser.Tactic
import Lean.Parser.Command
import Lean.Parser.Module
import Lean.Parser.Syntax
namespace Lean
namespace Parser
-- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
@[export lean_mk_antiquot_parenthesizer]
def mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : PrettyPrinter.Parenthesizer :=
mkAntiquot.parenthesizer name kind anonymous
end Parser
end Lean

2
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -210,7 +210,7 @@ catch p1 $ fun e => match e with
-- Note that there is a mutual recursion
-- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
-- anyway.
--@[extern "lean_mk_antiquot_parenthesizer"]
@[extern 7 "lean_mk_antiquot_parenthesizer"]
constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer :=
arbitrary _