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