feat: Migrate #print prefix from Mathlib

[joehendrix]

This migrates #print prefix while doing some migration of functionality naming to std conventions.

This also restricts the long line check to Std. I had some long lines in the test case file that aren't easy to fix.

[semorrison]

Mario once told me he prefers not to close namespaces if it is only being done at the end of the file. I forget why, however.

I would actually prefer the opposite convention, as it makes it easier doing single-file-minimization (i.e. you can copy a file into a section of another, and only have to move the imports, not adjust namespaces too).

[joehendrix]

I don't have a preference personally. You make a good point, but I deleted them for consistency with similar files.

[fgdorais]

Maybe these coding conventions should be recorded somewhere. I also did not know about that one!

[digama0]

The rule is that you shouldn't close the "main namespace" of the file, to make it easier to end-extend the file. I can also see the point regarding closing the main namespace, but you would have to also put everything in a section in order to really ensure that joining files "just works", because there could also be variables or options outside the namespace (if there even is a namespace).

[semorrison]

Otherwise LGTM.

[fgdorais]

This is better than my personal version, so I'm approving but I do have a question in the review comments.

[fgdorais]

My personal version of used "#print" &"prefix" rather than "#print prefix". I'm not sure my version is better but I am interested in learning more about the difference. (It's been so long I don't remember why I did that!)

[joehendrix]

It looks like this dates back at least to when it was checked into Mathlib by @digama0

[digama0]

"#print " "prefix " is better if the intent is to allow more or less whitespace between the tokens. One probably needs to also add a colGt or something, or else unfinished #print statements cannot be differentiated from #print prefix where the prefix just happens to be the next command. The current version "#print prefix " requires exactly one space between #print and prefix, which makes it quite unambiguous but may be seen as undesirable.

The & before "prefix" means that it won't make prefix a token (i.e. not legal as an identifier in e.g. def prefix := 1), but this doesn't make a difference because prefix is already a token (it's a command keyword used for prefix notations). It will parse the next token as an identifier and this may clash with regular #print ident though, so using the token form seems better.

[joehendrix]

Interesting, I needed to learn this. It seems like I should allow whitespace, but I noticed that i also need withPosition

Consider these two examples:

#print
  prefix
  Nat

#print
prefix
Nat

I think I want to parse the first, but not the second. However the line below parses both:

syntax (name := printPrefix) "#print " (colGt "prefix ") (colGt ident) : command

This works though:

syntax (name := printPrefix) withPosition("#print " (colGt "prefix ") (colGt ident)) : command

Any feedback? I was surprised I needed an explicit withPosition since other similar examples didn't seem to use it.

[digama0]

Yes, you will need a withPosition because commands are parsed at the top level and this doesn't have a position set. (Tactics, by contrast, appear somewhere after a by and this sets the position.)