# HG changeset patch # User wenzelm # Date 1645474505 -3600 # Node ID 488c7e8923b29fdd4ba3b418e0886ddce2d31015 # Parent 7bf685cbc7899dcc925ee7de39e8a9acbd9cbc6c clarified pdf path; diff -r 7bf685cbc789 -r 488c7e8923b2 src/Pure/General/http.scala --- 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) diff -r 7bf685cbc789 -r 488c7e8923b2 src/Pure/Tools/doc.scala --- 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) } diff -r 7bf685cbc789 -r 488c7e8923b2 src/Tools/jEdit/src/documentation_dockable.scala --- 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.output(name) + ": " + HTML.output(title) + "" - } - - 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.output(name) + ": " + HTML.output(title) + "" 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 _ => } } diff -r 7bf685cbc789 -r 488c7e8923b2 src/Tools/jEdit/src/jedit_editor.scala --- 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)) }