clarified module name;
authorwenzelm
Tue Dec 20 22:32:04 2016 +0100 (2016-12-20)
changeset 6462383f012ce2567
parent 64622 529bbb8977c7
child 64625 c6330e16743f
child 64639 bad5de3f9554
clarified module name;
src/Pure/build-jars
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/uri_resources.scala
src/Tools/VSCode/src/vscode_resources.scala
     1.1 --- a/src/Pure/build-jars	Tue Dec 20 22:24:16 2016 +0100
     1.2 +++ b/src/Pure/build-jars	Tue Dec 20 22:32:04 2016 +0100
     1.3 @@ -162,8 +162,8 @@
     1.4    ../Tools/VSCode/src/document_model.scala
     1.5    ../Tools/VSCode/src/protocol.scala
     1.6    ../Tools/VSCode/src/server.scala
     1.7 -  ../Tools/VSCode/src/uri_resources.scala
     1.8    ../Tools/VSCode/src/vscode_rendering.scala
     1.9 +  ../Tools/VSCode/src/vscode_resources.scala
    1.10  )
    1.11  
    1.12  
     2.1 --- a/src/Tools/VSCode/src/server.scala	Tue Dec 20 22:24:16 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Dec 20 22:32:04 2016 +0100
     2.3 @@ -96,7 +96,7 @@
     2.4    private val state = Synchronized(Server.State())
     2.5  
     2.6    def session: Session = state.value.session getOrElse error("Session inactive")
     2.7 -  def resources: URI_Resources = session.resources.asInstanceOf[URI_Resources]
     2.8 +  def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
     2.9  
    2.10  
    2.11    /* init and exit */
    2.12 @@ -105,7 +105,7 @@
    2.13    {
    2.14      val content = Build.session_content(options, false, session_dirs, session_name)
    2.15      val resources =
    2.16 -      new URI_Resources(content.loaded_theories, content.known_theories, content.syntax)
    2.17 +      new VSCode_Resources(content.loaded_theories, content.known_theories, content.syntax)
    2.18  
    2.19      val session =
    2.20        new Session(resources) {
     3.1 --- a/src/Tools/VSCode/src/uri_resources.scala	Tue Dec 20 22:24:16 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,43 +0,0 @@
     3.4 -/*  Title:      Tools/VSCode/src/uri_resources.scala
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Resources based on file-system URIs.
     3.8 -*/
     3.9 -
    3.10 -package isabelle.vscode
    3.11 -
    3.12 -
    3.13 -import isabelle._
    3.14 -
    3.15 -import java.net.{URI, URISyntaxException}
    3.16 -import java.io.{File => JFile}
    3.17 -
    3.18 -
    3.19 -object URI_Resources
    3.20 -{
    3.21 -  def is_wellformed(uri: String): Boolean =
    3.22 -    try { new JFile(new URI(uri)); true }
    3.23 -    catch { case _: URISyntaxException | _: IllegalArgumentException => false }
    3.24 -
    3.25 -  def canonical_file(uri: String): JFile =
    3.26 -    new JFile(new URI(uri)).getCanonicalFile
    3.27 -
    3.28 -  val empty: URI_Resources =
    3.29 -    new URI_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
    3.30 -}
    3.31 -
    3.32 -class URI_Resources(
    3.33 -    loaded_theories: Set[String],
    3.34 -    known_theories: Map[String, Document.Node.Name],
    3.35 -    base_syntax: Outer_Syntax)
    3.36 -  extends Resources(loaded_theories, known_theories, base_syntax)
    3.37 -{
    3.38 -  def node_name(uri: String): Document.Node.Name =
    3.39 -  {
    3.40 -    val file = URI_Resources.canonical_file(uri)  // FIXME wellformed!?
    3.41 -    val node = file.getPath
    3.42 -    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
    3.43 -    val master_dir = if (theory == "") "" else file.getParent
    3.44 -    Document.Node.Name(node, master_dir, theory)
    3.45 -  }
    3.46 -}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Dec 20 22:32:04 2016 +0100
     4.3 @@ -0,0 +1,43 @@
     4.4 +/*  Title:      Tools/VSCode/src/vscode_resources.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Resources for VSCode Language Server, based on file-system URIs.
     4.8 +*/
     4.9 +
    4.10 +package isabelle.vscode
    4.11 +
    4.12 +
    4.13 +import isabelle._
    4.14 +
    4.15 +import java.net.{URI, URISyntaxException}
    4.16 +import java.io.{File => JFile}
    4.17 +
    4.18 +
    4.19 +object VSCode_Resources
    4.20 +{
    4.21 +  def is_wellformed(uri: String): Boolean =
    4.22 +    try { new JFile(new URI(uri)); true }
    4.23 +    catch { case _: URISyntaxException | _: IllegalArgumentException => false }
    4.24 +
    4.25 +  def canonical_file(uri: String): JFile =
    4.26 +    new JFile(new URI(uri)).getCanonicalFile
    4.27 +
    4.28 +  val empty: VSCode_Resources =
    4.29 +    new VSCode_Resources(Set.empty, Map.empty, Outer_Syntax.empty)
    4.30 +}
    4.31 +
    4.32 +class VSCode_Resources(
    4.33 +    loaded_theories: Set[String],
    4.34 +    known_theories: Map[String, Document.Node.Name],
    4.35 +    base_syntax: Outer_Syntax)
    4.36 +  extends Resources(loaded_theories, known_theories, base_syntax)
    4.37 +{
    4.38 +  def node_name(uri: String): Document.Node.Name =
    4.39 +  {
    4.40 +    val file = VSCode_Resources.canonical_file(uri)  // FIXME wellformed!?
    4.41 +    val node = file.getPath
    4.42 +    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
    4.43 +    val master_dir = if (theory == "") "" else file.getParent
    4.44 +    Document.Node.Name(node, master_dir, theory)
    4.45 +  }
    4.46 +}