src/Tools/VSCode/extension/src/library.ts

--- a/src/Tools/VSCode/extension/src/library.ts	Mon Jun 12 15:20:07 2017 +0200
+++ b/src/Tools/VSCode/extension/src/library.ts	Mon Jun 12 15:40:40 2017 +0200
@@ -4,6 +4,14 @@
 import { TextEditor, Uri, workspace } from 'vscode'
 
 
+/* regular expressions */
+
+export function escape_regex(s: string): string
+{
+  return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&")
+}
+
+
 /* platform information */
 
 export function platform_is_windows(): boolean