# HG changeset patch # User wenzelm # Date 1730840750 -3600 # Node ID 1818358373e2b0fe0a0d5c8e64e75648e43f66f8 # Parent 31f9e5ada55054e2f0577f3d942d2af1d1a2d7c8 misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; recover plain file support from 488c7e8923b2; diff -r 31f9e5ada550 -r 1818358373e2 NEWS --- 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. diff -r 31f9e5ada550 -r 1818358373e2 src/Pure/Admin/build_doc.scala --- 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() } } } diff -r 31f9e5ada550 -r 1818358373e2 src/Pure/General/http.scala --- 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) diff -r 31f9e5ada550 -r 1818358373e2 src/Pure/Tools/doc.scala --- 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.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 31f9e5ada550 -r 1818358373e2 src/Tools/jEdit/src/documentation_dockable.scala --- 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.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 31f9e5ada550 -r 1818358373e2 src/Tools/jEdit/src/jedit_editor.scala --- 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 =