*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Proof_Context abstraction*From*: Makarius <makarius at sketis.net>*Date*: Wed, 30 Jul 2014 23:05:51 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk, Joachim Breitner <breitner at kit.edu>*In-reply-to*: <53D89D60.3020704@in.tum.de>*References*: <1406624447.10918.13.camel@kit.edu> <alpine.LNX.2.00.1407291947350.55056@lxbroy10.informatik.tu-muenchen.de> <1406668260.30054.3.camel@kit.edu> <53D88D65.30409@in.tum.de> <1406704452.1675.4.camel@kit.edu> <53D89D60.3020704@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 30 Jul 2014, Lars Hupel wrote:

And for code in my own modules Ctrl-Hover is very helpful, but thatdoesn’t work in ML files that have been loaded in the heap. Is theremaybe a way to get jEdit process Pure (instead of loading a Heap)?As far as I know, that is only possible for theories loaded *after* Purehas been bootstrapped. You're probably out of luck there.

Makarius

**References**:**[isabelle] Proof_Context abstraction***From:*Joachim Breitner

**Re: [isabelle] Proof_Context abstraction***From:*Makarius

**Re: [isabelle] Proof_Context abstraction***From:*Joachim Breitner

**Re: [isabelle] Proof_Context abstraction***From:*Lars Hupel

**Re: [isabelle] Proof_Context abstraction***From:*Joachim Breitner

**Re: [isabelle] Proof_Context abstraction***From:*Lars Hupel

- Previous by Date: Re: [isabelle] check phases
- Next by Date: Re: [isabelle] Proof_Context abstraction
- Previous by Thread: Re: [isabelle] Proof_Context abstraction
- Next by Thread: Re: [isabelle] Proof_Context abstraction
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list