diff --git a/src/Pure/General/http.scala b/src/Pure/General/http.scala
--- a/src/Pure/General/http.scala
+++ b/src/Pure/General/http.scala
@@ -1,370 +1,370 @@
/* Title: Pure/General/http.scala
Author: Makarius
HTTP client and server support.
*/
package isabelle
import java.io.{File => JFile}
import java.nio.file.Files
import java.net.{InetSocketAddress, URI, URL, HttpURLConnection}
import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
object HTTP
{
/** content **/
object Content
{
val mime_type_bytes: String = "application/octet-stream"
val mime_type_text: String = "text/plain; charset=utf-8"
val mime_type_html: String = "text/html; charset=utf-8"
val default_mime_type: String = mime_type_bytes
val default_encoding: String = UTF8.charset_name
def apply(
bytes: Bytes,
file_name: String = "",
mime_type: String = default_mime_type,
encoding: String = default_encoding,
elapsed_time: Time = Time.zero): Content =
new Content(bytes, file_name, mime_type, encoding, elapsed_time)
def read(file: JFile): Content =
{
val bytes = Bytes.read(file)
val file_name = file.getName
val mime_type = Option(Files.probeContentType(file.toPath)).getOrElse(default_mime_type)
apply(bytes, file_name = file_name, mime_type = mime_type)
}
def read(path: Path): Content = read(path.file)
}
class Content private(
val bytes: Bytes,
val file_name: String,
val mime_type: String,
val encoding: String,
val elapsed_time: Time)
{
def text: String = new String(bytes.array, encoding)
def json: JSON.T = JSON.parse(text)
}
/** client **/
val NEWLINE: String = "\r\n"
object Client
{
val default_timeout: Time = Time.seconds(180)
def open_connection(url: URL,
timeout: Time = default_timeout,
user_agent: String = ""): HttpURLConnection =
{
url.openConnection match {
case connection: HttpURLConnection =>
if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) {
val ms = timeout.ms.toInt
connection.setConnectTimeout(ms)
connection.setReadTimeout(ms)
}
proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
connection
case _ => error("Bad URL (not HTTP): " + quote(url.toString))
}
}
def get_content(connection: HttpURLConnection): Content =
{
val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r
val start = Time.now()
using(connection.getInputStream)(stream =>
{
val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
val stop = Time.now()
val file_name = Url.file_name(connection.getURL)
val mime_type = Option(connection.getContentType).getOrElse(Content.default_mime_type)
val encoding =
(connection.getContentEncoding, mime_type) match {
case (enc, _) if enc != null => enc
case (_, Charset(enc)) => enc
case _ => Content.default_encoding
}
Content(bytes, file_name = file_name, mime_type = mime_type,
encoding = encoding, elapsed_time = stop - start)
})
}
def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
get_content(open_connection(url, timeout = timeout, user_agent = user_agent))
def post(url: URL, parameters: List[(String, Any)],
timeout: Time = default_timeout,
user_agent: String = ""): Content =
{
val connection = open_connection(url, timeout = timeout, user_agent = user_agent)
connection.setRequestMethod("POST")
connection.setDoOutput(true)
val boundary = UUID.random().toString
connection.setRequestProperty(
"Content-Type", "multipart/form-data; boundary=" + quote(boundary))
using(connection.getOutputStream)(out =>
{
def output(s: String): Unit = out.write(UTF8.bytes(s))
def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE))
def output_boundary(end: Boolean = false): Unit =
output("--" + boundary + (if (end) "--" else "") + NEWLINE)
def output_name(name: String): Unit =
output("Content-Disposition: form-data; name=" + quote(name))
def output_value(value: Any): Unit =
{
output_newline(2)
output(value.toString)
}
def output_content(content: Content): Unit =
{
proper_string(content.file_name).foreach(s => output("; filename=" + quote(s)))
output_newline()
proper_string(content.mime_type).foreach(s => output("Content-Type: " + s))
output_newline(2)
content.bytes.write_stream(out)
}
output_newline(2)
for { (name, value) <- parameters } {
output_boundary()
output_name(name)
value match {
case content: Content => output_content(content)
case file: JFile => output_content(Content.read(file))
case path: Path => output_content(Content.read(path))
case _ => output_value(value)
}
output_newline()
}
output_boundary(end = true)
out.flush()
})
get_content(connection)
}
}
/** server **/
/* request */
def url_path(names: String*): String =
names.iterator.flatMap(a => if (a.isEmpty) None else Some("/" + a)).mkString
class Request private[HTTP](
val server: String,
val service: String,
val uri: URI,
val input: Bytes)
{
def home: String = url_path(server, service)
def root: String = home + "/"
def query: String = home + "?"
def toplevel: Boolean = uri_name == home || uri_name == root
val uri_name: String = uri.toString
def uri_path: Option[Path] =
for {
s <- Option(uri.getPath).flatMap(Library.try_unprefix(root, _))
if Path.is_wellformed(s)
p = Path.explode(s) if p.all_basic
} yield p
def decode_query: Option[String] =
Library.try_unprefix(query, uri_name).map(Url.decode)
def decode_properties: Properties.T =
space_explode('&', input.text).map(
{
case Properties.Eq(a, b) => Url.decode(a) -> Url.decode(b)
case s => error("Malformed key-value pair in HTTP/POST: " + quote(s))
})
}
/* response */
object Response
{
def apply(
bytes: Bytes = Bytes.empty,
content_type: String = Content.mime_type_bytes): Response =
new Response(bytes, content_type)
val empty: Response = apply()
def text(s: String): Response = apply(Bytes(s), Content.mime_type_text)
def html(s: String): Response = apply(Bytes(s), Content.mime_type_html)
def content(content: Content): Response = apply(content.bytes, content.mime_type)
def read(file: JFile): Response = content(Content.read(file))
def read(path: Path): Response = content(Content.read(path))
}
class Response private[HTTP](val output: Bytes, val content_type: String)
{
override def toString: String = output.toString
def write(http: HttpExchange, code: Int): Unit =
{
http.getResponseHeaders.set("Content-Type", content_type)
http.sendResponseHeaders(code, output.length.toLong)
using(http.getResponseBody)(output.write_stream)
}
}
/* service */
abstract class Service(val service: String, method: String = "GET")
{
override def toString: String = service
def apply(request: Request): Option[Response]
def context(server: String): String = proper_string(url_path(server, service)).getOrElse("/")
def handler(server: String): HttpHandler = (http: HttpExchange) => {
val uri = http.getRequestURI
val input = using(http.getRequestBody)(Bytes.read_stream(_))
if (http.getRequestMethod == method) {
val request = new Request(server, service, uri, input)
Exn.capture(apply(request)) match {
case Exn.Res(Some(response)) =>
response.write(http, 200)
case Exn.Res(None) =>
Response.empty.write(http, 404)
case Exn.Exn(ERROR(msg)) =>
Response.text(Output.error_message_text(msg)).write(http, 500)
case Exn.Exn(exn) => throw exn
}
}
else Response.empty.write(http, 400)
}
}
/* server */
class Server private[HTTP](val name: String, val http_server: HttpServer)
{
def += (service: Service): Unit =
http_server.createContext(service.context(name), service.handler(name))
def -= (service: Service): Unit =
http_server.removeContext(service.context(name))
def start(): Unit = http_server.start()
def stop(): Unit = http_server.stop(0)
def address: InetSocketAddress = http_server.getAddress
def url: String = "http://" + address.getHostName + ":" + address.getPort + url_path(name)
override def toString: String = url
}
def server(
name: String = UUID.random().toString,
services: List[Service] = isabelle_services): Server =
{
val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
http_server.setExecutor(null)
val server = new Server(name, http_server)
for (service <- services) server += service
server
}
/** Isabelle services **/
def isabelle_services: List[Service] =
List(new Welcome(), new Fonts(), new PDFjs(), new Docs())
/* welcome */
class Welcome(name: String = "") extends Service(name)
{
def apply(request: Request): Option[Response] =
if (request.toplevel) {
Some(Response.text("Welcome to " + Isabelle_System.identification()))
}
else None
}
/* fonts */
class Fonts(name: String = "fonts") extends Service(name)
{
private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
Isabelle_Fonts.fonts(hidden = true)
def apply(request: Request): Option[Response] =
if (request.toplevel) {
Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
}
else {
request.uri_path.flatMap(path =>
html_fonts.collectFirst(
{ case entry if path == entry.path.base => Response(entry.bytes) }
))
}
}
/* pdfjs */
class PDFjs(name: String = "pdfjs") extends Service(name)
{
def apply(request: Request): Option[Response] =
for {
p <- request.uri_path
path = Path.explode("$ISABELLE_PDFJS_HOME") + p if path.is_file
s = p.implode if s.startsWith("build/") || s.startsWith("web/")
} yield Response.read(path)
}
/* docs */
class Docs(name: String = "docs") extends PDFjs(name)
{
private val doc_contents = isabelle.Doc.main_contents()
def doc_request(request: Request): Option[Response] =
for {
p <- request.uri_path if p.is_pdf
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 --git a/src/Pure/Tools/doc.scala b/src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala
+++ b/src/Pure/Tools/doc.scala
@@ -1,162 +1,159 @@
/* Title: Pure/Tools/doc.scala
Author: Makarius
Access to Isabelle documentation.
*/
package isabelle
import scala.collection.mutable
object Doc
{
/* dirs */
def dirs(): List[Path] =
Path.split(Isabelle_System.getenv("ISABELLE_DOCS"))
/* contents */
private def contents_lines(): List[(Path, String)] =
for {
dir <- dirs()
catalog = dir + Path.basic("Contents")
if catalog.is_file
line <- Library.trim_split_lines(File.read(catalog))
} yield (dir, line)
object Contents
{
def apply(sections: List[Section]): Contents = new Contents(sections)
def section(title: String, important: Boolean, entries: List[Entry]): Contents =
apply(List(Section(title, important, entries)))
}
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
}
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))
def examples(): Contents =
Contents.section("Examples", true,
Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
text_file(file) match {
case Some(entry) => entry
case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
}))
def main_contents(): Contents =
{
val result = new mutable.ListBuffer[Section]
val entries = new mutable.ListBuffer[Entry]
var section: Option[Section] = None
def flush(): Unit =
if (section.nonEmpty) {
result += section.get.copy(entries = entries.toList)
entries.clear()
section = None
}
def begin(s: Section): Unit =
{
flush()
section = Some(s)
}
val Section_ = """^(\S.*)\s*$""".r
val Doc_ = """^\s+(\S+)\s+(.+)\s*$""".r
for ((dir, line) <- contents_lines()) {
line match {
case Section_(text) =>
Library.try_unsuffix("!", text) match {
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))
+ entries += Doc(name, title, dir + Path.basic(name).pdf)
case _ =>
}
}
flush()
Contents(result.toList)
}
def contents(): Contents =
{
examples() ++ release_notes() ++ main_contents()
}
object Doc_Names extends Scala.Fun_String("doc_names")
{
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)
}
/* view */
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)
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("doc", "view Isabelle PDF documentation",
Scala_Project.here, args =>
{
val getopts = Getopts("""
Usage: isabelle doc [DOC ...]
View Isabelle 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)
case None => error("No Isabelle documentation entry: " + quote(name))
}
)
}
})
}
diff --git a/src/Tools/jEdit/src/documentation_dockable.scala b/src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala
+++ b/src/Tools/jEdit/src/documentation_dockable.scala
@@ -1,117 +1,112 @@
/* Title: Tools/jEdit/src/documentation_dockable.scala
Author: Makarius
Dockable window for Isabelle documentation.
*/
package isabelle.jedit
import isabelle._
import java.awt.Dimension
import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
import javax.swing.{JTree, JScrollPane}
import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel}
import org.gjt.sp.jedit.{View, OperatingSystem}
class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
{
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
for (section <- doc_contents.sections) {
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)))
})
}
private val tree = new JTree(root)
tree.setRowHeight(0)
tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
override def focusOnDefaultComponent(): Unit = tree.requestFocusInWindow
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 _ =>
}
}
tree.addKeyListener(new KeyAdapter {
override def keyPressed(e: KeyEvent): Unit =
{
if (e.getKeyCode == KeyEvent.VK_ENTER) {
e.consume
val path = tree.getSelectionPath
if (path != null) {
path.getLastPathComponent match {
case node: DefaultMutableTreeNode => action(node)
case _ =>
}
}
}
}
})
tree.addMouseListener(new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit =
{
val click = tree.getPathForLocation(e.getX, e.getY)
if (click != null && e.getClickCount == 1) {
(click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
action(node)
case _ =>
}
}
}
})
{
var expand = true
var visible = 0
var row = 0
def make_visible(): Unit = { visible += 1; tree.expandRow(row) }
for (section <- doc_contents.sections) {
expand = section.important
make_visible()
row += 1
for (_ <- section.entries) {
if (expand) make_visible()
row += 1
}
}
tree.setRootVisible(false)
tree.setVisibleRowCount(visible)
}
private val tree_view = new JScrollPane(tree)
tree_view.setMinimumSize(new Dimension(200, 50))
set_content(tree_view)
}
diff --git a/src/Tools/jEdit/src/jedit_editor.scala b/src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala
+++ b/src/Tools/jEdit/src/jedit_editor.scala
@@ -1,322 +1,310 @@
/* Title: Tools/jEdit/src/jedit_editor.scala
Author: Makarius
PIDE editor operations for jEdit.
*/
package isabelle.jedit
import isabelle._
import java.io.{File => JFile}
import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.browser.VFSBrowser
import org.gjt.sp.jedit.io.{VFSManager, VFSFile}
class JEdit_Editor extends Editor[View]
{
/* session */
override def session: Session = PIDE.session
def flush_edits(hidden: Boolean = false, purge: Boolean = false): Unit =
GUI_Thread.require {
val (doc_blobs, edits) = Document_Model.flush_edits(hidden, purge)
session.update(doc_blobs, edits)
}
override def flush(): Unit = flush_edits()
def purge(): Unit = flush_edits(purge = true)
private val delay1_flush =
Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
private val delay2_flush =
Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() }
def invoke(): Unit = delay1_flush.invoke()
def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
def shutdown(): Unit =
GUI_Thread.require {
delay1_flush.revoke()
delay2_flush.revoke()
Document_Model.flush_edits(hidden = false, purge = false)
}
def visible_node(name: Document.Node.Name): Boolean =
(for {
text_area <- JEdit_Lib.jedit_text_areas()
doc_view <- Document_View.get(text_area)
} yield doc_view.model.node_name).contains(name)
/* current situation */
override def current_node(view: View): Option[Document.Node.Name] =
GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
override def current_node_snapshot(view: View): Option[Document.Snapshot] =
GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
{
GUI_Thread.require {}
Document_Model.get(name) match {
case Some(model) => model.snapshot()
case None => session.snapshot(name)
}
}
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
{
GUI_Thread.require {}
val text_area = view.getTextArea
val buffer = view.getBuffer
Document_View.get(text_area) match {
case Some(doc_view) if doc_view.model.is_theory =>
snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
case _ =>
Document_Model.get(buffer) match {
case Some(model) if !model.is_theory =>
snapshot.version.nodes.commands_loading(model.node_name).headOption
case _ => None
}
}
}
/* overlays */
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
Document_Model.node_overlays(name)
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
Document_Model.insert_overlay(command, fn, args)
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
Document_Model.remove_overlay(command, fn, args)
/* navigation */
def push_position(view: View): Unit =
{
val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
if (navigator != null) {
try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
catch { case _: NoSuchMethodException => }
}
}
def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit =
{
GUI_Thread.require {}
push_position(view)
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
try { view.getTextArea.moveCaretPosition(offset) }
catch {
case _: ArrayIndexOutOfBoundsException =>
case _: IllegalArgumentException =>
}
}
def goto_file(focus: Boolean, view: View, name: String): Unit =
goto_file(focus, view, Line.Node_Position.offside(name))
def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit =
{
GUI_Thread.require {}
push_position(view)
val name = pos.name
val line = pos.line
val column = pos.column
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
val text_area = view.getTextArea
try {
val line_start = text_area.getBuffer.getLineStartOffset(line)
text_area.moveCaretPosition(line_start)
if (column > 0) text_area.moveCaretPosition(line_start + column)
}
catch {
case _: ArrayIndexOutOfBoundsException =>
case _: IllegalArgumentException =>
}
case None =>
val is_dir =
try {
val vfs = VFSManager.getVFSForPath(name)
val vfs_file = vfs._getFile((), name, view)
vfs_file != null && vfs_file.getType == VFSFile.DIRECTORY
}
catch { case ERROR(_) => false }
if (is_dir) VFSBrowser.browseDirectory(view, name)
else if (!Isabelle_System.open_external_file(name)) {
val args =
if (line <= 0) Array(name)
else if (column <= 0) Array(name, "+line:" + (line + 1))
else Array(name, "+line:" + (line + 1) + "," + (column + 1))
jEdit.openFiles(view, null, args)
}
}
}
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))
}
/* 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)
}
})
def hyperlink_url(name: String): Hyperlink =
new Hyperlink {
override val external = true
def follow(view: View): Unit =
Isabelle_Thread.fork(name = "hyperlink_url") {
try { Isabelle_System.open(Url.escape_name(name)) }
catch {
case exn: Throwable =>
GUI_Thread.later {
GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
}
}
}
override def toString: String = "URL " + quote(name)
}
def hyperlink_file(focus: Boolean, name: String): Hyperlink =
hyperlink_file(focus, Line.Node_Position.offside(name))
def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
new Hyperlink {
def follow(view: View): Unit = goto_file(focus, view, pos)
override def toString: String = "file " + quote(pos.name)
}
def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink =
model match {
case file_model: File_Model =>
val pos =
try { file_model.node_position(offset) }
catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) }
hyperlink_file(focus, pos)
case buffer_model: Buffer_Model =>
new Hyperlink {
def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset)
override def toString: String = "buffer " + quote(model.node_name.node)
}
}
def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
: Option[Hyperlink] =
{
for (name <- PIDE.resources.source_file(source_name)) yield {
def hyperlink(pos: Line.Position) =
hyperlink_file(focus, Line.Node_Position(name, pos))
if (offset > 0) {
PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match {
case Some(text) =>
hyperlink(
Symbol.iterator(text).zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1).
foldLeft(Line.Position.zero)(_.advance(_)))
case None =>
hyperlink(Line.Position((line1 - 1) max 0))
}
}
else hyperlink(Line.Position((line1 - 1) max 0))
}
}
override def hyperlink_command(
focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
: Option[Hyperlink] =
{
if (snapshot.is_outdated) None
else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
}
def is_hyperlink_position(snapshot: Document.Snapshot,
text_offset: Text.Offset, pos: Position.T): Boolean =
{
pos match {
case Position.Item_Id(id, range) if range.start > 0 =>
snapshot.find_command(id) match {
case Some((node, command)) if snapshot.get_node(command.node_name) eq node =>
node.command_start(command) match {
case Some(start) => text_offset == start + command.chunk.decode(range.start)
case None => false
}
case _ => false
}
case _ => false
}
}
def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
: Option[Hyperlink] =
pos match {
case Position.Item_File(name, line, range) =>
hyperlink_source_file(focus, name, line, range.start)
case Position.Item_Id(id, range) =>
hyperlink_command(focus, snapshot, id, range.start)
case _ => None
}
def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
: Option[Hyperlink] =
pos match {
case Position.Item_Def_File(name, line, range) =>
hyperlink_source_file(focus, name, line, range.start)
case Position.Item_Def_Id(id, range) =>
hyperlink_command(focus, snapshot, id, range.start)
case _ => None
}
/* dispatcher thread */
override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body)
override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body)
override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body)
override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body)
}