Skip to content

Commit de064de

Browse files
Add option to use built-in browser (#15)
1 parent 698b253 commit de064de

File tree

5 files changed

+17
-6
lines changed

5 files changed

+17
-6
lines changed

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,5 @@ out
22
node_modules
33
.vscode-test
44
*.vsix
5+
_opam
56
tmp

.vscodeignore

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,4 +18,4 @@ src/node_modules/**
1818
!src/node_modules/{minimatch,brace-expansion,concat-map,balanced-match}/**
1919
!src/node_modules/{semver,lru-cache,yallist}/**
2020
tmp
21-
_opam
21+
_opam

package-lock.json

Lines changed: 2 additions & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

package.json

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"author": "Imandra Inc",
66
"publisher": "imandra",
77
"license": "MIT",
8-
"version": "0.0.7",
8+
"version": "0.0.8",
99
"repository": {
1010
"type": "git",
1111
"url": "https://github.com/imandra-ai/imandrax-vscode"
@@ -82,6 +82,12 @@
8282
"type": "boolean",
8383
"default": false,
8484
"description": "Use fresh model module names (e.g. M42) for interactive models (otherwise overwrite module M)"
85+
},
86+
"imandrax.useSimpleBrowser": {
87+
"scope": "window",
88+
"type": "boolean",
89+
"default": true,
90+
"description": "Use the built-in Simple Browser to open links (otherwise the system default browser)"
8591
}
8692
}
8793
},
@@ -160,4 +166,4 @@
160166
"mocha": "^9.2.1",
161167
"typescript": "^5.2.2"
162168
}
163-
}
169+
}

src/extension.ts

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,11 @@ export function check_all(): Thenable<void> | undefined {
151151
}
152152

153153
export function browse(uri: string): Thenable<boolean> | undefined {
154-
return env.openExternal(uri as any);
154+
const config = workspace.getConfiguration("imandrax");
155+
if (config.useSimpleBrowser)
156+
return commands.executeCommand("simpleBrowser.api.open", uri);
157+
else
158+
return env.openExternal(uri as any);
155159
}
156160

157161
export function toggle_full_ids(): Thenable<void> | undefined {

0 commit comments

Comments
 (0)