Re: [isabelle-dev] NEWS: PIDE document maintains file content internally

2017-01-10 Thread Makarius 
On 08/01/17 20:02, Makarius wrote:
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> 
> * The PIDE document model maintains file content independently of the
> status of jEdit editor buffers. Reloading jEdit buffers no longer causes
> changes of formal document content. Theory dependencies are always
> resolved internally, without the need for corresponding editor buffers.
> The system option "jedit_auto_load" has been discontinued: it is
> effectively always enabled.
> 
> 
> This refers to Isabelle/9c69b495c05d.

Here is a small add-on (Isabelle/e7220f4de11f):

* The Theories dockable provides a "Purge" button, in order to restrict
the document model to theories that are required for open editor
buffers.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: PIDE document maintains file content internally

2017-01-09 Thread Lawrence Paulson 
On 8 Jan 2017, at 19:02, Makarius  wrote:
> 
> * The PIDE document model maintains file content independently of the
> status of jEdit editor buffers. Reloading jEdit buffers no longer causes
> changes of formal document content. Theory dependencies are always
> resolved internally, without the need for corresponding editor buffers.
> The system option "jedit_auto_load" has been discontinued: it is
> effectively always enabled.

I’ve tried this, and it’s terrific. One slight problem however: I’ve been using 
the “goto-error” extension, and it no longer works. I hope that RafalThis can 
cook up a new version soon.

Larry


/*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 */

/*
 * Jump to first Isabelle error in text area (if available).
 *
 * by Rafal Kolanski (2015)

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev