← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

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

Committer: Bazaar Package Importer
Author(s): Iain Lane
Date: 2010-01-05 23:43:20 UTC
mfrom: (1.1.1 upstream)
Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu

Tags: 2.2.6-1

http://bugs.debian.org/559197

* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian)
* debian/README.source: Remove, no repacking so not necessary any more
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed.
    (Closes: #559197).
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

files added:
doc/release-notes/2-2-6.txt

src/full/Agda/Auto

src/full/Agda/Auto/Auto.hs

src/full/Agda/Auto/Convert.hs

src/full/Agda/Auto/NarrowingSearch.hs

src/full/Agda/Auto/Print.hs

src/full/Agda/Auto/SearchControl.hs

src/full/Agda/Auto/Syntax.hs

src/full/Agda/Auto/Typecheck.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs-boot

src/full/Agda/Interaction/FindFile.hs

src/full/Agda/Interaction/FindFile.hs-boot

src/full/Agda/TypeChecking/Level.hs

src/full/Agda/TypeChecking/MetaVars

src/full/Agda/TypeChecking/MetaVars/Occurs.hs

src/full/Agda/Utils/IO

src/full/Agda/Utils/IO/Binary.hs

src/full/Agda/Utils/IO/Locale.hs

src/full/Agda/Utils/IO/UTF8.hs

files removed:
debian/README.source

src/full/Agda/Utils/IO.hs

src/full/Agda/Utils/Monad

src/full/Agda/Utils/Monad/Undo.hs

src/full/Agda/Utils/Serialise.hs

files modified:
Agda.cabal

README

debian/50agda.el

debian/changelog

debian/control

debian/copyright

dist/build/Agda/Syntax/Parser/Lexer.hs

dist/build/Agda/Syntax/Parser/Parser.hs

src/agda-mode/Main.hs

src/data/Agda.css

src/data/emacs-mode/agda-input.el

src/data/emacs-mode/agda2-abbrevs.el

src/data/emacs-mode/agda2-highlight.el

src/data/emacs-mode/agda2-mode.el

src/data/emacs-mode/annotation.el

src/full/Agda/Compiler/Agate/Common.hs

src/full/Agda/Compiler/Agate/OptimizedPrinter.hs

src/full/Agda/Compiler/Alonzo/Main.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs

src/full/Agda/Compiler/MAlonzo/Encode.hs

src/full/Agda/Compiler/MAlonzo/Misc.hs

src/full/Agda/Compiler/MAlonzo/Primitives.hs

src/full/Agda/Interaction/BasicOps.hs

src/full/Agda/Interaction/CommandLine/CommandLine.hs

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/GhciTop.hs

src/full/Agda/Interaction/Highlighting/Emacs.hs

src/full/Agda/Interaction/Highlighting/Generate.hs

src/full/Agda/Interaction/Highlighting/HTML.hs

src/full/Agda/Interaction/Highlighting/Precise.hs

src/full/Agda/Interaction/Highlighting/Vim.hs

src/full/Agda/Interaction/Imports.hs

src/full/Agda/Interaction/MakeCase.hs

src/full/Agda/Interaction/Monad.hs

src/full/Agda/Interaction/Options.hs

src/full/Agda/Main.hs

src/full/Agda/Syntax/Abstract.hs

src/full/Agda/Syntax/Abstract/Name.hs

src/full/Agda/Syntax/Common.hs

src/full/Agda/Syntax/Concrete.hs

src/full/Agda/Syntax/Concrete/Definitions.hs

src/full/Agda/Syntax/Concrete/Name.hs

src/full/Agda/Syntax/Concrete/Pretty.hs

src/full/Agda/Syntax/Info.hs

src/full/Agda/Syntax/Internal.hs

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Parser.hs

src/full/Agda/Syntax/Parser/LexActions.hs

src/full/Agda/Syntax/Parser/Lexer.x

src/full/Agda/Syntax/Parser/Monad.hs

src/full/Agda/Syntax/Parser/Parser.y

src/full/Agda/Syntax/Parser/Tokens.hs

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Strict.hs

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

src/full/Agda/TypeChecking/Conversion.hs-boot

src/full/Agda/TypeChecking/Errors.hs

src/full/Agda/TypeChecking/Free.hs

src/full/Agda/TypeChecking/Injectivity.hs

src/full/Agda/TypeChecking/MetaVars.hs

src/full/Agda/TypeChecking/MetaVars.hs-boot

src/full/Agda/TypeChecking/Monad/Base.hs

src/full/Agda/TypeChecking/Monad/Builtin.hs

src/full/Agda/TypeChecking/Monad/Debug.hs

src/full/Agda/TypeChecking/Monad/Imports.hs

src/full/Agda/TypeChecking/Monad/MetaVars.hs

src/full/Agda/TypeChecking/Monad/Options.hs

src/full/Agda/TypeChecking/Monad/Signature.hs

src/full/Agda/TypeChecking/Monad/SizedTypes.hs

src/full/Agda/TypeChecking/Monad/State.hs

src/full/Agda/TypeChecking/Pretty.hs

src/full/Agda/TypeChecking/Primitive.hs

src/full/Agda/TypeChecking/Records.hs

src/full/Agda/TypeChecking/Records.hs-boot

src/full/Agda/TypeChecking/Reduce.hs

src/full/Agda/TypeChecking/Rules/Builtin.hs

src/full/Agda/TypeChecking/Rules/Data.hs

src/full/Agda/TypeChecking/Rules/Decl.hs

src/full/Agda/TypeChecking/Rules/Def.hs

src/full/Agda/TypeChecking/Rules/LHS.hs

src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs

src/full/Agda/TypeChecking/Rules/LHS/Split.hs

src/full/Agda/TypeChecking/Rules/LHS/Unify.hs

src/full/Agda/TypeChecking/Rules/Record.hs

src/full/Agda/TypeChecking/Rules/Term.hs

src/full/Agda/TypeChecking/Serialise.hs

src/full/Agda/TypeChecking/SizedTypes.hs

src/full/Agda/TypeChecking/Substitute.hs

src/full/Agda/TypeChecking/Telescope.hs

src/full/Agda/TypeChecking/Test/Generators.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Impossible.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/QuickCheck.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/TestHelpers.hs

src/full/Agda/undefined.h

Show diffs side-by-side

added added

removed removed

src/full/Agda/Interaction/Monad.hs

1

1

{-# LANGUAGE TypeSynonymInstances, MultiParamTypeClasses #-}

2

2

module Agda.Interaction.Monad where

3

3

4

4

import Agda.TypeChecking.Monad

5

5

6

6

import Control.Monad.Trans

7

import Control.Monad.Error

7

8

import System.Console.Haskeline

8

9

9

10

-- | Interaction monad.

10

11

11

12

type IM = TCMT (InputT IO)

12

13

14

instance MonadError TCErr IM where

15

throwError = liftIO . throwIO

16

catchError m h = mapTCMT liftIO $ runIM m `catchError` (runIM . h)

17

13

18

-- | Line reader. The line reader history is not stored between

14

19

-- sessions.

15

20

16

21

readline :: String -> IM (Maybe String)

17

22

readline s = lift (getInputLine s)

18

23

19

{-

20

data CurrentPoint = InInteractionPoint InteractionId | TopLevel

21

22

newtype IM a = IM {unIM :: StateT [CurrentPoint] TCM a}

23

deriving (Monad,MonadIO)

24

25

26

instance MonadError e IM where

27

throwError = lift . throwError

28

catchError m h = IM $ catchError (unIM m) (unIM . h)

29

30

31

32

instance MonadUndo [CurrentPoint] IM where

33

undo =

34

35

36

run

37

38

-}

39

40

41

24

runIM :: IM a -> TCM a

42

25

runIM = mapTCMT (runInputT defaultSettings)

Older »