39 is implemented in Isabelle/ML. The traditional prover command loop is |
39 is implemented in Isabelle/ML. The traditional prover command loop is |
40 given up; instead there is direct support for editing of source text, with |
40 given up; instead there is direct support for editing of source text, with |
41 rich formal markup for GUI rendering. |
41 rich formal markup for GUI rendering. |
42 |
42 |
43 \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close> |
43 \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close> |
44 implemented in Java\<^footnote>\<open>\<^url>\<open>https://adoptopenjdk.net\<close>\<close>. It is easily |
44 implemented in Java\<^footnote>\<open>\<^url>\<open>https://openjdk.java.net\<close>\<close>. The editor is easily |
45 extensible by plugins written in any language that works on the JVM. In |
45 extensible by plugins written in any language that works on the JVM. In |
46 the context of Isabelle this is always |
46 the context of Isabelle this is usually |
47 Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>. |
47 Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>. |
48 |
48 |
49 \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the |
49 \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the |
50 default user-interface for Isabelle. It targets both beginners and |
50 default user-interface for Isabelle. It targets both beginners and |
51 experts. Technically, Isabelle/jEdit consists of the original jEdit code |
51 experts. Technically, Isabelle/jEdit consists of the original jEdit code |