11// Common logic extracted from Main.res for shared use between desktop and web entry points
22
33// if end with '.agda' or '.lagda'
4- let isAgda = (fileName ): bool => {
5- let fileName = fileName -> Parser .filepath
6- RegExp .test (%re ("/\. agda$|\. lagda/i" ), fileName )
7- }
4+ let isAgda = (document ): bool =>
5+ RegExp .test (%re ("/\. agda$|\. lagda/i" ), document -> VSCode .TextDocument .fileName )
86
97module Inputs : {
108 let onOpenEditor : (VSCode .TextEditor .t => unit ) => VSCode .Disposable .t
@@ -27,8 +25,7 @@ module Inputs: {
2725 VSCode .Commands .registerCommand ("agda-mode." ++ name , () => {
2826 VSCode .Window .activeTextEditor -> Option .map (
2927 editor => {
30- let fileName = editor -> VSCode .TextEditor .document -> VSCode .TextDocument .fileName
31- if isAgda (fileName ) {
28+ if isAgda (editor -> VSCode .TextEditor .document ) {
3229 callback (command , editor )
3330 } else {
3431 Promise .resolve (None )
@@ -47,7 +44,6 @@ let initialize = (
4744 globalStorageUri ,
4845 memento ,
4946 editor ,
50- fileName ,
5147 semanticTokensRequest ,
5248) => {
5349 let panel = Singleton .Panel .make (extensionUri )
@@ -91,8 +87,8 @@ let initialize = (
9187 -> WebviewPanel .onEvent (event => {
9288 switch getCurrentEditor () {
9389 | Some (editor ') =>
94- let fileName ' =
95- editor '-> VSCode .TextEditor .document -> VSCode .TextDocument .fileName -> Parser . filepath
90+ let fileName = editor -> VSCode . TextEditor . document -> VSCode . TextDocument . fileName
91+ let fileName ' = editor '-> VSCode .TextEditor .document -> VSCode .TextDocument .fileName
9692 if fileName ' == fileName {
9793 State__Command .dispatchCommand (state , Command .EventFromView (event ))-> ignore
9894 }
@@ -147,8 +143,7 @@ let registerDocumentSemanticTokensProvider = () => {
147143 let tokenModifiers = Highlighting__SemanticToken .TokenModifier .enumurate
148144
149145 let provideDocumentSemanticTokens = (document , _cancel ) => {
150- let fileName = document -> VSCode .TextDocument .fileName -> Parser .filepath
151- Registry .requestSemanticTokens (fileName )
146+ Registry .requestSemanticTokens (document )
152147 -> Promise .thenResolve (tokens => {
153148 open Editor .Provider .Mock
154149
@@ -225,17 +220,17 @@ let activateWithoutContext = (
225220
226221 // on open editor
227222 Inputs .onOpenEditor (editor => {
228- let fileName = editor -> VSCode .TextEditor .document -> VSCode . TextDocument . fileName
223+ let document = editor -> VSCode .TextEditor .document
229224
230225 // filter out ".agda.git" files
231- if isAgda (fileName ) {
232- Registry .get (fileName )
226+ if isAgda (document ) {
227+ Registry .get (document )
233228 -> Option .flatMap (entry => entry .state )
234229 -> Option .forEach (state => {
235230 // after switching tabs, the old editor would be "_disposed"
236231 // we need to replace it with this new one
237232 state .editor = editor
238- state .document = editor -> VSCode . TextEditor . document
233+ state .document = document
239234 State__Command .dispatchCommand (state , Refresh )-> ignore
240235 })
241236 }
@@ -265,22 +260,21 @@ let activateWithoutContext = (
265260
266261 // on close editor
267262 Inputs .onCloseDocument (document => {
268- let fileName = VSCode .TextDocument .fileName (document )-> Parser .filepath
269- if isAgda (fileName ) {
270- Registry .removeAndDestroy (fileName )-> ignore
263+ if isAgda (document ) {
264+ Registry .removeAndDestroy (document )-> ignore
271265 finalize (false )-> ignore
272266 }
273267 })-> subscribe
274268 // on triggering commands
275269 Inputs .onTriggerCommand (async (command , editor ) => {
276- let fileName = editor -> VSCode .TextEditor .document -> VSCode . TextDocument . fileName
270+ let document = editor -> VSCode .TextEditor .document
277271 // destroy
278272 switch command {
279273 | Quit =>
280- await Registry .removeAndDestroy (fileName )
274+ await Registry .removeAndDestroy (document )
281275 finalize (false )
282276 | Restart =>
283- await Registry .removeAndDestroy (fileName )
277+ await Registry .removeAndDestroy (document )
284278 finalize (true )
285279 | _ => ()
286280 }
@@ -289,7 +283,7 @@ let activateWithoutContext = (
289283 | Load
290284 | Restart
291285 | InputMethod (Activate ) =>
292- switch Registry .get (fileName ) {
286+ switch Registry .get (document ) {
293287 | None =>
294288 let state = initialize (
295289 platformDeps ,
@@ -298,10 +292,9 @@ let activateWithoutContext = (
298292 globalStorageUri ,
299293 memento ,
300294 editor ,
301- fileName ,
302295 None ,
303296 )
304- Registry .add (fileName , state )
297+ Registry .add (document , state )
305298 | Some (entry ) =>
306299 switch entry .state {
307300 | None =>
@@ -313,18 +306,17 @@ let activateWithoutContext = (
313306 globalStorageUri ,
314307 memento ,
315308 editor ,
316- fileName ,
317309 Some (entry .semanticTokens ),
318310 )
319- Registry .add (fileName , state )
311+ Registry .add (document , state )
320312 | Some (_ ) => () // should not happen
321313 }
322314 }
323315 | _ => ()
324316 }
325317 // dispatch
326318
327- switch Registry .get (fileName )-> Option .flatMap (entry => entry .state ) {
319+ switch Registry .get (document )-> Option .flatMap (entry => entry .state ) {
328320 | None => None
329321 | Some (state ) =>
330322 await State__Command .dispatchCommand (state , command )
0 commit comments