Changes between Version 42 and Version 43 of Holes


Ignore:
Timestamp:
Aug 5, 2012 9:59:29 PM (3 years ago)
Author:
vilhelm_s
Comment:

How should holes interact with with GHC API?

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v42 v43  
    393393    In the definition of `main': main = _?x >>= return
    394394}}}
     395
     396= API access to Holes =
     397
     398Another open question is how to
     399programmatically get information back from GHC. It seems that so far we are
     400just thinking about printing a warning message from the compiler. But in order
     401to write something like Agda-mode, I guess we ultimately want to expose this in
     402the GHC API, so programs like [ghc-mod
     403http://www.haskell.org/haskellwiki/Haskell_mode_for_Emacs#ghc-mod ghc-mod] can display
     404the holes information and let the user move between them.
     405
     406This seems tricky since it doesn't fit completely with the way the GHC API is
     407currently set up. I think there are two options:
     408
     4091. Treat them like warning messages are currently handled, and extend the
     410"listener" callback which gets called during compilation to have messages about
     411holes as well as warnings in general.
     412
     413However, this is not very uniform: the list of holes in a module is
     414more similar to the list of top-level bindings in the modules, so the API for
     415querying them should be similar.
     416
     4172. Treat them like top-level bindings, and have a set of methods for querying
     418them that way.
     419
     420Currently, GHC is set up so that each time you compile a module a .hi is
     421generated, and all the API methods for querying for module information looks at
     422the .hi file. So this alternative entails modifying the .hi file format to also
     423have a section about holes.
     424
     425What is the best way to do this?