idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-22 11:13:36 +03:00
Code Issues Projects Releases Wiki Activity
2f66f3e006
Idris2/tests/ideMode/ideMode005/expectedC
Ohad Kammar e58bcfc7ef
Semantic highlighting (#1335) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-05-10 09:05:43 +01:00

82 lines
13 KiB
Plaintext
Raw Blame History

000018(:protocol-version 2 0)
000038(:write-string "1/1: Building WithApp (WithApp.idr)" 1)
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 3) (:end 11 4)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 3) (:end 12 4)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 16) (:end 12 17)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 1 1) (:end 1 4)) ((:decor :keyword)))))) 1)
000070(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 1 6) (:end 1 10)) ((:decor :type)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 1 12) (:end 1 12)) ((:decor :keyword)))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 1 14) (:end 1 16)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 1 18) (:end 1 19)) ((:decor :keyword)))))) 1)
000071(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 1 21) (:end 1 24)) ((:decor :type)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 1 26) (:end 1 30)) ((:decor :keyword)))))) 1)
00006f(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 2 3) (:end 2 3)) ((:decor :data)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 2 5) (:end 2 5)) ((:decor :keyword)))))) 1)
0000cf(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 2 7) (:end 2 11)) ((:name "Natty") (:namespace "Main") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 2 13) (:end 2 13)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
00006f(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 3) (:end 3 3)) ((:decor :data)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 5) (:end 3 5)) ((:decor :keyword)))))) 1)
0000cf(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 7) (:end 3 11)) ((:name "Natty") (:namespace "Main") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 13) (:end 3 13)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 15) (:end 3 16)) ((:decor :keyword)))))) 1)
0000d0(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 18) (:end 3 22)) ((:name "Natty") (:namespace "Main") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 24) (:end 3 24)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 25) (:end 3 25)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 27) (:end 3 27)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 3 28) (:end 3 28)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 1) (:end 5 4)) ((:decor :function)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 6) (:end 5 6)) ((:decor :keyword)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 8) (:end 5 8)) ((:decor :keyword)))))) 1)
0000c7(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 9) (:end 5 9)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 10) (:end 5 10)) ((:decor :keyword)))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 12) (:end 5 14)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 15) (:end 5 15)) ((:decor :keyword)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 17) (:end 5 18)) ((:decor :keyword)))))) 1)
0000d0(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 20) (:end 5 24)) ((:name "Natty") (:namespace "Main") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 5 26) (:end 5 26)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 6 1) (:end 6 4)) ((:name "view") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 6 6) (:end 6 6)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 6 8) (:end 6 8)) ((:decor :keyword)))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 6 10) (:end 6 10)) ((:name "Z") (:namespace "Main") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 1) (:end 7 4)) ((:name "view") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 6) (:end 7 6)) ((:decor :keyword)))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 7) (:end 7 7)) ((:name "S") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c7(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 9) (:end 7 9)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 10) (:end 7 10)) ((:decor :keyword)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 12) (:end 7 12)) ((:decor :keyword)))))) 1)
0000cc(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 14) (:end 7 14)) ((:name "S") (:namespace "Main") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 16) (:end 7 16)) ((:decor :keyword)))))) 1)
0000d3(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 17) (:end 7 20)) ((:name "view") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 22) (:end 7 22)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 7 23) (:end 7 23)) ((:decor :keyword)))))) 1)
000073(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 1) (:end 9 2)) ((:decor :function)))))) 1)
000072(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 4) (:end 9 4)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 6) (:end 9 8)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 10) (:end 9 11)) ((:decor :keyword)))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 9 13) (:end 9 15)) ((:name "Nat") (:namespace "Prelude.Types") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d1(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 1) (:end 10 2)) ((:name "id") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000c9(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 4) (:end 10 4)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 6) (:end 10 9)) ((:decor :keyword)))))) 1)
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 11) (:end 10 11)) ((:decor :keyword)))))) 1)
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 11) (:end 10 11)) ((:decor :keyword)))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 12) (:end 10 15)) ((:name "view") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000d5(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 12) (:end 10 15)) ((:name "view") (:namespace "Main") (:decor :function) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 17) (:end 10 17)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 17) (:end 10 17)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 10 18) (:end 10 18)) ((:decor :keyword)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 6) (:end 11 6)) ((:decor :keyword)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 8) (:end 11 8)) ((:decor :keyword)))))) 1)
0000ce(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 10) (:end 11 10)) ((:name "Z") (:namespace "Main") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 12) (:end 11 12)) ((:decor :keyword)))))) 1)
0000d7(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 11 14) (:end 11 14)) ((:name "Z") (:namespace "Prelude.Types") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 6) (:end 12 6)) ((:decor :keyword)))))) 1)
000074(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 8) (:end 12 8)) ((:decor :keyword)))))) 1)
0000ce(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 10) (:end 12 10)) ((:name "S") (:namespace "Main") (:decor :data) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 12) (:end 12 12)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 14) (:end 12 14)) ((:decor :keyword)))))) 1)
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 19) (:end 12 19)) ((:decor :keyword)))))) 1)
000076(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 21) (:end 12 21)) ((:decor :keyword)))))) 1)
0000cb(:output (:ok (:highlight-source ((((:filename "WithApp.idr") (:start 12 23) (:end 12 23)) ((:name "n") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "")))))) 1)
000015(:return (:ok ()) 1)
Alas the file is done, aborting
Reference in New Issue View Git Blame Copy Permalink