From 387938d70540f7ec8847d1e2cd1849d022581ec9 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 13 Dec 2024 17:15:27 +0100 Subject: [PATCH] feat: address code review --- lean4-infoview/src/infoview/userWidget.tsx | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx index b3bafc53..2cd3680c 100644 --- a/lean4-infoview/src/infoview/userWidget.tsx +++ b/lean4-infoview/src/infoview/userWidget.tsx @@ -30,6 +30,9 @@ const moduleCache = new Map() * and must have been annotated with `@[widget]` or `@[widget_module]` * at some point before `pos`. * + * If `hash` does not correspond to a registered module, + * the promise is rejected with an error. + * * #### Experimental `import` support for widget modules * * The module may import other `@[widget_module]`s by hash @@ -81,11 +84,8 @@ export async function importWidgetModule(rs: RpcSessionAtPos, pos: DocumentPosit await importWidgetModule(rs, pos, h) // `moduleCache.has(h)` is a postcondition of `importWidgetModule` const [_, uri] = moduleCache.get(h)! - /* HACK: `es-module-lexer` doesn't provide indices of `import`s into the module source, - * so just replace the `import`ed name wholesale wherever it appears. - * It will break any module that relies on having that string literal intact, - * but such modules ought to be extremely unusual. */ - src = src.replace(i.n, uri) + // Replace imported module name with the new URI + src = src.substring(0, i.s) + uri + src.substring(i.e) } } const [mod, uri] = await dynamicallyLoadModule(hash, src)