edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

add type information for names found in metadata

Browse Source
This commit is contained in:
Arnaud Bailly 2020-03-02 18:49:28 +01:00
parent 2fcc0c947c
commit 2d6394c76c
2 changed files with 29 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/Idris/IDEMode/SyntaxHighlight.idr
View File

@ -99,17 +99,17 @@ outputNameSyntax (fc, (name, _, term)) =
(Ref fc Func name) => Just Function
(Ref fc (DataCon tag arity) name) => Just Data
(Ref fc (TyCon tag arity) name) => Just Typ
(Meta fc x y xs) => Nothing
(Meta fc x y xs) => Just Bound
(Bind fc x b scope) => Just Bound
(App fc fn arg) => Nothing
(As fc x as pat) => Nothing
(App fc fn arg) => Just Bound
(As fc x as pat) => Just Bound
(TDelayed fc x y) => Nothing
(TDelay fc x ty arg) => Nothing
(TForce fc x y) => Nothing
(PrimVal fc c) => Nothing
(PrimVal fc c) => Just Typ
(Erased fc imp) => Just Bound
(TType fc) => Just Typ
hilite = F.map (\ d => MkHighlight fc name False "" d "" "" "") dec
hilite = F.map (\ d => MkHighlight fc name False "" d "" (show term) "") dec
in maybe (pure ()) outputHighlight hilite
export
@ -120,6 +120,6 @@ outputSyntaxHighlighting : {auto m : Ref MD Metadata} ->
Core REPLResult
outputSyntaxHighlighting fname loadResult = do
allNames <- filter (inFile fname) . names <$> get MD
decls <- filter (inFile fname) . tydecls <$> get MD
_ <- traverse outputNameSyntax (allNames ++ decls)
-- decls <- filter (inFile fname) . tydecls <$> get MD
_ <- traverse outputNameSyntax allNames -- ++ decls)
pure loadResult

38
tests/ideMode/ideMode001/expected
View File

@ -1,20 +1,26 @@
000018(:protocol-version 2 0)
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
0000c9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c7(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c7(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c7(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:176} a)")))))) 1)
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:176}_[] ?{_:177}_[])")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:177}_[]")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:178}_[] ?{_:177}_[])")))))) 1)
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:169}_[] ?{_:168}_[])")))))) 1)
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:159} : (Main.Vect n[0] a[1])) -> (({arg:160} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:630:1--637:1 n[2] m[4]) a[3])))")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 29) (:end 5 31)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 27) (:end 5 29)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 17) (:end 5 19)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 15) (:end 5 17)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 41) (:end 5 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 38) (:end 3 39)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 25) (:end 3 27)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 23) (:end 3 25)) ((:name "k") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 3 13) (:end 3 15)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 2 19) (:end 3 6)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
000015(:return (:ok ()) 1)
Alas the file is done, aborting