Custom Query (361 matches)

[message from Lucas Dixon]

(PG: 4.0pre090916) I used to sprinkle semi-colon's around my theory files so that I could quickly introduce new syntax. I noticed recently that this now has some annoying behaviour:

; ;

now produces:

*** Outer syntax error: exactly one command expected

It would be nicer (for me) if it still treated ";" as a command separator, and let them have whitespace between.

The same error crops up in a couple of other places:

type:

ML{*
val _ = 1;
*}

process this then add:

;
ML{*
val _ = 2;
*}

same error.

Also:

(*foo*)
;

Special messages, such as priority ones, but probably also tracing, are often duplicated in the output. The *isabelle* buffer contains messages only once, as expected.

This has been reported on Ubuntu with Emacs 23, but also other combinations.

Editing text doesn't always change the document model underlying. Then sending the next command sends the old text.