search

easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
30 stars 1 forks source link

nested comments confuse Proof General (but not the client) #43

Closed alleystoughton closed 9 months ago

alleystoughton commented 11 months ago

nested comments confuse Proof General (but not the client)

alleystoughton commented 10 months ago

EasyCrypt's Proof General script handles this by setting a single local variable. But it also doesn't use the proof-easy-config easy configuration mechanism. Not clear if setting this variable in some hook is enough to get the right behavior.

This issue is of moderate priority, as it's common to want to comment-out a part of a script, temporarily, and that part may have comments.

01tomislav commented 10 months ago

Couldn't find the right spot to set the local variable. (set (make-local-variable 'comment-quote-nested) nil) Tried in a bunch of places, also in proof general code, nothing worked. There is a workaround with quotes like this (*"(*)")

01tomislav commented 10 months ago

apparently GitHub also has problems with nested comments (*"(*)")

01tomislav commented 10 months ago

should look like this (*\"(*)\"\)

alleystoughton commented 10 months ago

Yes, this may not be fixable while using proof-easy-config. I tried setting the variable by hand in the script buffer, but it has no effect.