Travel time F #! This is by design. Block comments can be nested, and lines in block comments are marked as regular lines . Valid char literals are considered "strings" in this case.
So these are valid block comments:
(* "embedded string, this --> *) doesn't close the comment" *) (* (* nested *) comment *) (* quote considered to be in char literal '"' is ok *)
But it is not
(* "this string is not closed *) (* " this quote --> \" is escaped inside a string *)
And as if it werenβt so simple, there is a special treatment for operators starting with * , since (*) and the like, as a rule, the beginning or the end of a block comment will be considered.
(* I can talk about the operator (*) without ending my comment *)
AFAIK, they are all inherited from ML (nested comments are definitely not sure about the lines).
So, for your purposes, you can do something like this:
(* Character Meaning ------------------------------- " \' " Single Quote " \" " Double Quote or '\'' Single Quote '"' Double Quote *)
source share