--- a/src/Pure/General/http.scala Mon Feb 21 20:50:01 2022 +0100
+++ b/src/Pure/General/http.scala Mon Feb 21 21:15:05 2022 +0100
@@ -362,7 +362,7 @@
s = p.implode if s.startsWith("pdf/")
name = p.base.split_ext._1.implode
doc <- doc_contents.docs.find(_.name == name)
- } yield Response.read(doc.path.pdf)
+ } yield Response.read(doc.path)
override def apply(request: Request): Option[Response] =
doc_request(request) orElse super.apply(request)
--- a/src/Pure/Tools/doc.scala Mon Feb 21 20:50:01 2022 +0100
+++ b/src/Pure/Tools/doc.scala Mon Feb 21 21:15:05 2022 +0100
@@ -101,7 +101,7 @@
case Some(txt) => begin(Section(txt, true, Nil))
}
case Doc_(name, title) =>
- entries += Doc(name, title, dir + Path.basic(name))
+ entries += Doc(name, title, dir + Path.basic(name).pdf)
case _ =>
}
}
@@ -128,12 +128,9 @@
def view(path: Path): Unit =
{
- if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true)
- else {
- val pdf = path.ext("pdf")
- if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
- else error("Bad Isabelle documentation file: " + pdf)
- }
+ if (!path.is_file) error("Bad Isabelle documentation file: " + path)
+ else if (path.is_pdf) Isabelle_System.pdf_viewer(path)
+ else Output.writeln(Library.trim_line(File.read(path)), stdout = true)
}
--- a/src/Tools/jEdit/src/documentation_dockable.scala Mon Feb 21 20:50:01 2022 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Mon Feb 21 21:15:05 2022 +0100
@@ -21,15 +21,9 @@
{
private val doc_contents = Doc.contents()
- private case class Documentation(name: String, title: String, path: Path)
+ private case class Node(string: String, entry: Doc.Entry)
{
- override def toString: String =
- "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
- }
-
- private case class Text_File(name: String, path: Path)
- {
- override def toString: String = name
+ override def toString: String = string
}
private val root = new DefaultMutableTreeNode
@@ -37,12 +31,13 @@
root.add(new DefaultMutableTreeNode(section.title))
section.entries.foreach(
{
- case Doc.Doc(name, title, path) =>
+ case entry @ Doc.Doc(name, title, _) =>
+ val string = "<html><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>"
root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
- .add(new DefaultMutableTreeNode(Documentation(name, title, path)))
- case Doc.Text_File(name: String, path: Path) =>
+ .add(new DefaultMutableTreeNode(Node(string, entry)))
+ case entry @ Doc.Text_File(name: String, _) =>
root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
- .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
+ .add(new DefaultMutableTreeNode(Node(name, entry)))
})
}
@@ -55,10 +50,10 @@
private def action(node: DefaultMutableTreeNode): Unit =
{
node.getUserObject match {
- case Text_File(_, path) =>
+ 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))
- case Documentation(_, _, path) =>
- PIDE.editor.goto_doc(view, path)
case _ =>
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Feb 21 20:50:01 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Feb 21 21:15:05 2022 +0100
@@ -178,20 +178,8 @@
def goto_doc(view: View, path: Path): Unit =
{
- if (path.is_file)
- goto_file(true, view, File.platform_path(path))
- else {
- Isabelle_Thread.fork(name = "documentation") {
- try { Doc.view(path) }
- catch {
- case exn: Throwable =>
- GUI_Thread.later {
- GUI.error_dialog(view,
- "Documentation error", GUI.scrollable_text(Exn.message(exn)))
- }
- }
- }
- }
+ if (path.is_pdf) Doc.view(path)
+ else goto_file(true, view, File.platform_path(path))
}