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