different styles of comment

[ElifUskuplu]

Hi, is it possible to support two different styles of comment in proof general? For example, suppose I have

{` this is a comment block, 
it allows multiple lines `}

` this is a comment line, it must be just one line

How can I configure PG accordingly?

[Matafou]

I think this is standard in emacs. You define comment starters and enders in the syntax table. This is a bit convoluted for two-letters comment delimiters:

Look at https://www.gnu.org/software/emacs/manual/html_node/elisp/Syntax-Descriptors.html

You can have a look at coq-menu.el

[Matafou]

I think this should help.

[ElifUskuplu]

P.S: I edited my first entry to write my concrete syntax for comments.

@Matafou If I'm not mistaken, with modifying syntax table, we don't need to set variables like proof-script-comment-start. I mean I have

(defconst PA-mode-syntax-table-entries
  (append '(?\` "< 23b")
          '(?\n "> b")
          '(?\{ "(}1nb")
          '(?\} "){4nb")))

and

(proof-easy-config  'pa "PA"   
   ;;other configurations
   proof-script-syntax-table-entries     PA-mode-syntax-table-entries)

Comment highlighting works as I expected. When I load the commands, it seems the comment lines and blocks are captured as expected. Is there something I missed? What I mean is, does the proof-script-comment-start configuration affect other things too?

[Matafou]

It is used in the generic code of proofgeneral. In particular when PG splits a file into a sequence of commands and comments. Otherwise a comment is "glued" to the next command. I think it will work ok without, but it is better to define it. May be a matter of taste though.

PG amso sets comment-end and comment-start according to these variables (see comment-region and co).

[ElifUskuplu]

@Matafou I think when proof-script-comment-start and proof-script-comment-end are defined, a comment is "glued" to the next comand. Let me provide more configuration details

(proof-easy-config  'pa "PA"   
   ;;other configurations
   proof-script-syntax-table-entries     PA-mode-syntax-table-entries
   proof-script-comment-start            "{`"
   proof-script-comment-end              "`}"
   proof-script-command-start-regexp     "\\<\\(axiom\\|def\\)\\>"
 )

With this, next command is passing from a command to another one omitting the comments. I understand from your saying that "gluing" occurs without these two definitions. That's why I confused. Maybe, the problem is that I only defined proof-script-command-start-regexp, so next command is just passing one to another because of this. Is that correct?

PG amso sets comment-end and comment-start according to these variables (see comment-region and co).

Is there any reference for this? I would like to read it.

[Matafou]

I think the gluing behaviour becomes optional when these variables are set.

I don't know if this is documented but I just grepped "comment-start" in the generic directory and this seemed clear from comments there.