Re: [isabelle] Isabelle2014-RC0 available for testing



On Tue, 8 Jul 2014, Joachim Breitner wrote:

* I just observed an error message in the output window:
       Undefined constant: "list.size"⌂
 And I wonder what the ⌂ is about.

General PIDE principle: use C-hover to ask about what you see. Here it will give you a visual clue that it is a hyperlink -- the one stemming from a symbolic position.

IIRC, there is no explicit documentation of this new \<here> (or "house" / "home") symbol, but the general principles are now quite explicit in the Isabelle/jEdit manual.


	Makarius


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