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