Re: [isabelle] Isabelle2014-RC0: symbol completion in antiquotations

On Wed, 9 Jul 2014, Andreas Lochbihler wrote:

I don't know how I could find out which language context I am currently working in. Maybe it suffices to display the language context of the curser somewhere in Isabelle

This is done with the ubiquitious C-hover idiom: it produces a popup saying "language: NAME". The other flags for the language are not printed, but accessible dynamically in SideKick with "isabelle-markup" parser in the status window:

  <language name="NAME" symbols="false" antiquotes="false" delimited="true"/>

Or you look in ~~/src/Pure/PIDE/markup.ML for the language contexts that are presently used in Isabelle/Pure -- but tools could invent their own.

To make this exploration more fun, consider this formal Isar source:

  text ‹ see @{file "~~/src/Pure/PIDE/markup.ML"} ›

Here the file-system path specification has language context "path", because the "file" antiquotation has provided that semantic information. This means that file-name completion is active in PIDE: you can type some prefix of it and use C+b to get more from the directory content.

If this is madness, there is method in it ...


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