src/Tools/jEdit/src/documentation_dockable.scala
changeset 52541 97c950217d7f
parent 52447 9a74000426e2
child 52542 19d674acb764
     1.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Sat Jul 06 21:50:14 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Jul 06 21:51:35 2013 +0200
     1.3 @@ -29,6 +29,11 @@
     1.4        "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
     1.5    }
     1.6  
     1.7 +  private case class Text_File(path: Path)
     1.8 +  {
     1.9 +    override def toString = path.base.implode
    1.10 +  }
    1.11 +
    1.12    private val root = new DefaultMutableTreeNode
    1.13    docs foreach {
    1.14      case Doc.Section(text) =>
    1.15 @@ -36,6 +41,13 @@
    1.16      case Doc.Doc(name, title) =>
    1.17        root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    1.18          .add(new DefaultMutableTreeNode(Documentation(name, title)))
    1.19 +    case Doc.Text_File(path: Path) =>
    1.20 +      root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
    1.21 +        .add(new DefaultMutableTreeNode(Text_File(path.expand)))
    1.22 +  }
    1.23 +
    1.24 +  private def documentation_error(exn: Throwable) {
    1.25 +    GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    1.26    }
    1.27  
    1.28    private val tree = new JTree(root)
    1.29 @@ -52,11 +64,10 @@
    1.30                case Documentation(name, _) =>
    1.31                  default_thread_pool.submit(() =>
    1.32                    try { Doc.view(name) }
    1.33 -                  catch {
    1.34 -                    case exn: Throwable =>
    1.35 -                      GUI.error_dialog(view,
    1.36 -                        "Documentation error", GUI.scrollable_text(Exn.message(exn)))
    1.37 -                  })
    1.38 +                  catch { case exn: Throwable => documentation_error(exn) })
    1.39 +              case Text_File(path) =>
    1.40 +                  try { Hyperlink(Isabelle_System.platform_path(path)).follow(view) }
    1.41 +                  catch { case exn: Throwable => documentation_error(exn) }
    1.42                case _ =>
    1.43              }
    1.44            case _ =>