On 31/01/2019 23:11, Makarius wrote:
> *** Isabelle/jEdit Prover IDE ***
>
> * The jEdit File Browser is more prominent in the default GUI layout of
> Isabelle/jEdit: various virtual file-systems provide access to Isabelle
> resources, notably via "favorites:" (or "Edit Favorites").
There is an
*** Isabelle/jEdit Prover IDE ***
* The jEdit File Browser is more prominent in the default GUI layout of
Isabelle/jEdit: various virtual file-systems provide access to Isabelle
resources, notably via "favorites:" (or "Edit Favorites").
* Action "isabelle-export-browser" points the File Browser
*** Isabelle/jEdit Prover IDE ***
* System option "jedit_text_overview" allows to disable the text
overview column.
This refers to Isabelle/5a8ae7a4b7d0 -- it is a minor visual enhancement
for situations where the editor screen should look like a presentation,
without any distractions by extra
On 31/01/2019 20:37, Mathias Fleury wrote:
>
>> On 31. Jan 2019, at 20:10, Makarius >
>> Can you point to these special applications?
>>
>> If export_code uses Generated_Files.add_files (in addition to
>> Export.export) we get both a check for unique names and an easy way to
>> retrieve the
Hi Makarius,
> On 31. Jan 2019, at 20:10, Makarius wrote:
>
> On 31/01/2019 18:27, Peter Lammich wrote:
>> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
>>> I have looked around at typical uses of 'export_code' in AFP. Most of
>>> the time it is just informative: writing a file and looking
On 31/01/2019 18:27, Peter Lammich wrote:
> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
>> I have looked around at typical uses of 'export_code' in AFP. Most of
>> the time it is just informative: writing a file and looking at it in
>> the
>> editor (or via the command-line!?), or doing that
On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
> I have looked around at typical uses of 'export_code' in AFP. Most of
> the time it is just informative: writing a file and looking at it in
> the
> editor (or via the command-line!?), or doing that on the output
> channel.
> The isabelle-export:
On 14/01/2019 20:20, Florian Haftmann wrote:
>
>> * Are there remaining uses of 'file' with empty name? Is the virtual
>> file-system browser sufficiently convenient to inspect results
>> interactively?
>
> I checked the file system browser and would be quite content with it; as
> a bonus you
On 22/01/2019 22:24, Florian Haftmann wrote:
>
> as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
> seen Local_Theory.reset invocations are gone, conveniently replaced by
> Local_Theory.subtarget_result.
This looks clean and canonical. At least we have Local_Theory.reset
