# HG changeset patch
# User wenzelm
# Date 1645561839 -3600
# Node ID 8c7bdd68a47a3c45810ab87b3358cfb2622f9259
# Parent  1fed80019bff8f9e8fc4ef5929ff0f3ae39eb976
more operations;

diff -r 1fed80019bff -r 8c7bdd68a47a src/Tools/VSCode/extension/src/library.ts
--- 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