Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: PIDE is able to load theory markup from underlying ...

Email Gateway (Jun 30 2025 at 18:55):

From: Makarius <makarius@sketis.net>
* General *

• A Prover IDE session, e.g. in Isabelle/jEdit or Isabelle/VSCode, is
  now able to load markup and messages from the underlying session
  database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory
  "HOL.Nat" in session "HOL". This information is read-only: editing
  theory sources in the editor will invalidate formal markup, and replace
  it by an error message.

This refers to Isabelle/476627cac12e.

It addresses an old omission from our great Prover IDE. It now behaves like
IntellJ IDEA when jumping into "jar" files of the background library.

Makarius

Email Gateway (Jul 03 2025 at 18:53):

From: Makarius <makarius@sketis.net>
On 03/07/2025 16:34, Lawrence Paulson wrote:

This is cool and totally great. I hope we don't pay a price in memory usage?

There is no change on the Isabelle/ML side.

On the Isabelle/Scala side, the memory usage should be the same as if the
theory had been loaded interactively into the Prover IDE.

Nonetheless, we need to watch out for irregularities, after many years without
that functionality.

Makarius

Email Gateway (Jul 04 2025 at 06:21):

From: Tobias Nipkow <nipkow@in.tum.de>
I almost missed this improvement, which is indeed totally great!

Tobias

On 03/07/2025 20:52, Makarius wrote:

On 03/07/2025 16:34, Lawrence Paulson wrote:

This is cool and totally great. I hope we don't pay a price in memory usage?

There is no change on the Isabelle/ML side.

On the Isabelle/Scala side, the memory usage should be the same as if the theory
had been loaded interactively into the Prover IDE.

Nonetheless, we need to watch out for irregularities, after many years without
that functionality.

Makarius

smime.p7s

Last updated: Jul 12 2025 at 16:25 UTC