# HG changeset patch
# User wenzelm
# Date 1730845667 -3600
# Node ID c5a61c7e27251ccbc41f43cb24b8bef135cd2881
# Parent d026fa14433bf2d27dc466f133b92d4fe710f2a4# Parent 95cb584cb77714fd7a8d259e8af96248873e5ee2
merged
diff -r d026fa14433b -r c5a61c7e2725 Admin/components/components.sha1
--- a/Admin/components/components.sha1 Tue Nov 05 19:59:30 2024 +0100
+++ b/Admin/components/components.sha1 Tue Nov 05 23:27:47 2024 +0100
@@ -202,6 +202,7 @@
d4b43d1be10c9cffb406faeb36e9d46027834980 jdk-21.0.1.tar.gz
94f27b086cf6a2fb305cc961fe2932d8ea3634af jdk-21.0.2.tar.gz
c4e05634d371a305c982b6ce5478df42fd1ad9c5 jdk-21.0.3.tar.gz
+8414b3c9f4fe1f9f5a1590f3abd33f0a017e35b9 jdk-21.0.5.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
diff -r d026fa14433b -r c5a61c7e2725 Admin/components/main
--- a/Admin/components/main Tue Nov 05 19:59:30 2024 +0100
+++ b/Admin/components/main Tue Nov 05 23:27:47 2024 +0100
@@ -13,7 +13,7 @@
isabelle_fonts-20211004
isabelle_setup-20240327
javamail-20240109
-jdk-21.0.3
+jdk-21.0.5
jedit-20241101
jfreechart-1.5.3
jortho-1.0-2
diff -r d026fa14433b -r c5a61c7e2725 NEWS
--- a/NEWS Tue Nov 05 19:59:30 2024 +0100
+++ b/NEWS Tue Nov 05 23:27:47 2024 +0100
@@ -127,6 +127,10 @@
formal markup by the prover. Repeated invocation of this action extends
the selection incrementally.
+* The "Documentation" panel supports plain text files again, notably
+"jedit-changes". This was broken in Isabelle2022, Isabelle2023,
+Isabelle2024.
+
* Update to jEdit 5.7.0, the latest release.
diff -r d026fa14433b -r c5a61c7e2725 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Pure/Admin/build_doc.scala Tue Nov 05 23:27:47 2024 +0100
@@ -71,8 +71,8 @@
if (errs.nonEmpty) error(cat_lines(errs))
if (view) {
- for (doc <- Doc.main_contents().docs if docs.contains(doc.name)) {
- Doc.view(doc.path)
+ for (entry <- Doc.main_contents().entries(name = docs.contains, pdf = true)) {
+ entry.view()
}
}
}
diff -r d026fa14433b -r c5a61c7e2725 src/Pure/Admin/component_jdk.scala
--- a/src/Pure/Admin/component_jdk.scala Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Pure/Admin/component_jdk.scala Tue Nov 05 23:27:47 2024 +0100
@@ -33,8 +33,8 @@
/* build jdk */
val default_base_url = "https://cdn.azul.com/zulu/bin"
- val default_jdk_version = "21.0.3"
- val default_zulu_version = "21.34.19-ca"
+ val default_jdk_version = "21.0.5"
+ val default_zulu_version = "21.38.21-ca"
def build_jdk(
target_dir: Path = Path.current,
diff -r d026fa14433b -r c5a61c7e2725 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Pure/General/http.scala Tue Nov 05 23:27:47 2024 +0100
@@ -363,8 +363,8 @@
p <- request.uri_path if p.is_pdf
s = p.implode if s.startsWith("web/")
name = p.base.split_ext._1.implode
- doc <- doc_contents.docs.find(_.name == name)
- } yield Response.read(doc.path)
+ entry <- doc_contents.entries(name = _ == name, pdf = true).headOption
+ } yield Response.read(entry.path)
override def apply(request: Request): Option[Response] =
doc_request(request) orElse super.apply(request)
diff -r d026fa14433b -r c5a61c7e2725 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Pure/ROOT.ML Tue Nov 05 23:27:47 2024 +0100
@@ -373,4 +373,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
-
diff -r d026fa14433b -r c5a61c7e2725 src/Pure/ROOT.scala
--- a/src/Pure/ROOT.scala Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Pure/ROOT.scala Tue Nov 05 23:27:47 2024 +0100
@@ -29,3 +29,4 @@
def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
}
+
diff -r d026fa14433b -r c5a61c7e2725 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Pure/Tools/doc.scala Tue Nov 05 23:27:47 2024 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/doc.scala
Author: Makarius
-Access to Isabelle documentation.
+Access to Isabelle examples and PDF documentation.
*/
package isabelle
@@ -11,14 +11,32 @@
object Doc {
- /* dirs */
+ /* entries */
+
+ case class Section(title: String, important: Boolean, entries: List[Entry])
+ case class Entry(name: String, path: Path, title: String = "") {
+ def view(): Unit = Doc.view(path)
+ override def toString: String = // GUI label
+ if (title.nonEmpty) {
+ "" + HTML.output(name) + ": " + HTML.output(title) + ""
+ }
+ else name
+ }
+
+ def plain_file(path: Path): Option[Entry] =
+ if (path.is_file && !path.is_pdf) {
+ val a = path.implode
+ val b = Library.try_unprefix("$ISABELLE_HOME/", a).getOrElse(a)
+ Some(Entry(b, path))
+ }
+ else None
+
+
+ /* contents */
def dirs(): List[Path] =
Path.split(Isabelle_System.getenv("ISABELLE_DOCS"))
-
- /* contents */
-
private def contents_lines(): List[(Path, String)] =
for {
dir <- dirs()
@@ -35,34 +53,18 @@
}
class Contents private(val sections: List[Section]) {
def ++ (other: Contents): Contents = new Contents(sections ::: other.sections)
- def entries: List[Entry] = sections.flatMap(_.entries)
- def docs: List[Doc] = entries.collect({ case doc: Doc => doc })
- }
-
- case class Section(title: String, important: Boolean, entries: List[Entry])
- sealed abstract class Entry {
- def name: String
- def path: Path
+ def entries(name: String => Boolean = _ => true, pdf: Boolean = false): List[Entry] =
+ sections.flatMap(s => s.entries.filter(e => name(e.name) && (!pdf || e.path.is_pdf)))
}
- case class Doc(name: String, title: String, path: Path) extends Entry
- case class Text_File(name: String, path: Path) extends Entry
-
- def text_file(path: Path): Option[Text_File] =
- if (path.is_file) {
- val a = path.implode
- val b = Library.try_unprefix("$ISABELLE_HOME/", a).getOrElse(a)
- Some(Text_File(b, path))
- }
- else None
def release_notes(): Contents =
Contents.section("Release Notes", true,
- Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file))
+ Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(plain_file))
def examples(): Contents =
Contents.section("Examples", true,
Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
- text_file(file) match {
+ plain_file(file) match {
case Some(entry) => entry
case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
}))
@@ -85,7 +87,7 @@
}
val Section_ = """^(\S.*)\s*$""".r
- val Doc_ = """^\s+(\S+)\s+(.+)\s*$""".r
+ val Entry_ = """^\s+(\S+)\s+(.+)\s*$""".r
for ((dir, line) <- contents_lines()) {
line match {
@@ -94,8 +96,9 @@
case None => begin(Section(text, false, Nil))
case Some(txt) => begin(Section(txt, true, Nil))
}
- case Doc_(name, title) =>
- entries += Doc(name, title, dir + Path.basic(name).pdf)
+ case Entry_(name, title) =>
+ val path = dir + Path.basic(name)
+ entries += Entry(name, if (path.is_file) path else path.pdf, title = title)
case _ =>
}
}
@@ -112,7 +115,7 @@
val here = Scala_Project.here
def apply(arg: String): String =
if (arg.nonEmpty) error("Bad argument: " + quote(arg))
- else cat_lines((for (doc <- contents().docs) yield doc.name).sorted)
+ else cat_lines((for (entry <- contents().entries(pdf = true)) yield entry.name).sorted)
}
@@ -133,15 +136,15 @@
val getopts = Getopts("""
Usage: isabelle doc [DOC ...]
- View Isabelle PDF documentation.
+ View Isabelle examples and PDF documentation.
""")
val docs = getopts(args)
if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
else {
docs.foreach(name =>
- contents().docs.find(_.name == name) match {
- case Some(doc) => view(doc.path)
+ contents().entries(name = docs.contains).headOption match {
+ case Some(entry) => entry.view()
case None => error("No Isabelle documentation entry: " + quote(name))
}
)
diff -r d026fa14433b -r c5a61c7e2725 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Tue Nov 05 23:27:47 2024 +0100
@@ -19,34 +19,22 @@
class Documentation_Dockable(view: View, position: String) extends Dockable(view, position) {
private val doc_contents = Doc.contents()
- private case class Node(string: String, entry: Doc.Entry) {
- override def toString: String = string
- }
-
private val tree = new Tree_View(single_selection_mode = true)
for (section <- doc_contents.sections) {
tree.root.add(Tree_View.Node(section.title))
- section.entries.foreach(
- {
- case entry @ Doc.Doc(name, title, _) =>
- val string = "" + HTML.output(name) + ": " + HTML.output(title) + ""
- tree.root.getLastChild.asInstanceOf[Tree_View.Node]
- .add(Tree_View.Node(Node(string, entry)))
- case entry @ Doc.Text_File(name: String, _) =>
- tree.root.getLastChild.asInstanceOf[Tree_View.Node]
- .add(Tree_View.Node(Node(name, entry)))
- })
+ for (entry <- section.entries) {
+ tree.root.getLastChild.asInstanceOf[Tree_View.Node].add(Tree_View.Node(entry))
+ }
}
override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
private def action(node: Tree_View.Node): Unit = {
- node.getUserObject match {
- case Node(_, Doc.Doc(_, _, path)) =>
- PIDE.editor.goto_doc(view, path)
- case Node(_, Doc.Text_File(_, path)) =>
- PIDE.editor.goto_file(true, view, File.platform_path(path))
+ node match {
+ case Tree_View.Node(entry: Doc.Entry) =>
+ if (entry.path.is_pdf) PIDE.editor.goto_doc(view, entry.path)
+ else PIDE.editor.goto_file(true, view, File.platform_path(entry.path))
case _ =>
}
}
diff -r d026fa14433b -r c5a61c7e2725 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 05 19:59:30 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 05 23:27:47 2024 +0100
@@ -186,13 +186,11 @@
/* hyperlinks */
def hyperlink_doc(name: String): Option[Hyperlink] =
- Doc.contents().entries.collectFirst(
- { case entry if entry.name == name =>
- new Hyperlink {
- override val external: Boolean = !entry.path.is_file
- def follow(view: View): Unit = goto_doc(view, entry.path)
- override def toString: String = "doc " + quote(name)
- }
+ Doc.contents().entries(name = _ == name).headOption.map(entry =>
+ new Hyperlink {
+ override val external: Boolean = !entry.path.is_file
+ def follow(view: View): Unit = goto_doc(view, entry.path)
+ override def toString: String = "doc " + quote(name)
})
def hyperlink_url(name: String): Hyperlink =