Re: [isabelle] Isabelle2017-RC0: jEdit plugin insists all files for all sessions are present



> Maybe we should advertize $ISABELLE_HOME_USER/ROOTS to users more
> prominently. At some point the Prover IDE might provide an editor for
> that: at the moment it just means to open that text file directly using
> the above symbolic name (maybe I should add a menu item for that).

Alternatively, another possibility could be to provide an Isabelle tool
and/or jEdit action to do it automatically. It could be as simple as

  isabelle add_root /path/to/afp

... and/or a corresponding action in jEdit. I posit that that could be
useful to many users. Using the AFP is a disruption to the otherwise
quite nice workflow of "extract Isabelle and it just works".

> Performance is one problem, and polluting the logical session name space
> another (i.e. the important option "-a" becomes hardly usable).

Is the latter really a problem? I thought this is what session groups
are for, i.e. "build -g afp" instead of "build -D $AFP".

But surely adding the AFP to "$ISABELLE_HOME_USER/ROOTS" would also give
these drawbacks.

Cheers
Lars




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