misc tuning and clarification: Doc.Entry supports both plain files and pdf documents;
recover plain file support from 488c7e8923b2;
--- a/NEWS Mon Nov 04 22:36:42 2024 +0100
+++ b/NEWS Tue Nov 05 22:05:50 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.
--- a/src/Pure/Admin/build_doc.scala Mon Nov 04 22:36:42 2024 +0100
+++ b/src/Pure/Admin/build_doc.scala Tue Nov 05 22:05:50 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()
}
}
}
--- a/src/Pure/General/http.scala Mon Nov 04 22:36:42 2024 +0100
+++ b/src/Pure/General/http.scala Tue Nov 05 22:05:50 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)
--- a/src/Pure/Tools/doc.scala Mon Nov 04 22:36:42 2024 +0100
+++ b/src/Pure/Tools/doc.scala Tue Nov 05 22:05:50 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><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
+ }
+ 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))
}
)
--- a/src/Tools/jEdit/src/documentation_dockable.scala Mon Nov 04 22:36:42 2024 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Tue Nov 05 22:05:50 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><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
- 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 _ =>
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 04 22:36:42 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 05 22:05:50 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 =