--- a/src/Tools/VSCode/extension/src/library.ts Tue Feb 22 12:23:21 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts Tue Feb 22 21:30:39 2022 +0100
@@ -14,6 +14,11 @@
/* strings */
+export function quote(s: string): string
+{
+ return "\"" + s + "\""
+}
+
export function reverse(s: string): string
{
return s.split("").reverse().join("")
@@ -24,6 +29,23 @@
return text.includes("\n") || text.includes("\r")
}
+
+/* settings environment */
+
+export function getenv(name: string): string
+{
+ const s = process.env[name]
+ return s || ""
+}
+
+export function getenv_strict(name: string): string
+{
+ const s = getenv(name)
+ if (s) return s
+ else throw new Error("Undefined Isabelle environment variable: " + quote(name))
+}
+
+
/* platform information */
export function platform_is_windows(): boolean