diff --git a/src/GF/Compile/BackOpt.hs b/src/GF/Compile/BackOpt.hs
index 529a74334..089a192d5 100644
--- a/src/GF/Compile/BackOpt.hs
+++ b/src/GF/Compile/BackOpt.hs
@@ -21,7 +21,6 @@ import GF.Grammar.Grammar
 import GF.Infra.Ident
 import GF.Infra.Option
 import qualified GF.Grammar.Macros as C
-import GF.Grammar.PrGrammar (prt)
 import GF.Data.Operations
 import Data.List
 import qualified GF.Infra.Modules as M
@@ -72,7 +71,7 @@ factor c i t = case t of
 
 --- we hope this will be fresh and don't check... in GFC would be safe
 
-qqIdent c i = identC (BS.pack ("q_" ++ prt c ++ "__" ++ show i))
+qqIdent c i = identC (BS.pack ("q_" ++ showIdent c ++ "__" ++ show i))
 
 
 --  we need to replace subterms
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index cc2083a47..58c168565 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -32,7 +32,7 @@ import GF.Compile.TypeCheck
 import GF.Compile.Refresh
 import GF.Grammar.Lexer
 import GF.Grammar.Grammar
-import GF.Grammar.PrGrammar
+import GF.Grammar.Printer
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
 import GF.Grammar.Macros
@@ -45,43 +45,37 @@ import GF.Infra.CheckM
 
 import Data.List
 import qualified Data.Set as Set
-import qualified Data.Map as Map
 import Control.Monad
-import Debug.Trace ---
-
+import Text.PrettyPrint
 
 showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
-showCheckModule mos m = do
-  (st,(_,msg)) <- checkStart $ checkModule mos m
-  return (st, unlines $ reverse msg)
-
-mapsCheckTree :: 
-  (Ord a) => ((a,b) -> Check (a,c)) -> BinTree a b -> Check (BinTree a c)
-mapsCheckTree f = checkErr . mapsErrTree (\t -> checkStart (f t) >>= return . fst)
-
+showCheckModule mos m =
+  case runCheck (checkModule mos m) of
+    Left        msgs  -> Bad (   render (vcat (reverse msgs)))
+    Right (st,_,msgs) -> Ok (st, render (vcat (reverse msgs)))
 
 -- | checking is performed in the dependency order of modules
 checkModule :: [SourceModule] -> SourceModule -> Check [SourceModule]
-checkModule ms (name,mo) = checkIn ("checking module" +++ prt name) $ do
+checkModule ms (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do
     let js = jments mo
     checkRestrictedInheritance ms (name, mo)
     js' <- case mtype mo of
-      MTAbstract -> mapsCheckTree (checkAbsInfo gr name mo) js
+      MTAbstract -> checkMap (checkAbsInfo gr name mo) js
 
-      MTTransfer a b -> mapsCheckTree (checkAbsInfo gr name mo) js
+      MTTransfer a b -> checkMap (checkAbsInfo gr name mo) js
 
-      MTResource -> mapsCheckTree (checkResInfo gr name mo) js
+      MTResource -> checkMap (checkResInfo gr name mo) js
 
       MTConcrete a -> do
         checkErr $ topoSortOpers $ allOperDependencies name js
         abs <- checkErr $ lookupModule gr a
         js1 <- checkCompleteGrammar gr abs mo
-        mapsCheckTree (checkCncInfo gr name mo (a,abs)) js1
+        checkMap (checkCncInfo gr name mo (a,abs)) js1
 
-      MTInterface -> mapsCheckTree (checkResInfo gr name mo) js
+      MTInterface -> checkMap (checkResInfo gr name mo) js
 
       MTInstance a -> do
-        mapsCheckTree (checkResInfo gr name mo) js
+        checkMap (checkResInfo gr name mo) js
 
     return $ (name, replaceJudgements mo js') : ms
  where
@@ -104,22 +98,21 @@ checkRestrictedInheritance mos (name,mo) = do
            (f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
      case illegals of 
        [] -> return ()
-       cs -> fail $ "In inherited module" +++ prt i ++
-               ", dependence of excluded constants:" ++++
-               unlines ["  " ++ prt f +++ "on" +++ unwords (map prt is) | 
-                              (f,is) <- cs]
+       cs -> checkError (text "In inherited module" <+> ppIdent i <> text ", dependence of excluded constants:" $$
+                         nest 2 (vcat [ppIdent f <+> text "on" <+> fsep (map ppIdent is) | (f,is) <- cs]))
    allDeps = concatMap (allDependencies (const True) . jments . snd) mos
 
 -- | check if a term is typable
 justCheckLTerm :: SourceGrammar -> Term -> Err Term
-justCheckLTerm src t = do
-  ((t',_),_) <- checkStart (inferLType src t)
-  return t'
+justCheckLTerm src t =
+  case runCheck (inferLType src t) of
+    Left msgs          -> Bad (   render (vcat (reverse msgs)))
+    Right ((t',_),_,_) -> Ok t'
 
 checkAbsInfo :: 
-  SourceGrammar -> Ident -> SourceModInfo -> (Ident,Info) -> Check (Ident,Info)
-checkAbsInfo st m mo (c,info) = do
----- checkReservedId c
+  SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
+checkAbsInfo st m mo c info = do
+ checkReservedId c
  case info of
    AbsCat (Just cont) _ -> mkCheck "category" $ 
      checkContext st cont ---- also cstrs
@@ -130,25 +123,16 @@ checkAbsInfo st m mo (c,info) = do
      case md of
        Just eqs -> mkCheck "definition of function" $
 	             checkDef st (m,c) typ eqs
-       Nothing  -> return (c,info)
-     return $ (c,AbsFun (Just typ) ma md)
-   _ -> return (c,info)
+       Nothing  -> return info
+     return $ (AbsFun (Just typ) ma md)
+   _ -> return info
  where
    mkCheck cat ss = case ss of
-     [] -> return (c,info)
-     _  -> checkErr $ Bad (unlines ss ++++ "in" +++ cat +++ prt c +++ pos c)
-   ---- temporary solution when tc of defs is incomplete
-   mkCheckWarn cat ss = case ss of
-     [] -> return (c,info)
-     ["[]"] -> return (c,info) ----
-     _  -> do
-       checkWarn (unlines ss ++++ "in" +++ cat +++ prt c +++ pos c)
-       return (c,info)
-
-   pos c = showPosition mo c
+     [] -> return info
+     _  -> checkError (vcat (map text ss) $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition mo c)
 
    compAbsTyp g t = case t of
-     Vr x -> maybe (fail ("no value given to variable" +++ prt x)) return $ lookup x g
+     Vr x -> maybe (checkError (text "no value given to variable" <+> ppIdent x)) return $ lookup x g
      Let (x,(_,a)) b -> do
        a' <- compAbsTyp g a
        compAbsTyp ((x, a'):g) b
@@ -169,8 +153,7 @@ checkCompleteGrammar gr abs cnc = do
   -- remove those lincat and lin in concrete that are not in abstract
   let unkn = filter (not . flip isInBinTree jsa) fsc
   jsc1 <- if (null unkn) then return jsc else do
-    checkWarn $ "ignoring constants not in abstract:" +++ 
-                unwords (map prt unkn)
+    checkWarn $ text "ignoring constants not in abstract:" <+> fsep (map ppIdent unkn)
     return $ filterBinTree (\f _ -> notElem f unkn) jsc 
 
   -- check that all abstract constants are in concrete; build default lincats
@@ -196,32 +179,30 @@ checkCompleteGrammar gr abs cnc = do
                                   Ok (CncFun cty Nothing  pn) ->
                                     case mb_def of
                                       Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js
-                                      Bad _  -> do checkWarn $ "no linearization of" +++ prt c
+                                      Bad _  -> do checkWarn $ text "no linearization of" <+> ppIdent c
                                                    return js
                                   _ -> do
                                     case mb_def of
                                       Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js
-                                      Bad _  -> do checkWarn $ "no linearization of" +++ prt c
+                                      Bad _  -> do checkWarn $ text "no linearization of" <+> ppIdent c
                                                    return js
      AbsCat (Just _) _ -> case lookupIdent c js of
        Ok (AnyInd _ _) -> return js
        Ok (CncCat (Just _) _ _) -> return js
        Ok (CncCat _ mt mp) -> do
          checkWarn $ 
-           "no linearization type for" +++ prt c ++ 
-           ", inserting default {s : Str}" 
+           text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}"
          return $ updateTree (c,CncCat (Just defLinType) mt mp) js
        _ -> do
          checkWarn $ 
-           "no linearization type for" +++ prt c ++ 
-           ", inserting default {s : Str}" 
+           text "no linearization type for" <+> ppIdent c <> text ", inserting default {s : Str}"
          return $ updateTree (c,CncCat (Just defLinType) Nothing Nothing) js
      _ -> return js
 
 -- | General Principle: only Just-values are checked. 
 -- A May-value has always been checked in its origin module.
-checkResInfo :: SourceGrammar -> Ident -> SourceModInfo -> (Ident,Info) -> Check (Ident,Info)
-checkResInfo gr mo mm (c,info) = do
+checkResInfo :: SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
+checkResInfo gr mo mm c info = do
   checkReservedId c
   case info of
     ResOper pty pde -> chIn "operation" $ do
@@ -234,47 +215,43 @@ checkResInfo gr mo mm (c,info) = do
            (de',ty') <- infer de
            return (Just ty', Just de')
          (_      , Nothing) -> do
-           raise "No definition given to oper"
-      return (c, ResOper pty' pde')
+           checkError (text "No definition given to the operation")
+      return (ResOper pty' pde')
 
     ResOverload os tysts -> chIn "overloading" $ do
       tysts' <- mapM (uncurry $ flip check) tysts  -- return explicit ones
       tysts0 <- checkErr $ lookupOverload gr mo c  -- check against inherited ones too
       tysts1 <- mapM (uncurry $ flip check) 
                   [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
-      let tysts2 = [(y,x) | (x,y) <- tysts1]
       --- this can only be a partial guarantee, since matching
       --- with value type is only possible if expected type is given
       checkUniq $ 
-        sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]]
-      return (c,ResOverload os [(y,x) | (x,y) <- tysts'])
+        sort [t : map snd xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
+      return (ResOverload os [(y,x) | (x,y) <- tysts'])
 
     ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
-----      mapM ((mapM (computeLType gr . snd)) . snd) pcs
-      mapM_ ((mapM_ (checkIfParType gr . snd)) . snd) pcs
       ts <- checkErr $ lookupParamValues gr mo c
-      return (c,ResParam (Just (pcs, Just ts)))
+      return (ResParam (Just (pcs, Just ts)))
 
-    _ ->  return (c,info)
+    _ ->  return info
  where
    infer = inferLType gr
    check = checkLType gr
-   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ pos c +++ ":")
+   chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mm c <+> colon)
    comp = computeLType gr
-   pos c = showPosition mm c
 
    checkUniq xss = case xss of
      x:y:xs 
-      | x == y -> raise $ "ambiguous for type" +++ 
-                           prtType gr (mkFunType (tail x) (head x))  
+      | x == y    -> checkError $ text "ambiguous for type" <+>
+                                  ppType gr (mkFunType (tail x) (head x))  
       | otherwise -> checkUniq $ y:xs
      _ -> return ()
 
 
 checkCncInfo :: SourceGrammar -> Ident -> SourceModInfo -> 
                 (Ident,SourceModInfo) -> 
-                (Ident,Info) -> Check (Ident,Info)
-checkCncInfo gr m mo (a,abs) (c,info) = do
+                Ident -> Info -> Check Info
+checkCncInfo gr m mo (a,abs) c info = do
   checkReservedId c
   case info of
 
@@ -285,73 +262,28 @@ checkCncInfo gr m mo (a,abs) (c,info) = do
       (trm',_)   <- check trm (mkFunType (map snd cont) val)  -- erases arg vars
       checkPrintname gr mpr
       cat        <- return $ snd cat0
-      return (c, CncFun (Just (cat,(cont,val))) (Just trm') mpr)
+      return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
                                                    -- cat for cf, typ for pe
 
     CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do
       checkErr $ lookupCatContext gr a c
-      typ'  <- checkIfLinType gr typ
+      typ'  <- computeLType gr typ
       mdef' <- case mdef of
         Just def -> do
           (def',_) <- checkLType gr def (mkFunType [typeStr] typ)
           return $ Just def'
         _ -> return mdef
       checkPrintname gr mpr
-      return (c,CncCat (Just typ') mdef' mpr)
+      return (CncCat (Just typ') mdef' mpr)
 
-    _ -> checkResInfo gr m mo (c,info)
+    _ -> checkResInfo gr m mo c info
 
  where
    env = gr
    infer = inferLType gr
    comp = computeLType gr 
    check = checkLType gr
-   chIn cat = checkIn ("Happened in" +++ cat +++ prt c +++ pos c +++ ":")
-   pos c = showPosition mo c
-
-checkIfParType :: SourceGrammar -> Type -> Check ()
-checkIfParType st typ = checkCond ("Not parameter type" +++ prt typ) (isParType typ)
-  where
-   isParType ty = True ----
-{- case ty of
-     Cn typ -> case lookupConcrete st typ of
-       Ok (CncParType _ _ _) -> True
-       Ok (CncOper _ ty' _) -> isParType ty'
-       _ -> False
-     Q p t -> case lookupInPackage st (p,t) of
-       Ok (CncParType _ _ _) -> True
-       _ -> False
-     RecType r -> all (isParType . snd) r
-     _ -> False
--}
-
-checkIfStrType :: SourceGrammar -> Type -> Check ()
-checkIfStrType st typ = case typ of
-  Table arg val -> do
-    checkIfParType st arg 
-    checkIfStrType st val
-  _ | typ == typeStr -> return ()
-  _ -> prtFail "not a string type" typ
-
-
-checkIfLinType :: SourceGrammar -> Type -> Check Type
-checkIfLinType st typ0 = do
-  typ <- computeLType st typ0
-{- ---- should check that not fun type
-  case typ of
-    RecType r -> do
-      let (lins,ihs) = partition (isLinLabel .fst) r
-      --- checkErr $ checkUnique $ map fst r
-      mapM_ checkInh ihs
-      mapM_ checkLin lins
-    _ -> prtFail "a linearization type cannot be" typ
--}
-  return typ
-
- where
-   checkInh (label,typ) = checkIfParType st typ
-   checkLin (label,typ) = return () ---- checkIfStrType st typ
-
+   chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
 
 computeLType :: SourceGrammar -> Type -> Check Type
 computeLType gr t = do
@@ -363,7 +295,7 @@ computeLType gr t = do
     _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
       | isPredefConstant ty     -> return ty ---- shouldn't be needed
 
-    Q m ident -> checkIn ("module" +++ prt m) $ do
+    Q m ident -> checkIn (text "module" <+> ppIdent m) $ do
       ty' <- checkErr (lookupResDef gr m ident) 
       if ty' == ty then return ty else comp ty' --- is this necessary to test?
 
@@ -412,17 +344,9 @@ checkPrintname _  _        = return ()
 -- | for grammars obtained otherwise than by parsing ---- update!!
 checkReservedId :: Ident -> Check ()
 checkReservedId x
-  | isReservedWord (ident2bs x) = checkWarn ("reserved word used as identifier:" +++ prt x)
+  | isReservedWord (ident2bs x) = checkWarn (text "reserved word used as identifier:" <+> ppIdent x)
   | otherwise                   = return ()
 
--- to normalize records and record types
-labelIndex :: Type -> Label -> Int
-labelIndex ty lab = case ty of
-  RecType ts -> maybe (error ("label index" +++ prt lab)) id $ lookup lab $ labs ts
-  _ -> error $ "label index" +++ prt ty
- where 
-  labs ts = zip (map fst (sortRec ts)) [0..]
-
 -- the underlying algorithms
 
 inferLType :: SourceGrammar -> Term -> Check (Term, Type)
@@ -435,7 +359,7 @@ inferLType gr trm = case trm of
      ,
      checkErr (lookupResDef gr m ident) >>= infer
      ,
-     prtFail "cannot infer type of constant" trm
+     checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
      ]
 
    QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
@@ -445,7 +369,7 @@ inferLType gr trm = case trm of
        ,
        checkErr (lookupResDef gr m ident) >>= infer
        ,
-       prtFail "cannot infer type of canonical constant" trm
+       checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
        ]
 
    Val _ ty i -> termWith trm $ return ty
@@ -471,8 +395,7 @@ inferLType gr trm = case trm of
                       then return val
                       else substituteLType [(z,a')] val
              return (App f' a',ty) 
-           _ -> raise ("function type expected for"+++ 
-                      prt f +++"instead of" +++ prtType env fty)
+           _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType env fty)
 
    S f x -> do
      (f', fty) <- infer f
@@ -480,24 +403,25 @@ inferLType gr trm = case trm of
        Table arg val -> do
          x'<- justCheck x arg
          return (S f' x', val)
-       _ -> prtFail "table lintype expected for the table in" trm
+       _ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
 
    P t i -> do
      (t',ty) <- infer t   --- ??
      ty' <- comp ty
------     let tr2 = PI t' i (labelIndex ty' i)
      let tr2 = P t' i
-     termWith tr2 $ checkErr $ case ty' of
-       RecType ts -> maybeErr ("unknown label" +++ prt i +++ "in" +++ prt ty') $ 
-                     lookup i ts
-       _ -> prtBad ("record type expected for" +++ prt t +++ "instead of") ty'
+     termWith tr2 $ case ty' of
+       RecType ts -> case lookup i ts of
+                       Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
+                       Just x  -> return x
+       _          -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
+                                 text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
    PI t i _ -> infer $ P t i
 
    R r -> do
      let (ls,fs) = unzip r
      fsts <- mapM inferM fs
      let ts = [ty | (Just ty,_) <- fsts]
-     checkCond ("cannot infer type of record"+++ prt trm) (length ts == length fsts)
+     checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
      return $ (R (zip ls fsts), RecType (zip ls ts))
 
    T (TTyped arg) pts -> do
@@ -509,7 +433,7 @@ inferLType gr trm = case trm of
    T ti pts -> do  -- tries to guess: good in oper type inference
      let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
      case pts' of 
-       [] -> prtFail "cannot infer table type of" trm
+       [] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
 ----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
        _  -> do 
          (arg,val) <- checks $ map (inferCase Nothing) pts'
@@ -542,9 +466,8 @@ inferLType gr trm = case trm of
 
 ---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
    Strs (Cn c : ts) | c == cConflict -> do
-     trace ("WARNING: unresolved constant, could be any of" +++ unwords (map prt ts)) (infer $ head ts)
---     checkWarn ("unresolved constant, could be any of" +++ unwords (map prt ts))
---     infer $ head ts
+     checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
+     infer (head ts)
 
    Strs ts -> do
      ts' <- mapM (\t -> justCheck t typeStr) ts 
@@ -576,7 +499,7 @@ inferLType gr trm = case trm of
          rt <- checkErr $ plusRecType rT' sT'
          check trm' rt ---- return (trm', rt)
        _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
-       _ -> prtFail "records or record types expected in" trm
+       _ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
 
    Sort _     -> 
      termWith trm $ return typeType
@@ -608,7 +531,7 @@ inferLType gr trm = case trm of
      ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
      return $ (ELin c trm', ty') 
 
-   _ -> prtFail "cannot infer lintype of" trm
+   _ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
 
  where
    env = gr
@@ -685,28 +608,23 @@ getOverload env@gr mt ot = case appForm ot of
      case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
        ([(val,fun)],_) -> return (mkApp fun tts, val)
        ([],[(val,fun)]) -> do
-         checkWarn ("ignoring lock fields in resolving" +++ prt ot) 
+         checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
          return (mkApp fun tts, val)
        ([],[]) -> do
          ---- let prtType _ = prt  -- to debug grammars
-         let sought = unwords (map (prtType env) tys)
-         let showTypes ty = case unwords (map (prtType env) ty) of
-               s | s == sought -> 
-                 s +++ "  -- i.e." +++ unwords (map prt ty) ++++
-                 "     where we sought" +++ unwords (map prt tys)
-               s -> s
-         raise $ "no overload instance of" +++ prt f +++ 
-           "for" +++ 
-           sought +++
-           "among" ++++ 
-           unlines ["  " ++ showTypes ty | (ty,_) <- typs] ++
-           maybe [] (("with value type" +++) . prtType env) mt
+         let showTypes ty = vcat (map (ppType env) ty)
+         checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
+                      text "for" $$
+                      nest 2 (showTypes tys) $$
+                      text "among" $$
+                      nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$
+                      maybe empty (\x -> text "with value type" <+> ppType env x) mt
 
        (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
          ([(val,fun)],_) -> do
            return (mkApp fun tts, val)
          ([],[(val,fun)]) -> do
-           checkWarn ("ignoring lock fields in resolving" +++ prt ot) 
+           checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
            return (mkApp fun tts, val)
 
 ----- unsafely exclude irritating warning AR 24/5/2008
@@ -715,9 +633,10 @@ getOverload env@gr mt ot = case appForm ot of
 -----             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
 
 
-         _ -> raise $ "ambiguous overloading of" +++ prt f +++
-             "for" +++ unwords (map (prtType env) tys) ++++ "with alternatives" ++++ 
-             unlines [prtType env ty | (ty,_) <- if (null vfs1) then vfs2 else vfs2]
+         _ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
+                           text "for" <+> hsep (map (ppType env) tys) $$ 
+                           text "with alternatives" $$
+                           nest 2 (vcat [ppType env ty | (ty,_) <- if null vfs1 then vfs2 else vfs2])
 
    matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
 
@@ -755,11 +674,11 @@ checkLType env trm typ0 = do
           (c',b') <- if isWildIdent z
                         then check c b
                         else do
-                          b' <- checkIn "abs" $ substituteLType [(z,Vr x)] b
+                          b' <- checkIn (text "abs") $ substituteLType [(z,Vr x)] b
                           check c b'
           checkReset
           return $ (Abs x c', Prod x a b')
-        _ -> raise $ "function type expected instead of" +++ prtType env typ
+        _ -> checkError $ text "function type expected instead of" <+> ppType env typ
 
     App f a -> do
        over <- getOverload env (Just typ) trm
@@ -778,7 +697,7 @@ checkLType env trm typ0 = do
           termWith trm' $ checkEq typ ty' trm'
 
     T _ [] ->
-      prtFail "found empty table in type" typ
+      checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
     T _ cs -> case typ of 
       Table arg val -> do 
         case allParamValues env arg of
@@ -787,20 +706,12 @@ checkLType env trm typ0 = do
             ps <- checkErr $ testOvershadow ps0 vs
             if null ps 
               then return () 
----- use this if you want to see where the error is
---              else raise $ "patterns never reached:" +++ 
---                               concat (intersperse ", " (map prt ps))
----- else use this
-              else trace ("WARNING: patterns never reached:" +++ 
-                               concat (intersperse ", " (map prt ps))) (return ())
----- AR 6/4/2009: this would be the best but checkWarn doesn't show because of laziness (?)
-----              else checkWarn $ "patterns never reached:" +++ 
-----                               concat (intersperse ", " (map prt ps))
-
+              else checkWarn (text "patterns never reached:" $$
+                              nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
           _ -> return () -- happens with variable types
         cs' <- mapM (checkCase arg val) cs
         return (T (TTyped arg) cs', typ)
-      _ -> raise $ "table type expected for table instead of" +++ prtType env typ
+      _ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType env typ)
 
     R r -> case typ of --- why needed? because inference may be too difficult
        RecType rr -> do
@@ -808,7 +719,7 @@ checkLType env trm typ0 = do
          fsts <- mapM (checkM r) rr   -- check that they are found in the record
          return $ (R fsts, typ)       -- normalize record
 
-       _ -> prtFail "record type expected in type checking instead of" typ
+       _ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
 
     ExtR r s -> case typ of
        _ | typ == typeType -> do
@@ -817,7 +728,7 @@ checkLType env trm typ0 = do
            RecType _ -> termWith trm $ return typeType
            ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
                                       -- ext t = t ** ...
-           _ -> prtFail "invalid record type extension" trm
+           _ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
        RecType rr -> do
          (r',ty,s') <- checks [
             do (r',ty) <- infer r
@@ -832,15 +743,15 @@ checkLType env trm typ0 = do
                 r2 <- justCheck r' rr0
                 s2 <- justCheck s' rr2
                 return $ (ExtR r2 s2, typ) 
-           _ -> raise ("record type expected in extension of" +++ prt r +++ 
-                       "but found" +++ prt ty)
+           _ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
+                            text "but found" <+> ppTerm Unqualified 0 ty)
 
        ExtR ty ex -> do
          r' <- justCheck r ty
          s' <- justCheck s ex
          return $ (ExtR r' s', typ) --- is this all?
 
-       _ -> prtFail "record extension not meaningful for" typ
+       _ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
 
     FV vs -> do
       ttys <- mapM (flip check typ) vs
@@ -855,8 +766,7 @@ checkLType env trm typ0 = do
           (arg',val) <- check arg p
           checkEq typ t trm
           return (S tab' arg', t)
-        _ -> raise $ "table type expected for applied table instead of" +++ 
-                   prtType env ty'
+        _ -> checkError (text "table type expected for applied table instead of" <+> ppType env ty')
      , do
       (arg',ty) <- infer arg
       ty'       <- comp ty
@@ -903,14 +813,12 @@ checkLType env trm typ0 = do
      Just (_,t) -> do
        (t',ty') <- check t ty
        return (l,(Just ty',t'))
-     _ -> raise $ 
-       if isLockLabel l 
-       then
-         let cat = drop 5 (prt l) in
-         prt_ (R rms) +++ "is not in the lincat of" +++ cat ++ 
-         "; try wrapping it with lin " ++ cat
-       else
-         "cannot find value for label" +++ prt l +++ "in" +++ prt_ (R rms)
+     _ -> checkError $ 
+            if isLockLabel l 
+              then let cat = drop 5 (showIdent (label2ident l))
+                   in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <> 
+                      text "; try wrapping it with lin" <+> text cat
+              else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
 
    checkCase arg val (p,t) = do
      cont <- pattContext env arg p
@@ -925,7 +833,7 @@ pattContext env typ p = case p of
   PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
     t <- checkErr $ lookupResType cnc q c
     (cont,v) <- checkErr $ typeFormCnc t
-    checkCond ("wrong number of arguments for constructor in" +++ prt p) 
+    checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
               (length cont == length ps)
     checkEqLType env typ v (patt2term p)
     mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
@@ -936,7 +844,7 @@ pattContext env typ p = case p of
         let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
         ----- checkWarn $ prt p ++++ show pts ----- debug
         mapM (uncurry (pattContext env)) pts >>= return . concat
-      _ -> prtFail "record type expected for pattern instead of" typ'
+      _ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
   PT t p' -> do
     checkEqLType env typ t (patt2term p')
     pattContext env typ p'
@@ -948,11 +856,11 @@ pattContext env typ p = case p of
   PAlt p' q -> do
     g1 <- pattContext env typ p'
     g2 <- pattContext env typ q
-    let pts = [pt | pt <- g1, notElem pt g2] ++ [pt | pt <- g2, notElem pt g1]
+    let pts = nub ([fst pt | pt <- g1, notElem pt g2] ++ [fst pt | pt <- g2, notElem pt g1])
     checkCond 
-      ("incompatible bindings of" +++ 
-       unwords (nub (map (prt . fst) pts))+++ 
-       "in pattern alterantives" +++ prt p) (null pts) 
+      (text "incompatible bindings of" <+>
+       fsep (map ppIdent pts) <+> 
+       text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
     return g1 -- must be g1 == g2
   PSeq p q -> do
     g1 <- pattContext env typ p
@@ -967,7 +875,7 @@ pattContext env typ p = case p of
    noBind typ p' = do
     co <- pattContext env typ p'
     if not (null co)
-      then checkWarn ("no variable bound inside pattern" +++ prt p) 
+      then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
            >> return []
       else return []
 
@@ -999,9 +907,9 @@ checkEqLType env t u trm = do
   (b,t',u',s) <- checkIfEqLType env t u trm
   case b of
     True  -> return t'
-    False -> raise $ s +++ "type of" +++ prt trm +++ 
-                        ": expected:" +++ prtType env t ++++ 
-                        "inferred:" +++ prtType env u
+    False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
+                          text "expected:" <+> ppType env t $$
+                          text "inferred:" <+> ppType env u
 
 checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
 checkIfEqLType env t u trm = do
@@ -1013,7 +921,7 @@ checkIfEqLType env t u trm = do
     --- better: use a flag to forgive? (AR 31/1/2006)
     _ -> case missingLock [] t' u' of
       Ok lo -> do
-        checkWarn $ "missing lock field" +++ unwords (map prt lo)
+        checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo)
         return (True,t',u',[])
       Bad s -> return (False,t',u',s)
 
@@ -1066,7 +974,7 @@ checkIfEqLType env t u trm = do
                    not (any (\ (k,b) -> alpha g a b && l == k) ts)]
          (locks,others) = partition isLockLabel ls
        in case others of
-         _:_ -> Bad $ "missing record fields" +++ unwords (map prt others)
+         _:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others))
          _ -> return locks
      -- contravariance
      (Prod x a b, Prod y c d) -> do
@@ -1079,24 +987,15 @@ checkIfEqLType env t u trm = do
    sTypes = [typeStr, typeTok, typeString]
    comp = computeLType env
 
--- if prtType is misleading, print the full type
-prtTypeF :: LTEnv -> Type -> Type -> String
-prtTypeF env exp ty = 
- let pty = prtType env ty 
- in if pty == prtType env exp then prt ty else pty
-
 -- printing a type with a lock field lock_C as C
-prtType :: LTEnv -> Type -> String
-prtType env ty = case ty of
-  RecType fs -> case filter isLockLabel $ map fst fs of
-    [lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty
-    _ -> prtt ty
-  Prod x a b -> prtType env a +++ "->" +++ prtType env b
-  _ -> prtt ty
- where
-   prtt t = prt t
-   ---- use computeLType gr to check if really equal to the cat with lock
-
+ppType :: LTEnv -> Type -> Doc
+ppType env ty =
+  case ty of
+    RecType fs -> case filter isLockLabel $ map fst fs of
+                    [lock] -> text (drop 5 (showIdent (label2ident lock)))
+                    _      -> ppTerm Unqualified 0 ty
+    Prod x a b -> ppType env a <+> text "->" <+> ppType env b
+    _          -> ppTerm Unqualified 0 ty
 
 -- | linearization types and defaults
 linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
@@ -1111,8 +1010,11 @@ linTypeOfType cnc m typ = do
      let vars = mkRecType varLabel $ replicate n typeStr
 	 symb = argIdent n cat i
      rec <- if n==0 then return val else
-            checkErr $ errIn ("extending" +++ prt vars +++ "with" +++ prt val) $
-            plusRecType vars val
+            checkErr $ errIn (render (text "extending" $$
+                                      nest 2 (ppTerm Unqualified 0 vars) $$
+                                      text "with" $$
+                                      nest 2 (ppTerm Unqualified 0 val))) $
+                             plusRecType vars val
      return (symb,rec)
    lookLin (_,c) = checks [ --- rather: update with defLinType ?
       checkErr (lookupLincat cnc m c) >>= computeLType cnc
@@ -1148,5 +1050,5 @@ topoSortOpers st = do
   let eops = topoTest st
   either 
     return 
-    (\ops -> Bad ("circular definitions:" +++ unwords (map prt (head ops))))
+    (\ops -> Bad (render (text "circular definitions:" <+> fsep (map ppIdent (head ops)))))
     eops
diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs
index 115f3e319..881166695 100644
--- a/src/GF/Compile/GrammarToGFCC.hs
+++ b/src/GF/Compile/GrammarToGFCC.hs
@@ -38,7 +38,7 @@ traceD s t = t
 -- the main function: generate PGF from GF.
 mkCanon2gfcc :: Options -> String -> SourceGrammar -> (String,D.PGF)
 mkCanon2gfcc opts cnc gr = 
-  (prIdent abs, (canon2gfcc opts pars . reorder abs . canon2canon opts abs) gr)
+  (showIdent abs, (canon2gfcc opts pars . reorder abs . canon2canon opts abs) gr)
   where
     abs = err (const c) id $ M.abstractOfConcrete gr c where c = identC (BS.pack cnc)
     pars = mkParamLincat gr
diff --git a/src/GF/Compile/ReadFiles.hs b/src/GF/Compile/ReadFiles.hs
index 0b4850b1f..b12ced07e 100644
--- a/src/GF/Compile/ReadFiles.hs
+++ b/src/GF/Compile/ReadFiles.hs
@@ -198,7 +198,7 @@ importsOfModule (m,mi) = (modName m,depModInfo mi [])
 
     depInst (m,n) xs = modName m:modName n:xs
 
-    modName = prIdent
+    modName = showIdent
 
 -- | options can be passed to the compiler by comments in @--#@, in the main file
 getOptionsFromFile :: FilePath -> IOE Options
diff --git a/src/GF/Compile/Update.hs b/src/GF/Compile/Update.hs
index ec5161403..e4e827451 100644
--- a/src/GF/Compile/Update.hs
+++ b/src/GF/Compile/Update.hs
@@ -58,7 +58,7 @@ extendModule gr (name,m)
 
      -- test that the module types match, and find out if the old is complete
      testErr (sameMType (mtype m) (mtype mo)) 
-             ("illegal extension type to module" +++ prIdent name)
+             ("illegal extension type to module" +++ showIdent name)
 
      let isCompl = isCompleteModule m0
 
@@ -86,12 +86,12 @@ rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
     -- add the information given in interface into an instance module
     Nothing -> do
       testErr (null is || mstatus mi == MSIncomplete) 
-              ("module" +++ prIdent i +++ 
+              ("module" +++ showIdent i +++ 
                "has open interfaces and must therefore be declared incomplete") 
       case mt of
         MTInstance i0 -> do
           m1 <- lookupModule gr i0
-          testErr (isModRes m1) ("interface expected instead of" +++ prIdent i0)
+          testErr (isModRes m1) ("interface expected instead of" +++ showIdent i0)
           js' <- extendMod gr False (i0,const True) i (jments m1) (jments mi)
           --- to avoid double inclusions, in instance I of I0 = J0 ** ...
           case extends mi of
@@ -110,7 +110,7 @@ rebuildModule gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ js_ ps_)) = do
       let stat' = ifNull MSComplete (const MSIncomplete)
                     [i | i <- is, notElem i infs]
       testErr (stat' == MSComplete || stat == MSIncomplete) 
-              ("module" +++ prIdent i +++ "remains incomplete")
+              ("module" +++ showIdent i +++ "remains incomplete")
       ModInfo mt0 _ fs me' _ ops0 _ js ps0 <- lookupModule gr ext
       let ops1 = nub $
                    ops_ ++ -- N.B. js has been name-resolved already
diff --git a/src/GF/Grammar/Lookup.hs b/src/GF/Grammar/Lookup.hs
index b136eee83..f6cf60873 100644
--- a/src/GF/Grammar/Lookup.hs
+++ b/src/GF/Grammar/Lookup.hs
@@ -54,16 +54,16 @@ unlock c = unlockRecord c -- return
 -- to look up a constant etc in a search tree --- why here? AR 29/5/2008
 lookupIdent :: Ident -> BinTree Ident b -> Err b
 lookupIdent c t =
-  case lookupTree prIdent c t of
+  case lookupTree showIdent c t of
     Ok v  -> return v
-    Bad _ -> Bad ("unknown identifier" +++ prIdent c)
+    Bad _ -> Bad ("unknown identifier" +++ showIdent c)
 
 lookupIdentInfo :: ModInfo Ident a -> Ident -> Err a
 lookupIdentInfo mo i = lookupIdent i (jments mo)
 
 lookupIdentInfoIn :: ModInfo Ident a -> Ident -> Ident -> Err a
 lookupIdentInfoIn mo m i = 
-  err (\s -> Bad (s +++ "in module" +++ prIdent m)) return $ lookupIdentInfo mo i
+  err (\s -> Bad (s +++ "in module" +++ showIdent m)) return $ lookupIdentInfo mo i
 
 lookupResDef :: SourceGrammar -> Ident -> Ident -> Err Term
 lookupResDef gr m c = liftM fst $ lookupResDefKind gr m c
diff --git a/src/GF/Grammar/MMacros.hs b/src/GF/Grammar/MMacros.hs
index f00859ffd..84b365225 100644
--- a/src/GF/Grammar/MMacros.hs
+++ b/src/GF/Grammar/MMacros.hs
@@ -214,7 +214,7 @@ freeVarsExp e = case e of
   _ -> [] --- thus applies to abstract syntax only
 
 ident2string :: Ident -> String
-ident2string = prIdent
+ident2string = showIdent
 {-
 tree :: (TrNode,[Tree]) -> Tree
 tree = Tr
diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs
index c7a9cfa73..b195292eb 100644
--- a/src/GF/Grammar/Macros.hs
+++ b/src/GF/Grammar/Macros.hs
@@ -350,10 +350,10 @@ float2term = EFloat
 
 -- | create a terminal from identifier
 ident2terminal :: Ident -> Term
-ident2terminal = K . prIdent
+ident2terminal = K . showIdent
 
 symbolOfIdent :: Ident -> String
-symbolOfIdent = prIdent
+symbolOfIdent = showIdent
 
 symid :: Ident -> String
 symid = symbolOfIdent
diff --git a/src/GF/Grammar/Parser.hs b/src/GF/Grammar/Parser.hs
index 699870f18..e9d0d7c3a 100644
--- a/src/GF/Grammar/Parser.hs
+++ b/src/GF/Grammar/Parser.hs
@@ -753,7 +753,7 @@ happyReduction_3 (happy_x_4 `HappyStk`
                                                 Ok x    -> return x
                                                 Bad msg -> fail msg
                                       let poss  = buildTree [(i,(fname,mkSrcSpan p)) | (i,p,_) <- jments]
-                                          fname = prIdent id ++ ".gf"
+                                          fname = showIdent id ++ ".gf"
                                           
                                           mkSrcSpan :: (Posn, Posn) -> (Int,Int)
 					  mkSrcSpan (Pn l1 _, Pn l2 _) = (l1,l2)
diff --git a/src/GF/Grammar/Parser.y b/src/GF/Grammar/Parser.y
index c25693652..e08169a17 100644
--- a/src/GF/Grammar/Parser.y
+++ b/src/GF/Grammar/Parser.y
@@ -117,7 +117,7 @@ ModDef
                                                 Ok x    -> return x
                                                 Bad msg -> fail msg
                                       let poss  = buildTree [(i,(fname,mkSrcSpan p)) | (i,p,_) <- jments]
-                                          fname = prIdent id ++ ".gf"
+                                          fname = showIdent id ++ ".gf"
                                           
                                           mkSrcSpan :: (Posn, Posn) -> (Int,Int)
 					  mkSrcSpan (Pn l1 _, Pn l2 _) = (l1,l2)
@@ -278,7 +278,7 @@ TermDef
 
 FlagDef :: { Options }
 FlagDef
-  : Posn Ident '=' Ident Posn  {% case parseModuleOptions ["--" ++ prIdent $2 ++ "=" ++ prIdent $4] of
+  : Posn Ident '=' Ident Posn  {% case parseModuleOptions ["--" ++ showIdent $2 ++ "=" ++ showIdent $4] of
                                     Ok  x   -> return x
                                     Bad msg -> failLoc $1 msg                                           } 
 
@@ -626,7 +626,7 @@ listCatDef id pos cont size = [catd,nilfund,consfund]
     mkId x i = if isWildIdent x then (varX i) else x
 
 tryLoc (c,mty,Just e) = return (c,(mty,e))
-tryLoc (c,_  ,_     ) = fail ("local definition of" +++ prIdent c +++ "without value")
+tryLoc (c,_  ,_     ) = fail ("local definition of" +++ showIdent c +++ "without value")
 
 mkR []       = return $ RecType [] --- empty record always interpreted as record type
 mkR fs@(f:_) =
@@ -635,10 +635,10 @@ mkR fs@(f:_) =
     _                     -> mapM tryR  fs >>= return . R
   where
     tryRT (lab,Just ty,Nothing) = return (ident2label lab,ty)
-    tryRT (lab,_      ,_      ) = fail $ "illegal record type field" +++ prIdent lab --- manifest fields ?!
+    tryRT (lab,_      ,_      ) = fail $ "illegal record type field" +++ showIdent lab --- manifest fields ?!
 
     tryR (lab,mty,Just t) = return (ident2label lab,(mty,t))
-    tryR (lab,_  ,_     ) = fail $ "illegal record field" +++ prIdent lab
+    tryR (lab,_  ,_     ) = fail $ "illegal record field" +++ showIdent lab
 
 mkOverload pdt pdf@(Just df) =
   case appForm df of
@@ -660,8 +660,8 @@ mkOverload pdt pdf = [ResOper pdt pdf]
 
 isOverloading t =
   case t of
-    Vr keyw | prIdent keyw == "overload" -> True      -- overload is a "soft keyword"
-    _                                    -> False
+    Vr keyw | showIdent keyw == "overload" -> True      -- overload is a "soft keyword"
+    _                                      -> False
 
 
 type SrcSpan = (Posn,Posn)
diff --git a/src/GF/Grammar/Printer.hs b/src/GF/Grammar/Printer.hs
index 5f46d4321..e366f45d5 100644
--- a/src/GF/Grammar/Printer.hs
+++ b/src/GF/Grammar/Printer.hs
@@ -235,7 +235,7 @@ ppDDecl q (id,typ)
   | id == identW = ppTerm q 6 typ
   | otherwise    = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)
 
-ppIdent = text . prIdent
+ppIdent = text . showIdent
 
 ppQIdent q m id =
   case q of
diff --git a/src/GF/Infra/CheckM.hs b/src/GF/Infra/CheckM.hs
index ab6052a9e..f701b7c3a 100644
--- a/src/GF/Infra/CheckM.hs
+++ b/src/GF/Infra/CheckM.hs
@@ -12,33 +12,51 @@
 -- (Description of the module)
 -----------------------------------------------------------------------------
 
-module GF.Infra.CheckM (Check,
+module GF.Infra.CheckM
+          (Check, Message, runCheck,
 	       checkError, checkCond, checkWarn, checkUpdate, checkInContext,
 	       checkUpdates, checkReset, checkResets, checkGetContext, 
-	       checkLookup, checkStart, checkErr, checkVal, checkIn, 
-	       prtFail
+	       checkLookup, checkErr, checkIn, checkMap
 	      ) where
 
 import GF.Data.Operations
-import GF.Grammar.Grammar
 import GF.Infra.Ident
-import GF.Grammar.PrGrammar
+import GF.Grammar.Grammar
+import GF.Grammar.Printer
 
--- | the strings are non-fatal warnings
-type Check a = STM (Context,[String]) a
+import qualified Data.Map as Map
+import Text.PrettyPrint
 
-checkError :: String -> Check a
-checkError = raise
+type Message = Doc
+data CheckResult a
+  = Fail              [Message]
+  | Success a Context [Message]
+newtype Check a = Check {unCheck :: Context -> [Message] -> CheckResult a}
 
-checkCond :: String -> Bool -> Check ()
+instance Monad Check where
+  return x = Check (\ctxt msgs -> Success x ctxt msgs)
+  f >>= g  = Check (\ctxt msgs -> case unCheck f ctxt msgs of
+                                    Success x ctxt msgs -> unCheck (g x) ctxt msgs
+                                    Fail msgs           -> Fail msgs)
+
+instance ErrorMonad Check where
+  raise s = checkError (text s)
+  handle f h = Check (\ctxt msgs -> case unCheck f ctxt msgs of
+                                      Success x ctxt msgs -> Success x ctxt msgs
+                                      Fail (msg:msgs)     -> unCheck (h (render msg)) ctxt msgs)
+
+checkError :: Message -> Check a
+checkError msg = Check (\ctxt msgs -> Fail (msg : msgs))
+
+checkCond :: Message -> Bool -> Check ()
 checkCond s b = if b then return () else checkError s
 
 -- | warnings should be reversed in the end
-checkWarn :: String -> Check ()
-checkWarn s = updateSTM (\ (cont,msg) -> (cont, ("Warning: "++s):msg))
+checkWarn :: Message -> Check ()
+checkWarn msg = Check (\ctxt msgs -> Success () ctxt ((text "Warning:" <+> msg) : msgs))
 
 checkUpdate :: Decl -> Check ()
-checkUpdate d = updateSTM (\ (cont,msg) -> (d:cont, msg))
+checkUpdate d = Check (\ctxt msgs -> Success () (d:ctxt) msgs)
 
 checkInContext :: [Decl] -> Check r -> Check r
 checkInContext g ch = do
@@ -54,36 +72,36 @@ checkReset :: Check ()
 checkReset = checkResets 1
 
 checkResets :: Int -> Check ()
-checkResets i = updateSTM (\ (cont,msg) -> (drop i cont, msg))
+checkResets i = Check (\ctxt msgs -> Success () (drop i ctxt) msgs)
 
 checkGetContext :: Check Context
-checkGetContext = do
-  (co,_) <- readSTM
-  return co
+checkGetContext = Check (\ctxt msgs -> Success ctxt ctxt msgs)
 
 checkLookup :: Ident -> Check Type
 checkLookup x = do
   co <- checkGetContext
-  checkErr $ maybe (prtBad "unknown variable" x) return $ lookup x co
+  case lookup x co of
+    Nothing -> checkError (text "unknown variable" <+> ppIdent x)
+    Just ty -> return ty
 
-checkStart :: Check a -> Err (a,(Context,[String]))
-checkStart c = appSTM c ([],[])
+runCheck :: Check a -> Either [Message] (a,Context,[Message])
+runCheck c =
+  case unCheck c [] [] of
+    Fail msgs           -> Left          msgs
+    Success v ctxt msgs -> Right (v,ctxt,msgs)
+
+checkMap :: (Ord a) => (a -> b -> Check b) -> Map.Map a b -> Check (Map.Map a b)
+checkMap f map = do xs <- mapM (\(k,v) -> do v <- f k v
+                                             return (k,v)) (Map.toList map)
+                    return (Map.fromAscList xs)
 
 checkErr :: Err a -> Check a
-checkErr e = stm (\s -> do
-  v <- e
-  return (v,s)
-  )
+checkErr (Ok x)    = return x
+checkErr (Bad err) = checkError (text err)
 
-checkVal :: a -> Check a
-checkVal v = return v
-
-prtFail :: Print a => String -> a -> Check b
-prtFail s t = checkErr $ prtBad s t
-
-checkIn :: String -> Check a -> Check a
-checkIn msg c = stm $ \s@(g,ws) -> case appSTM c s of
-  Bad e -> Bad $ msg ++++ e
-  Ok (v,(g',ws')) -> Ok (v,(g',ws2)) where
-    new = take (length ws' - length ws) ws'
-    ws2 = [msg ++++ w | w <- new] ++ ws
+checkIn :: Doc -> Check a -> Check a
+checkIn msg c = Check $ \ctxt msgs ->
+  case unCheck c ctxt [] of
+    Fail            msgs' -> Fail ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
+    Success v ctxt' msgs' | null msgs' -> Success v ctxt' msgs
+                          | otherwise  -> Success v ctxt' ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
diff --git a/src/GF/Infra/Dependencies.hs b/src/GF/Infra/Dependencies.hs
index 43fe4f458..af2088711 100644
--- a/src/GF/Infra/Dependencies.hs
+++ b/src/GF/Infra/Dependencies.hs
@@ -18,16 +18,16 @@ prDepGraph deps = unlines $ [
   "}"
   ]
  where
-   mkNode (i,dep) = unwords [prIdent i, "[",nodeAttr (modtype dep),"]"]
+   mkNode (i,dep) = unwords [showIdent i, "[",nodeAttr (modtype dep),"]"]
    nodeAttr ty = case ty of
        MTAbstract   -> "style = \"solid\", shape = \"box\""
        MTConcrete _ -> "style = \"solid\", shape = \"ellipse\""
        _ -> "style = \"dashed\", shape = \"ellipse\""
    mkArrows (i,dep) = 
-     [unwords [prIdent i,"->",prIdent j,"[",arrowAttr "of","]"] | j <- ofs dep] ++
-     [unwords [prIdent i,"->",prIdent j,"[",arrowAttr "ex","]"] | j <- extendeds dep] ++
-     [unwords [prIdent i,"->",prIdent j,"[",arrowAttr "op","]"] | j <- openeds dep] ++
-     [unwords [prIdent i,"->",prIdent j,"[",arrowAttr "ed","]"] | j <- extrads dep]
+     [unwords [showIdent i,"->",showIdent j,"[",arrowAttr "of","]"] | j <- ofs dep] ++
+     [unwords [showIdent i,"->",showIdent j,"[",arrowAttr "ex","]"] | j <- extendeds dep] ++
+     [unwords [showIdent i,"->",showIdent j,"[",arrowAttr "op","]"] | j <- openeds dep] ++
+     [unwords [showIdent i,"->",showIdent j,"[",arrowAttr "ed","]"] | j <- extrads dep]
    arrowAttr s = case s of
      "of" -> "style = \"solid\", arrowhead = \"empty\""
      "ex" -> "style = \"solid\""
diff --git a/src/GF/Infra/Ident.hs b/src/GF/Infra/Ident.hs
index 45ebf3a5b..efe6f9261 100644
--- a/src/GF/Infra/Ident.hs
+++ b/src/GF/Infra/Ident.hs
@@ -13,7 +13,7 @@
 -----------------------------------------------------------------------------
 
 module GF.Infra.Ident (-- * Identifiers
-	      Ident(..), ident2bs, prIdent,
+	      Ident(..), ident2bs, showIdent,
 	      identC, identV, identA, identAV, identW,
 	      argIdent, varStr, varX, isWildIdent, varIndex,
 	      -- * refreshing identifiers
@@ -48,8 +48,8 @@ ident2bs i = case i of
   IAV s b j -> BS.append s (BS.pack ('_':show b ++ '_':show j))
   IW -> BS.pack "_"
 
-prIdent :: Ident -> String
-prIdent i = BS.unpack $! ident2bs i
+showIdent :: Ident -> String
+showIdent i = BS.unpack $! ident2bs i
 
 identC :: BS.ByteString -> Ident
 identV :: BS.ByteString -> Int -> Ident
diff --git a/src/GF/Infra/Modules.hs b/src/GF/Infra/Modules.hs
index 573c59ca5..0b951dd14 100644
--- a/src/GF/Infra/Modules.hs
+++ b/src/GF/Infra/Modules.hs
@@ -33,7 +33,7 @@ module GF.Infra.Modules (
 		IdentM(..),
 		abstractOfConcrete, abstractModOfConcrete,
 		lookupModule, lookupModuleType, lookupInfo,
-                lookupPosition, showPosition,
+                lookupPosition, showPosition, ppPosition,
 		isModAbs, isModRes, isModCnc, isModTrans,
 		sameMType, isCompilableModule, isCompleteModule,
 		allAbstracts, greatestAbstract, allResources,
@@ -45,7 +45,7 @@ import GF.Infra.Option
 import GF.Data.Operations
 
 import Data.List
-
+import Text.PrettyPrint
 
 -- AR 29/4/2003
 
@@ -274,6 +274,12 @@ showPosition mo i = case lookupPosition mo i of
   Ok (f,(b,e)) -> "in" +++ f ++ ", lines" +++ show b ++ "-" ++ show e
   _ -> ""
 
+ppPosition :: (Show i, Ord i) => ModInfo i a -> i -> Doc
+ppPosition mo i = case lookupPosition mo i of
+  Ok (f,(b,e)) | b == e    -> text "in" <+> text f <> text ", line" <+> int b
+               | otherwise -> text "in" <+> text f <> text ", lines" <+> int b <> text "-" <> int e
+  _ -> empty
+
 isModAbs :: ModInfo i a -> Bool
 isModAbs m = case mtype m of
   MTAbstract -> True
diff --git a/src/GF/Source/SourceToGrammar.hs b/src/GF/Source/SourceToGrammar.hs
index fc7c2b285..21d670768 100644
--- a/src/GF/Source/SourceToGrammar.hs
+++ b/src/GF/Source/SourceToGrammar.hs
@@ -205,7 +205,7 @@ buildPosTree m = buildTree . mkPoss . filter ((>0) . snd) where
     (i,p):rest@((_,q):_) -> (i,(name,(p,max p (q-1)))) : mkPoss rest
     (i,p):[]             -> (i,(name,(p,p+100))) : [] --- don't know last line
     _ -> []
-  name = prIdent m ++ ".gf" ----
+  name = showIdent m ++ ".gf" ----
 
 transAbsDef :: TopDef -> Err (Either [(Ident, Int, G.Info)] GO.Options)
 transAbsDef x = case x of
diff --git a/src/GF/Speech/VoiceXML.hs b/src/GF/Speech/VoiceXML.hs
index cf6f7120f..134964062 100644
--- a/src/GF/Speech/VoiceXML.hs
+++ b/src/GF/Speech/VoiceXML.hs
@@ -226,16 +226,16 @@ string s = "'" ++ concatMap esc s ++ "'"
 --
 
 isListCat :: (CId, [(CId, [CId])]) -> Bool
-isListCat (cat,rules) = "List" `isPrefixOf` prIdent cat && length rules == 2
+isListCat (cat,rules) = "List" `isPrefixOf` showIdent cat && length rules == 2
 		    && ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
-    where c = drop 4 (prIdent cat)
-	  fs = map (prIdent . fst) rules
+    where c = drop 4 (showIdent cat)
+	  fs = map (showIdent . fst) rules
 
 isBaseFun :: CId -> Bool
-isBaseFun f = "Base" `isPrefixOf` prIdent f
+isBaseFun f = "Base" `isPrefixOf` showIdent f
 
 isConsFun :: CId -> Bool
-isConsFun f = "Cons" `isPrefixOf` prIdent f
+isConsFun f = "Cons" `isPrefixOf` showIdent f
 
 baseSize :: (CId, [(CId, [CId])]) -> Int
 baseSize (_,rules) = length bs