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

chore(library/init/meta/interactive_base): remove Lean3 format macros

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-05 16:29:12 -07:00
parent bd7138349a
commit 50ce4e8ae9
1 changed files with 0 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
library/init/meta/interactive_base.lean
View file

@ -200,41 +200,3 @@ meta structure inductive_decl :=
meta constant inductive_decl.parse : decl_meta_info → parser inductive_decl
end interactive
section macros
open interaction_monad
open interactive
private meta def parse_format : string → list char → parser pexpr
| acc [] := pure ``(to_fmt %%(reflect acc))
| acc ('\n'::s) :=
do f ← parse_format "" s,
pure ``(to_fmt %%(reflect acc) ++ format.line ++ %%f)
| acc ('{'::'{'::s) := parse_format (acc ++ "{") s
| acc ('{'::s) :=
do (e, s) ← with_input (lean3.parser.pexpr 0) s.as_string,
'}'::s ← return s.to_list | fail "'}' expected",
f ← parse_format "" s,
pure ``(to_fmt %%(reflect acc) ++ to_fmt %%e ++ %%f)
| acc (c::s) := parse_format (acc.str c) s
reserve prefix `format! `:100
@[user_notation]
meta def format_macro (_ : parse $ tk "format!") (s : string) : parser pexpr :=
parse_format "" s.to_list
private meta def parse_sformat : string → list char → parser pexpr
| acc [] := pure $ pexpr.of_expr (reflect acc)
| acc ('{'::'{'::s) := parse_sformat (acc ++ "{") s
| acc ('{'::s) :=
do (e, s) ← with_input (lean3.parser.pexpr 0) s.as_string,
'}'::s ← return s.to_list | fail "'}' expected",
f ← parse_sformat "" s,
pure ``(%%(reflect acc) ++ to_string %%e ++ %%f)
| acc (c::s) := parse_sformat (acc.str c) s
reserve prefix `sformat! `:100
@[user_notation]
meta def sformat_macro (_ : parse $ tk "sformat!") (s : string) : parser pexpr :=
parse_sformat "" s.to_list
end macros