Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle/jEdit building workflow


view this post on Zulip Email Gateway (Aug 14 2023 at 08:25):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Hi there,

is it possible to build and then use the source in
IsabelleXXXX/contrib/jedit-20XXYYZZ ? Is there a documented workflow for
this?

view this post on Zulip Email Gateway (Aug 14 2023 at 12:20):

From: Makarius <makarius@sketis.net>
In Isabelle2023-RC3 there is an administrative tool "isabelle
component_jedit", where "administrative" means you need to run from an
Isabelle repository clone, such as
https://isabelle.sketis.net/repos/isabelle-release

Afterwards you need to replace the Admin/components/main configuration
according, e.g. see this past changeset:
https://isabelle.sketis.net/repos/isabelle-release/rev/a755733c1eb5

What are you trying to do? This is definitely an administrative operation and
not expected from regular users.

Makarius

view this post on Zulip Email Gateway (Aug 14 2023 at 12:39):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
I am to make jEdit to output the typeset theory file through the JTextArea
object.

view this post on Zulip Email Gateway (Aug 14 2023 at 14:40):

From: Makarius <makarius@sketis.net>
I don't understand.

Maybe the misunderstanding is based on the conflation of "jEdit" (the plain
text editor) and "Isabelle/jEdit" (the Isabelle Prover IDE based on jEdit).

For the latter, the sources are in src/Tools/jEdit/src and rebuild implicitly
on startup of "isabelle jedit" --- for Isabelle repository version.

It is probably also possible to make a regular Isabelle/jEdit plugin as
Isabelle/Scala component (with etc/build.props). See also chapter 5 of
"isabelle doc system".

My guess is that it will require some delicate tinkering of jEdit properties
somewhere.

(Don't count on me to provide anything right now, as we are heading towards a
stable release, and I am busy elsewhere.)

Makarius

view this post on Zulip Email Gateway (Aug 14 2023 at 15:14):

From: Makarius <makarius@sketis.net>
Why this confusion of terminology, for no particular reason?

Makarius

view this post on Zulip Email Gateway (Aug 14 2023 at 15:20):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Thanks, these are good starting points for me.

And yes, in the context of the Isabelle mailing list when I talk about
jEdit I mean Isabelle/jEdit.


Last updated: Apr 28 2024 at 20:16 UTC