NEWS: PIDE is able to load theory markup from underlying database

Makarius makarius at sketis.net
Mon Jun 30 20:54:40 CEST 2025


*** 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



More information about the isabelle-dev mailing list