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


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

2017-01-08 Thread Makarius
*** 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. It is a substantial reform of PIDE
file management to make things more scalable. A few more consequences of
it are still in the pipeline: the ultimate goal (since 2013) is to load
all of AFP into one big PIDE session!

Moreover the accidental meaning of "Reload" and "Reload All" to restart
formal processing has disappeared. I occasionally used that for testing
purposes -- now that needs to be done by actual edits.


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