[isabelle] Qualified theory imports and isabelle jedit -l â -R â



Dear all,

when inspecting a Âbroken session (let as assume, HOL-Number_Theory), I
used to invoke

> isabelle jedit -l HOL-Number_Theory -R ../Number_Theory/Number_Theory.thy
	
and everything worked out smoothly.

With qualified theory imports emerged in future Isabelle2017, this is no
longer the case: theory ÂResidues chokes on imports from HOL-Algebra.

Inspecting the corresponding session entry in src/HOL/ROOT:

> session "HOL-Number_Theory" (timing) in Number_Theory = "HOL-Computational_Algebra" +
>   â
>   sessions
>     "HOL-Algebra"
>   â

it seems to be the case that -R operates on the direct ancestor session
HOL-Computational_Algebra but not on the Âside path HOL-Algebra.

Is that intended? I have the feeling that the current behaviour would
diminish the usability of -R considerably.

Cheers,
    Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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