src/Tools/VSCode/src/uri_resources.scala
author wenzelm
Tue Dec 20 22:24:16 2016 +0100 (2016-12-20)
changeset 64622 529bbb8977c7
parent 64605 9c1173a7e4cb
permissions -rw-r--r--
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm@64605
     1
/*  Title:      Tools/VSCode/src/uri_resources.scala
wenzelm@64605
     2
    Author:     Makarius
wenzelm@64605
     3
wenzelm@64605
     4
Resources based on file-system URIs.
wenzelm@64605
     5
*/
wenzelm@64605
     6
wenzelm@64605
     7
package isabelle.vscode
wenzelm@64605
     8
wenzelm@64605
     9
wenzelm@64605
    10
import isabelle._
wenzelm@64605
    11
wenzelm@64605
    12
import java.net.{URI, URISyntaxException}
wenzelm@64605
    13
import java.io.{File => JFile}
wenzelm@64605
    14
wenzelm@64605
    15
wenzelm@64605
    16
object URI_Resources
wenzelm@64605
    17
{
wenzelm@64605
    18
  def is_wellformed(uri: String): Boolean =
wenzelm@64605
    19
    try { new JFile(new URI(uri)); true }
wenzelm@64605
    20
    catch { case _: URISyntaxException | _: IllegalArgumentException => false }
wenzelm@64605
    21
wenzelm@64605
    22
  def canonical_file(uri: String): JFile =
wenzelm@64605
    23
    new JFile(new URI(uri)).getCanonicalFile
wenzelm@64605
    24
wenzelm@64605
    25
  val empty: URI_Resources =
wenzelm@64605
    26
    new URI_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
wenzelm@64605
    27
}
wenzelm@64605
    28
wenzelm@64605
    29
class URI_Resources(
wenzelm@64605
    30
    loaded_theories: Set[String],
wenzelm@64605
    31
    known_theories: Map[String, Document.Node.Name],
wenzelm@64605
    32
    base_syntax: Outer_Syntax)
wenzelm@64605
    33
  extends Resources(loaded_theories, known_theories, base_syntax)
wenzelm@64605
    34
{
wenzelm@64605
    35
  def node_name(uri: String): Document.Node.Name =
wenzelm@64605
    36
  {
wenzelm@64605
    37
    val file = URI_Resources.canonical_file(uri)  // FIXME wellformed!?
wenzelm@64605
    38
    val node = file.getPath
wenzelm@64605
    39
    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
wenzelm@64605
    40
    val master_dir = if (theory == "") "" else file.getParent
wenzelm@64605
    41
    Document.Node.Name(node, master_dir, theory)
wenzelm@64605
    42
  }
wenzelm@64605
    43
}