src/Tools/jEdit/src/jedit_editor.scala
changeset 64663 4c9fb4d4bca3
parent 64662 5a2c15faf89c
child 64664 951507563033
equal deleted inserted replaced
64662:5a2c15faf89c 64663:4c9fb4d4bca3
   222   def hyperlink_doc(name: String): Option[Hyperlink] =
   222   def hyperlink_doc(name: String): Option[Hyperlink] =
   223     Doc.contents().collectFirst({
   223     Doc.contents().collectFirst({
   224       case doc: Doc.Text_File if doc.name == name => doc.path
   224       case doc: Doc.Text_File if doc.name == name => doc.path
   225       case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
   225       case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
   226         new Hyperlink {
   226         new Hyperlink {
   227           val external = !path.is_file
   227           override val external = !path.is_file
   228           def follow(view: View): Unit = goto_doc(view, path)
   228           def follow(view: View): Unit = goto_doc(view, path)
   229           override def toString: String = "doc " + quote(name)
   229           override def toString: String = "doc " + quote(name)
   230         })
   230         })
   231 
   231 
   232   def hyperlink_url(name: String): Hyperlink =
   232   def hyperlink_url(name: String): Hyperlink =
   233     new Hyperlink {
   233     new Hyperlink {
   234       val external = true
   234       override val external = true
   235       def follow(view: View): Unit =
   235       def follow(view: View): Unit =
   236         Standard_Thread.fork("hyperlink_url") {
   236         Standard_Thread.fork("hyperlink_url") {
   237           try { Isabelle_System.open(Url.escape(name)) }
   237           try { Isabelle_System.open(Url.escape(name)) }
   238           catch {
   238           catch {
   239             case exn: Throwable =>
   239             case exn: Throwable =>
   245       override def toString: String = "URL " + quote(name)
   245       override def toString: String = "URL " + quote(name)
   246     }
   246     }
   247 
   247 
   248   def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
   248   def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
   249     new Hyperlink {
   249     new Hyperlink {
   250       val external = false
       
   251       def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
   250       def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
   252       override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
   251       override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
   253     }
   252     }
   254 
   253 
   255   def hyperlink_file(focus: Boolean, name: String): Hyperlink =
   254   def hyperlink_file(focus: Boolean, name: String): Hyperlink =
   256     hyperlink_file(focus, Line.Node_Position(name))
   255     hyperlink_file(focus, Line.Node_Position(name))
   257 
   256 
   258   def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
   257   def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
   259     new Hyperlink {
   258     new Hyperlink {
   260       val external = false
       
   261       def follow(view: View): Unit = goto_file(focus, view, pos)
   259       def follow(view: View): Unit = goto_file(focus, view, pos)
   262       override def toString: String = "file " + quote(pos.name)
   260       override def toString: String = "file " + quote(pos.name)
   263     }
   261     }
   264 
   262 
   265   def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
   263   def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)