Custom Query (361 matches)

In prover output, the special characters ? and ' seem to be missing. For example:

lemma "A --> A" ..

In the response there is only "A" not "?A", as could be expected with show_question_marks := false.

Same effect for typ 'a --- only a named "a" is displayed.

Copy/paste works -- the characters show up in the source as expected.

GNU Emacs 22.1.1, Ubuntu 8.04 LTS, Isabelle2009.

The span passed to isar-positions-of includes the whitespace before the actual command keyword. The latter is the start of the actual string passed on to the prover. Thus the line position comes out incorrect. For example:

theory Scratch imports Pure begin
ML {* Binding.pos_of @{binding x} *}

This produces a position with line 1, column 58, but the line should be 2. Column is garbled, too.

(Interestingly, after asserting the command the cursor jumps back to the span start. Should this be the end instead?)

In isar-symbol-shortcuts there are some odd abbreviations, notably |> which is very common in Isabelle/ML, but its expansion \<triangleright> is very rare.

Anyway, how can the user prevent unwanted expansion? In X-Symbol mode, plain editor undo would revert to the original, but now it just reverst to the ASCII form of the replaced symbol. Of course, editor quote *before* editing works, but is a bit cumbersome.