mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 21:37:48 +03:00
[ refactor ] introduce allSemanticHighlighting
Side effect: all the aspects are now sorted by ranges as we are merging the PosMaps instead of appending the lists.
This commit is contained in:
parent
84a504738c
commit
a4b99bd81c
@ -90,14 +90,47 @@ record Metadata where
|
||||
nameLocMap : PosMap (NonEmptyFC, Name)
|
||||
sourceIdent : OriginDesc
|
||||
|
||||
-- Semantic Highlighting
|
||||
-- Posmap of known semantic decorations
|
||||
||| Semantic Highlighting
|
||||
||| Posmap of known semantic decorations
|
||||
semanticHighlighting : PosMap ASemanticDecoration
|
||||
-- Posmap of aliases (in `with` clauses the LHS disapear during
|
||||
-- elaboration after making sure that they match their parents'
|
||||
|
||||
||| Posmap of aliases (in `with` clauses the LHS disapear during
|
||||
||| elaboration after making sure that they match their parents'
|
||||
semanticAliases : PosMap (NonEmptyFC, NonEmptyFC)
|
||||
|
||||
||| Posmap of decorations to default to if the elaboration does not
|
||||
||| produce any highlighting for this range
|
||||
semanticDefaults : PosMap ASemanticDecoration
|
||||
|
||||
|
||||
||| Combine semanticHighlighting, semanticAliases, and semanticDefaults into
|
||||
||| a single posmap with all the information
|
||||
export
|
||||
allSemanticHighlighting :
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
Metadata -> Core (PosMap ASemanticDecoration)
|
||||
allSemanticHighlighting meta = do
|
||||
let semHigh = meta.semanticHighlighting
|
||||
log "ide-mode.highlight" 19 $
|
||||
"Semantic metadata is: " ++ show semHigh
|
||||
|
||||
let aliases
|
||||
: List ASemanticDecoration
|
||||
= flip foldMap meta.semanticAliases $ \ (from, to) =>
|
||||
let decors = uncurry exactRange (snd to) semHigh in
|
||||
map (\ ((fnm, loc), rest) => ((fnm, snd from), rest)) decors
|
||||
log "ide-mode.highlight.alias" 19 $
|
||||
"Semantic metadata from aliases is: " ++ show aliases
|
||||
|
||||
let defaults
|
||||
: List ASemanticDecoration
|
||||
= flip foldMap meta.semanticDefaults $ \ decor@((_, range), _) =>
|
||||
case uncurry exactRange range semHigh of
|
||||
[] => [decor]
|
||||
_ => []
|
||||
|
||||
pure (fromList aliases `union` (fromList defaults `union` semHigh))
|
||||
|
||||
covering
|
||||
Show Metadata where
|
||||
show (MkMetadata apps names tydecls currentLHS holeLHS nameLocMap
|
||||
|
@ -81,30 +81,13 @@ outputSyntaxHighlighting fname loadResult = do
|
||||
--decls <- filter (inFile fname) . tydecls <$> get MD
|
||||
--_ <- traverse outputNameSyntax allNames -- ++ decls)
|
||||
|
||||
let semHigh = meta.semanticHighlighting
|
||||
log "ide-mode.highlight" 19 $
|
||||
"Semantic metadata is: " ++ show semHigh
|
||||
|
||||
let aliases
|
||||
: List ASemanticDecoration
|
||||
= flip foldMap meta.semanticAliases $ \ (from, to) =>
|
||||
let decors = uncurry exactRange (snd to) semHigh in
|
||||
map (\ ((fnm, loc), rest) => ((fnm, snd from), rest)) decors
|
||||
log "ide-mode.highlight.alias" 19 $
|
||||
"Semantic metadata from aliases is: " ++ show aliases
|
||||
|
||||
let defaults
|
||||
: List ASemanticDecoration
|
||||
= flip foldMap meta.semanticDefaults $ \ decor@((_, range), _) =>
|
||||
case uncurry exactRange range semHigh of
|
||||
[] => [decor]
|
||||
_ => []
|
||||
decors <- allSemanticHighlighting meta
|
||||
|
||||
traverse_ {b = Unit}
|
||||
(\(nfc, decor, mn) =>
|
||||
case mn of
|
||||
Nothing => lwOutputHighlight (fname, nfc, decor)
|
||||
Just n => outputNameSyntax (fname, nfc, decor, n))
|
||||
(defaults ++ aliases ++ toList semHigh)
|
||||
(toList decors)
|
||||
|
||||
pure loadResult
|
||||
|
@ -1,6 +1,5 @@
|
||||
000018(:protocol-version 2 1)
|
||||
000036(:write-string "1/1: Building Syntax (Syntax.idr)" 1)
|
||||
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 28) (:end 41 29)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 0 0) (:end 0 6)) ((:decor :keyword)))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 0 7) (:end 0 13)) ((:decor :module)))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 2 0) (:end 2 8)) ((:decor :keyword)))))) 1)
|
||||
@ -238,6 +237,7 @@
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 21) (:end 41 24)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 21) (:end 41 24)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000da(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 25) (:end 41 27)) ((:name "DPair") (:namespace "Builtin.DPair") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 28) (:end 41 29)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000da(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 30) (:end 41 32)) ((:name "DPair") (:namespace "Builtin.DPair") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000ca(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 33) (:end 41 34)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d6(:output (:ok (:highlight-source ((((:filename "Syntax.idr") (:start 41 35) (:end 41 38)) ((:name "===") (:namespace "Builtin") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
|
@ -1,68 +1,5 @@
|
||||
000018(:protocol-version 2 1)
|
||||
000032(:write-string "1/1: Building With (With.idr)" 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 2) (:end 4 3)) ((:name "f") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 4) (:end 4 5)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 5 2) (:end 5 3)) ((:name "f") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 5 4) (:end 5 5)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000cd(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 2) (:end 10 3)) ((:name "g") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c6(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 5) (:end 10 6)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 7) (:end 10 9)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c9(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 10) (:end 10 12)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d2(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 2) (:end 14 8)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 9) (:end 14 10)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 4) (:end 15 10)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 11) (:end 15 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 11) (:end 15 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 15) (:end 15 16)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 4) (:end 16 10)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 11) (:end 16 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 11) (:end 16 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 15) (:end 16 16)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 6) (:end 17 12)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 13) (:end 17 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 13) (:end 17 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 13) (:end 17 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 17) (:end 17 18)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 21) (:end 17 22)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 23) (:end 17 24)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 6) (:end 18 12)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 13) (:end 18 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 13) (:end 18 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 13) (:end 18 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 17) (:end 18 18)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 21) (:end 18 22)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 23) (:end 18 24)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 8) (:end 19 14)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 19) (:end 19 20)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 23) (:end 19 24)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 25) (:end 19 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 25) (:end 19 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 29) (:end 19 30)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 31) (:end 19 32)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 8) (:end 20 14)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 19) (:end 20 20)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 23) (:end 20 24)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 25) (:end 20 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 25) (:end 20 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 29) (:end 20 30)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 31) (:end 20 32)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d2(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 21 2) (:end 21 8)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 21 9) (:end 21 10)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d5(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 2) (:end 28 10)) ((:name "someNats") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 11) (:end 28 12)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d5(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 4) (:end 29 12)) ((:name "someNats") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 13) (:end 29 14)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 13) (:end 29 14)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d0(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 20) (:end 29 26)) ((:name "MkANat") (:namespace "With") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 27) (:end 29 28)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
00006f(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 0 0) (:end 0 6)) ((:decor :keyword)))))) 1)
|
||||
00006f(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 0 7) (:end 0 11)) ((:decor :module)))))) 1)
|
||||
000070(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 2 0) (:end 2 1)) ((:decor :function)))))) 1)
|
||||
@ -107,6 +44,8 @@
|
||||
000071(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 3 15) (:end 3 16)) ((:decor :keyword)))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 3 17) (:end 3 22)) ((:decor :keyword)))))) 1)
|
||||
00006f(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 3 23) (:end 3 25)) ((:decor :bound)))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 2) (:end 4 3)) ((:name "f") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 4) (:end 4 5)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 4) (:end 4 5)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
00006f(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 6) (:end 4 7)) ((:decor :keyword)))))) 1)
|
||||
0000d0(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 8) (:end 4 9)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
@ -117,6 +56,8 @@
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 24) (:end 4 26)) ((:name "MkDPair") (:namespace "Builtin.DPair") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d2(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 27) (:end 4 30)) ((:name "sym") (:namespace "Builtin") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 4 31) (:end 4 33)) ((:name "eq") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 5 2) (:end 5 3)) ((:name "f") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 5 4) (:end 5 5)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 5 4) (:end 5 5)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
00006f(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 5 6) (:end 5 7)) ((:decor :keyword)))))) 1)
|
||||
00006f(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 5 8) (:end 5 9)) ((:decor :keyword)))))) 1)
|
||||
@ -157,8 +98,12 @@
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 9 24) (:end 9 26)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 9 24) (:end 9 26)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 9 26) (:end 9 27)) ((:decor :keyword)))))) 1)
|
||||
0000cd(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 2) (:end 10 3)) ((:name "g") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 4) (:end 10 5)) ((:decor :keyword)))))) 1)
|
||||
0000c6(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 5) (:end 10 6)) ((:name "a") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c6(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 5) (:end 10 6)) ((:name "b") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 7) (:end 10 9)) ((:name "::") (:namespace "Prelude.Basics") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c9(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 10) (:end 10 12)) ((:name "as") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c9(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 10) (:end 10 12)) ((:name "bs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 12) (:end 10 13)) ((:decor :keyword)))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 10 14) (:end 10 15)) ((:decor :keyword)))))) 1)
|
||||
@ -178,6 +123,8 @@
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 13 15) (:end 13 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 13 15) (:end 13 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 13 16) (:end 13 17)) ((:decor :keyword)))))) 1)
|
||||
0000d2(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 2) (:end 14 8)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 9) (:end 14 10)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 9) (:end 14 10)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 11) (:end 14 12)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 13) (:end 14 14)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
@ -191,14 +138,22 @@
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 25) (:end 14 26)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 25) (:end 14 26)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 14 26) (:end 14 27)) ((:decor :keyword)))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 4) (:end 15 10)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 11) (:end 15 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 11) (:end 15 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 11) (:end 15 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 13) (:end 15 14)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 15) (:end 15 16)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 17) (:end 15 18)) ((:decor :keyword)))))) 1)
|
||||
000070(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 19) (:end 15 20)) ((:decor :data)))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 21) (:end 15 22)) ((:decor :keyword)))))) 1)
|
||||
000070(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 15 23) (:end 15 24)) ((:decor :data)))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 4) (:end 16 10)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 11) (:end 16 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 11) (:end 16 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 11) (:end 16 12)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 13) (:end 16 14)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 15) (:end 16 16)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 17) (:end 16 18)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 19) (:end 16 20)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 21) (:end 16 22)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
@ -212,17 +167,31 @@
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 33) (:end 16 34)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 33) (:end 16 34)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 16 34) (:end 16 35)) ((:decor :keyword)))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 6) (:end 17 12)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 13) (:end 17 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 13) (:end 17 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 13) (:end 17 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 13) (:end 17 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 15) (:end 17 16)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 17) (:end 17 18)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 19) (:end 17 20)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 21) (:end 17 22)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 23) (:end 17 24)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 23) (:end 17 24)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 25) (:end 17 26)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 27) (:end 17 28)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 29) (:end 17 30)) ((:decor :keyword)))))) 1)
|
||||
000070(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 17 31) (:end 17 32)) ((:decor :data)))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 6) (:end 18 12)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 13) (:end 18 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 13) (:end 18 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 13) (:end 18 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 13) (:end 18 14)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 15) (:end 18 16)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 17) (:end 18 18)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 19) (:end 18 20)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 21) (:end 18 22)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 23) (:end 18 24)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 23) (:end 18 24)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 25) (:end 18 26)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 27) (:end 18 28)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
@ -237,27 +206,51 @@
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 41) (:end 18 42)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 41) (:end 18 42)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 18 42) (:end 18 43)) ((:decor :keyword)))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 8) (:end 19 14)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 15) (:end 19 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 17) (:end 19 18)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 19) (:end 19 20)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 21) (:end 19 22)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 23) (:end 19 24)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 25) (:end 19 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 25) (:end 19 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 25) (:end 19 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 27) (:end 19 28)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 29) (:end 19 30)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 31) (:end 19 32)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 31) (:end 19 32)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 33) (:end 19 34)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 35) (:end 19 36)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 37) (:end 19 38)) ((:decor :keyword)))))) 1)
|
||||
000070(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 19 39) (:end 19 40)) ((:decor :data)))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 8) (:end 20 14)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 15) (:end 20 16)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 17) (:end 20 18)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 19) (:end 20 20)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 21) (:end 20 22)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 23) (:end 20 24)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 25) (:end 20 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 25) (:end 20 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 25) (:end 20 26)) ((:name "k") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 27) (:end 20 28)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 29) (:end 20 30)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 31) (:end 20 32)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 31) (:end 20 32)) ((:name "l") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 33) (:end 20 34)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 35) (:end 20 36)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 37) (:end 20 38)) ((:name "p") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 39) (:end 20 40)) ((:decor :keyword)))))) 1)
|
||||
000070(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 20 41) (:end 20 42)) ((:decor :data)))))) 1)
|
||||
0000d2(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 21 2) (:end 21 8)) ((:name "nested") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 21 9) (:end 21 10)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c7(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 21 9) (:end 21 10)) ((:name "m") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 21 11) (:end 21 12)) ((:decor :keyword)))))) 1)
|
||||
0000d4(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 21 13) (:end 21 14)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
@ -296,6 +289,8 @@
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 27 24) (:end 27 25)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 27 24) (:end 27 25)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 27 25) (:end 27 26)) ((:decor :keyword)))))) 1)
|
||||
0000d5(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 2) (:end 28 10)) ((:name "someNats") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 11) (:end 28 12)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 11) (:end 28 12)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 13) (:end 28 14)) ((:decor :keyword)))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 15) (:end 28 16)) ((:decor :bound)))))) 1)
|
||||
@ -312,10 +307,15 @@
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 41) (:end 28 42)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 41) (:end 28 42)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 28 42) (:end 28 43)) ((:decor :keyword)))))) 1)
|
||||
0000d5(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 4) (:end 29 12)) ((:name "someNats") (:namespace "With") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 13) (:end 29 14)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 13) (:end 29 14)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 15) (:end 29 16)) ((:decor :keyword)))))) 1)
|
||||
000071(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 17) (:end 29 18)) ((:decor :bound)))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 18) (:end 29 19)) ((:decor :keyword)))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 19) (:end 29 20)) ((:decor :keyword)))))) 1)
|
||||
0000d0(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 20) (:end 29 26)) ((:name "MkANat") (:namespace "With") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 27) (:end 29 28)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c8(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 27) (:end 29 28)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 28) (:end 29 29)) ((:decor :keyword)))))) 1)
|
||||
000073(:output (:ok (:highlight-source ((((:filename "With.idr") (:start 29 30) (:end 29 31)) ((:decor :keyword)))))) 1)
|
||||
|
@ -1,8 +1,5 @@
|
||||
000018(:protocol-version 2 1)
|
||||
000038(:write-string "1/1: Building WithApp (WithApp.idr)" 1)
|
||||
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 2) (:end 10 4)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 2) (:end 11 4)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 15) (:end 11 17)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 0 0) (:end 0 4)) ((:decor :keyword)))))) 1)
|
||||
000070(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 0 5) (:end 0 10)) ((:decor :type)))))) 1)
|
||||
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 0 11) (:end 0 12)) ((:decor :keyword)))))) 1)
|
||||
@ -64,16 +61,19 @@
|
||||
0000c9(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 16) (:end 9 17)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000c9(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 16) (:end 9 17)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 17) (:end 9 18)) ((:decor :keyword)))))) 1)
|
||||
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 2) (:end 10 4)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 5) (:end 10 6)) ((:decor :keyword)))))) 1)
|
||||
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 7) (:end 10 8)) ((:decor :keyword)))))) 1)
|
||||
0000cd(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 9) (:end 10 10)) ((:name "Z") (:namespace "Main") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 11) (:end 10 12)) ((:decor :keyword)))))) 1)
|
||||
0000d7(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 13) (:end 10 14)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 2) (:end 11 4)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 5) (:end 11 6)) ((:decor :keyword)))))) 1)
|
||||
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 7) (:end 11 8)) ((:decor :keyword)))))) 1)
|
||||
0000cd(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 9) (:end 11 10)) ((:name "S") (:namespace "Main") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 11) (:end 11 12)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 13) (:end 11 14)) ((:decor :keyword)))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 15) (:end 11 17)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 18) (:end 11 19)) ((:decor :keyword)))))) 1)
|
||||
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 20) (:end 11 21)) ((:decor :keyword)))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 22) (:end 11 23)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
|
||||
|
Loading…
Reference in New Issue
Block a user