Re: [isabelle] Macro to comment and uncomment selected text so I don't get error?



At least part of the problem is a "(*" and "*)" (or other sets of matched delimiters) not being inserted on the same line.

I do this with my modified "Add_Prefix_and_Suffix.bsh" or with "Edit / Source / Range Comment",

    (*
    find_consts name:List.list.Nil
    value "a # b # List.Nil"
    *)

and it results in an error until I save the file or delete the block and reinsert it.

I do this with "Add_Prefix_and_Suffix.bsh" or "Edit / Source / Line Comment",

    (*find_consts name:List.list.Nil*)
    (*value "a # b # List.Nil"*)

and I get no errors.

That's a workaround to commenting out code, but only if I have a macro that will uncomment it line by line.

More details. I do this with my modified "Add_Prefix_and_Suffix.bsh", and I get no errors:

    text{*value "a # b # List.Nil"
    value "a # b # List.Nil"*}

I do this, and I get errors:

    text{*value "a # b # List.Nil"
    value "a # b # List.Nil"
    value "a # b # List.Nil"*}

So if the "text{*" and "*} get inserted over more than two lines, then I get the error, and the same thing with "(*" and "*)".

It's never simple. Using my modified macro, this gets no error with the blank line in between:

    (*value "a # b # List.Nil"

    value "a # b # List.Nil"*)

Regards,
GB






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.