Wire web playground to LSP code

This commit is contained in:
2026-02-25 19:41:57 -08:00
parent f3b8b1b7b5
commit d5b5ee8265
10 changed files with 185 additions and 103 deletions

View File

@@ -29,7 +29,6 @@ decomposeName fn =
then go (x :: acc) xs
else (joinBy "/" (xs :< x <>> Nil), joinBy "." acc)
switchModule : FileSource String M (Maybe ModContext)
switchModule repo modns = do
-- TODO processing on hover is expensive, but info is not always there
@@ -69,10 +68,18 @@ getHoverInfo repo modns row col = do
pure $ HasHover e.fc ("\{show e.name} : \{rpprint Nil ty}")
where
-- We don't want to pick up the paren token when on the border
isIdent : BTok Bool
isIdent (MkBounded (Tok Ident _) _) = True
isIdent (MkBounded (Tok UIdent _) _) = True
isIdent (MkBounded (Tok MixFix _) _) = True
isIdent (MkBounded (Tok Projection _) _) = True
isIdent _ = False
getTok : List BTok Maybe String
getTok Nil = Nothing
getTok (tok :: toks) =
if tok.bounds.startCol <= col && (col <= tok.bounds.endCol)
if tok.bounds.startCol <= col && col <= tok.bounds.endCol && isIdent tok
then Just $ value tok else getTok toks
data FileEdit = MkEdit FC String

View File

@@ -16,6 +16,7 @@ import Commands
import Lib.ProcessDecl
import Lib.Prettier
import Lib.Error
import Lib.Compile
pfunc js_castArray : Array JSObject JSObject := `x => x`
pfunc js_castInt : Int JSObject := `x => x`
@@ -224,4 +225,25 @@ checkFile fn = unsafePerformIO $ do
modifyIORef state $ [ topContext := top ]
pure $ jsonToJObject $ JsonArray json
#export updateFile checkFile hoverInfo codeActionInfo
compileJS : String JSObject
compileJS fn = unsafePerformIO $ do
let (base, modName) = decomposeName fn
st <- readIORef state
when (st.baseDir /= base) $ \ _ => resetState base
repo <- lspFileSource
(Right (top, src)) <- (do
putStrLn "woo"
mod <- processModule emptyFC repo Nil modName
docs <- compile
let src = unlines $
( "const bouncer = (f,ini) => { let obj = ini; while (obj.tag) obj = f(obj); return obj.h0 };"
:: Nil)
++ map (render 90 noAlt) docs
pure src).runM st.topContext
| Left err => pure $ js_castStr "// \{errorMsg err}"
modifyIORef state [ topContext := top ]
pure $ js_castStr src
#export updateFile checkFile hoverInfo codeActionInfo compileJS

View File

@@ -37,10 +37,10 @@ deriveEq fc name = do
where
arr : Raw Raw Raw
arr a b = RPi emptyFC (BI fc "_" Explicit Many) a b
arr a b = RPi fc (BI fc "_" Explicit Many) a b
rvar : String Raw
rvar nm = RVar emptyFC nm
rvar nm = RVar fc nm
getExplictNames : SnocList String Tm List String
getExplictNames acc (Pi fc nm Explicit quant a b) = getExplictNames (acc :< nm) b
@@ -49,7 +49,7 @@ deriveEq fc name = do
getExplictNames acc _ = acc <>> Nil
buildApp : String List Raw Raw
buildApp nm nms = foldl (\ t u => RApp emptyFC t u Explicit) (rvar nm) $ nms
buildApp nm nms = foldl (\ t u => RApp fc t u Explicit) (rvar nm) $ nms
equate : (Raw × Raw) Raw
equate (a,b) = buildApp "_==_" (a :: b :: Nil)
@@ -89,13 +89,13 @@ deriveShow fc name = do
where
arr : Raw Raw Raw
arr a b = RPi emptyFC (BI fc "_" Explicit Many) a b
arr a b = RPi fc (BI fc "_" Explicit Many) a b
rvar : String Raw
rvar nm = RVar emptyFC nm
rvar nm = RVar fc nm
lstring : String Raw
lstring s = RLit emptyFC (LString s)
lstring s = RLit fc (LString s)
getExplictNames : SnocList String Tm List String
getExplictNames acc (Pi fc nm Explicit quant a b) = getExplictNames (acc :< nm) b
@@ -104,7 +104,7 @@ deriveShow fc name = do
getExplictNames acc _ = acc <>> Nil
buildApp : String List Raw Raw
buildApp nm nms = foldl (\ t u => RApp emptyFC t u Explicit) (rvar nm) $ nms
buildApp nm nms = foldl (\ t u => RApp fc t u Explicit) (rvar nm) $ nms
equate : (Raw × Raw) Raw
equate (a,b) = buildApp "_==_" (a :: b :: Nil)
@@ -118,7 +118,7 @@ deriveShow fc name = do
let names = getExplictNames Lin ty
anames <- map rvar <$> traverse freshName names
let left = buildApp "show" $ buildApp nm anames :: Nil
let shows = map (\ nm => RApp emptyFC (rvar "show") nm Explicit) anames
let shows = map (\ nm => RApp fc (rvar "show") nm Explicit) anames
let right = case anames of
Nil => lstring nm
_ =>