← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Interaction/Response.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Interaction/Response.hs
1
1
------------------------------------------------------------------------
2
2
-- | Data type for all interactive responses
3
3
------------------------------------------------------------------------
4
 
{-# LANGUAGE CPP, TypeSynonymInstances, FlexibleInstances #-}
 
4
 
 
5
{-# LANGUAGE CPP #-}
 
6
{-# LANGUAGE FlexibleInstances #-}
 
7
{-# LANGUAGE TypeSynonymInstances #-}
5
8
 
6
9
module Agda.Interaction.Response
7
10
  ( Response (..)
 
11
  , MakeCaseVariant (..)
8
12
  , DisplayInfo (..)
9
13
  , Status (..)
10
14
  , GiveResult (..)
13
17
  ) where
14
18
 
15
19
import Agda.Interaction.Highlighting.Precise
16
 
import Agda.Interaction.FindFile (ModuleToSource)
17
 
--import Agda.Interaction.MakeCase
18
20
import Agda.TypeChecking.Monad.Base
 
21
import Agda.Syntax.Common   (InteractionId(..))
19
22
import Agda.Syntax.Concrete (Expr)
20
23
import Agda.Utils.Pretty
21
24
 
 
25
import Control.Monad.Trans
22
26
import Data.Int
 
27
import System.IO
23
28
 
24
29
#include "../undefined.h"
25
30
import Agda.Utils.Impossible
35
40
    | Resp_JumpToError FilePath Int32
36
41
    | Resp_InteractionPoints [InteractionId]
37
42
    | Resp_GiveAction InteractionId GiveResult
38
 
    | Resp_MakeCaseAction [String]
39
 
    | Resp_MakeCase String [String]
 
43
    | Resp_MakeCase MakeCaseVariant [String]
40
44
    | Resp_SolveAll [(InteractionId, Expr)]
41
45
    | Resp_DisplayInfo DisplayInfo
42
 
    | Resp_RunningInfo String
 
46
    | Resp_RunningInfo Int String
 
47
      -- ^ The integer is the message's debug level.
43
48
    | Resp_ClearRunningInfo
44
49
    | Resp_ClearHighlighting
45
50
 
 
51
-- | There are two kinds of \"make case\" commands.
 
52
 
 
53
data MakeCaseVariant = Function | ExtendedLambda
 
54
 
46
55
-- | Info to display at the end of an interactive command
47
56
 
48
57
data DisplayInfo
59
68
        -- ^ 'Info_Auto' denotes either an error or a success (when 'Resp_GiveAction' is present)
60
69
        --   TODO: split these into separate constructors
61
70
    | Info_ModuleContents Doc
 
71
    | Info_WhyInScope Doc
62
72
    | Info_NormalForm Doc
63
73
    | Info_GoalType Doc
64
74
    | Info_CurrentGoal Doc
65
75
    | Info_InferredType Doc
66
76
    | Info_Context Doc
 
77
    | Info_HelperFunction Doc
67
78
        deriving Show
68
79
 
69
80
-- | Status information.
106
117
 
107
118
type InteractionOutputCallback = Response -> TCM ()
108
119
 
 
120
-- | The default 'InteractionOutputCallback' function prints certain
 
121
-- things to stdout (other things generate internal errors).
109
122
 
110
123
defaultInteractionOutputCallback :: InteractionOutputCallback
111
 
defaultInteractionOutputCallback = __IMPOSSIBLE__
 
124
defaultInteractionOutputCallback r = case r of
 
125
  Resp_HighlightingInfo {}  -> __IMPOSSIBLE__
 
126
  Resp_Status {}            -> __IMPOSSIBLE__
 
127
  Resp_JumpToError {}       -> __IMPOSSIBLE__
 
128
  Resp_InteractionPoints {} -> __IMPOSSIBLE__
 
129
  Resp_GiveAction {}        -> __IMPOSSIBLE__
 
130
  Resp_MakeCase {}          -> __IMPOSSIBLE__
 
131
  Resp_SolveAll {}          -> __IMPOSSIBLE__
 
132
  Resp_DisplayInfo {}       -> __IMPOSSIBLE__
 
133
  Resp_RunningInfo _ s      -> liftIO $ do
 
134
                                 putStr s
 
135
                                 hFlush stdout
 
136
  Resp_ClearRunningInfo {}  -> __IMPOSSIBLE__
 
137
  Resp_ClearHighlighting {} -> __IMPOSSIBLE__