Custom Query (361 matches)

Hi,

in the Proof General documentation at http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+user+manual&file=releases%2FProofGeneral%2Fdoc%2FProofGeneral%2FProofGeneral_11.html#Multiple-File-Support the link for "Current Limitations", pointing to subsubsection 10.2.4 does not work. The other links for subsubsections do not work as well.

The text of these subsubsections is present and on http://proofgeneral.inf.ed.ac.uk/userman the link to 10.2.4 _does_ work.

If I compile the documentation myself and view it on the hard disk, the links do also work.

Bye,

Hendrik

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?)

if i parse a theory passed the "end" point, "undo" no longer works; ("undo all" sometimes does, but "undo" should give an error at least)

i'm also not sure it correctly registers that the theory is closed, when i switch to another theory it wouldn't let me activate it (but that could be do to a failed retract...)