# HG changeset patch # User wenzelm # Date 1482269524 -3600 # Node ID 83f012ce256791a0ee559db4989d1a4701dbc0a4 # Parent 529bbb8977c700d00419936103b969fdedb908f1 clarified module name; diff -r 529bbb8977c7 -r 83f012ce2567 src/Pure/build-jars --- a/src/Pure/build-jars Tue Dec 20 22:24:16 2016 +0100 +++ b/src/Pure/build-jars Tue Dec 20 22:32:04 2016 +0100 @@ -162,8 +162,8 @@ ../Tools/VSCode/src/document_model.scala ../Tools/VSCode/src/protocol.scala ../Tools/VSCode/src/server.scala - ../Tools/VSCode/src/uri_resources.scala ../Tools/VSCode/src/vscode_rendering.scala + ../Tools/VSCode/src/vscode_resources.scala ) diff -r 529bbb8977c7 -r 83f012ce2567 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Tue Dec 20 22:24:16 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Tue Dec 20 22:32:04 2016 +0100 @@ -96,7 +96,7 @@ private val state = Synchronized(Server.State()) def session: Session = state.value.session getOrElse error("Session inactive") - def resources: URI_Resources = session.resources.asInstanceOf[URI_Resources] + def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] /* init and exit */ @@ -105,7 +105,7 @@ { val content = Build.session_content(options, false, session_dirs, session_name) val resources = - new URI_Resources(content.loaded_theories, content.known_theories, content.syntax) + new VSCode_Resources(content.loaded_theories, content.known_theories, content.syntax) val session = new Session(resources) { diff -r 529bbb8977c7 -r 83f012ce2567 src/Tools/VSCode/src/uri_resources.scala --- a/src/Tools/VSCode/src/uri_resources.scala Tue Dec 20 22:24:16 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,43 +0,0 @@ -/* Title: Tools/VSCode/src/uri_resources.scala - Author: Makarius - -Resources based on file-system URIs. -*/ - -package isabelle.vscode - - -import isabelle._ - -import java.net.{URI, URISyntaxException} -import java.io.{File => JFile} - - -object URI_Resources -{ - def is_wellformed(uri: String): Boolean = - try { new JFile(new URI(uri)); true } - catch { case _: URISyntaxException | _: IllegalArgumentException => false } - - def canonical_file(uri: String): JFile = - new JFile(new URI(uri)).getCanonicalFile - - val empty: URI_Resources = - new URI_Resources(Set.empty, Map.empty, Outer_Syntax.empty) -} - -class URI_Resources( - loaded_theories: Set[String], - known_theories: Map[String, Document.Node.Name], - base_syntax: Outer_Syntax) - extends Resources(loaded_theories, known_theories, base_syntax) -{ - def node_name(uri: String): Document.Node.Name = - { - val file = URI_Resources.canonical_file(uri) // FIXME wellformed!? - val node = file.getPath - val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("") - val master_dir = if (theory == "") "" else file.getParent - Document.Node.Name(node, master_dir, theory) - } -} diff -r 529bbb8977c7 -r 83f012ce2567 src/Tools/VSCode/src/vscode_resources.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Dec 20 22:32:04 2016 +0100 @@ -0,0 +1,43 @@ +/* Title: Tools/VSCode/src/vscode_resources.scala + Author: Makarius + +Resources for VSCode Language Server, based on file-system URIs. +*/ + +package isabelle.vscode + + +import isabelle._ + +import java.net.{URI, URISyntaxException} +import java.io.{File => JFile} + + +object VSCode_Resources +{ + def is_wellformed(uri: String): Boolean = + try { new JFile(new URI(uri)); true } + catch { case _: URISyntaxException | _: IllegalArgumentException => false } + + def canonical_file(uri: String): JFile = + new JFile(new URI(uri)).getCanonicalFile + + val empty: VSCode_Resources = + new VSCode_Resources(Set.empty, Map.empty, Outer_Syntax.empty) +} + +class VSCode_Resources( + loaded_theories: Set[String], + known_theories: Map[String, Document.Node.Name], + base_syntax: Outer_Syntax) + extends Resources(loaded_theories, known_theories, base_syntax) +{ + def node_name(uri: String): Document.Node.Name = + { + val file = VSCode_Resources.canonical_file(uri) // FIXME wellformed!? + val node = file.getPath + val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("") + val master_dir = if (theory == "") "" else file.getParent + Document.Node.Name(node, master_dir, theory) + } +}