content: {- |
  Module      :  ./Common/Doc.hs
  Description :  document data type Doc for (pretty) printing in various formats
  Copyright   :  (c) Christian Maeder and Uni Bremen 2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  This module contains a document data type 'Doc' for displaying
  (heterogenous) CASL specifications at least as plain text and latex
  (and maybe html as well)
  
  Inspired by John Hughes's and Simon Peyton Jones's Pretty Printer
  Combinators in Text.PrettyPrint.HughesPJ, Thomas Hallgren's
  PrettyDoc within programatica,
  Daan Leijen's PPrint: A prettier printer 2001, and Olaf Chiti's Pretty
  printing with lazy Dequeues 2003
  
  The main combinators are those of HughesPJ except
  nest, hang and $$. Instead of $$ '$+$' must be used that always forces a
  line break. Indentation must be constructed using '<>' or '<+>', i.e.
  'text' \"spec\" '<+>' MultilineBlock.
  
  Also char, ptext, int, integer, float, double and rational do not
  exist. These can all be simulated using 'text' (and 'show'). There's
  an instance for 'Int' in "Common.DocUtils".
  
  Furthermore, documents can no longer be tested with isEmpty. 'empty'
  documents are silently ignored (as by HughesPJ) and
  often it is more natural (or even necessary anyway) to test the
  original data structure for emptiness.
  
  Putting a document into braces should be done using 'specBraces' (but
  a function braces is also exported), ensuring that opening and closing
  braces are in the same column if the whole document does not fit on a
  single line.
  
  Rendering of documents is achieved by translations to the old
  "Common.Lib.Pretty". For plain text simply 'show' can be
  used. Any document can be translated to LaTeX via 'toLatex' and then
  processed further by "Common.PrintLaTeX". If you like the output is a
  different question, but the result should be legal LaTeX in
  conjunction with the hetcasl.sty file.
  
  For nicer looking LaTeX the predefined symbol constants should be
  used! There is a difference between 'bullet' and 'dot' that is not
  visible in plain text.
  
  There are also three kinds of keywords, a plain 'keyword', a
  'topSigKey' having the width of \"preds\", and a 'topKey' having the
  width of \"view\". In plain text only inserted spaces are visible.
  
  Strings in small caps are created by 'structId' and
  'indexed'. The latter puts the string also into a LaTeX index.
  
  In order to avoid considering display annotations and precedences,
  documents can be constructed using 'annoDoc', 'idDoc', and 'idApplDoc'.
  
  Currently only a few annotations (i.e. labels and %implied) are
  printed 'flushRight'. This function is problematic as it does not
  prevent something to be appended using '<>' or '<+>'. Furthermore
  flushed parts are currently only visible in plain text, if they don't
  fit on the same line (as nest is used for indenting).
  
  Further functions are documented in "Common.DocUtils".
  
  Examples can be produced using: hets -v2 -o pp.dol,pp.tex
  -}
  
  module Common.Doc
      ( -- * the document type
        Doc
      , Label (..)
      , StripComment (..)
      , renderHtml
      , renderExtHtml
      , renderText
      , renderExtText
        -- * primitive documents
      , empty
      , space
      , semi
      , comma
      , colon
      , quMarkD
      , equals
      , lparen
      , rparen
      , lbrack
      , rbrack
      , lbrace
      , rbrace
        -- * converting strings into documents
      , plainText
      , text
      , codeToken
      , commentText
      , keyword
      , topSigKey
      , topKey
      , indexed
      , structId
        -- * wrapping documents in delimiters
      , parens
      , brackets
      , braces
      , specBraces
      , quotes
      , doubleQuotes
        -- * combining documents
      -- , (<>)  -- exported via instance Semigroup Doc
      , (<+>)
      , hcat
      , hsep
      , ($+$)
      , ($++$)
      , vcat
      , vsep
      , sep
      , cat
      , fsep
      , fcat
      , punctuate
      , sepByCommas
      , sepBySemis
        -- * symbols possibly rendered differently for Text or LaTeX
      , dot
      , bullet
      , defn
      , less
      , greater
      , lambda
      , mapsto
      , funArrow
      , pfun
      , cfun
      , pcfun
      , exequal
      , forallDoc
      , exists
      , unique
      , cross
      , bar
      , notDoc
      , inDoc
      , andDoc
      , orDoc
      , implies
      , equiv
      , prefix_proc
      , sequential
      , interleave
      , synchronous
      , genpar_open
      , genpar_close
      , alpar_open
      , alpar_sep
      , alpar_close
      , external_choice
      , internal_choice
      , hiding_proc
      , ren_proc_open
      , ren_proc_close
      , dagger
      , vdash
      , dashv
      , breve
        -- * for Hybrid casl
      , prettyAt
      , prettyHere
      , prettyBind
      , prettyUniv
      , prettyExist
        -- * docifying annotations and ids
      , annoDoc
      , idDoc
      , idLabelDoc
      , predIdApplDoc
      , idApplDoc
        -- * transforming to existing formats
      , toLatex
      , toLatexAux
        -- * manipulating documents
      , flushRight
      , changeGlobalAnnos
      , rmTopKey
      , showRaw
      ) where
  
  import Common.AS_Annotation
  import Common.ConvertLiteral
  import Common.GlobalAnnotations
  import Common.Id
  import Common.IRI
  import Common.Keywords
  import Common.LaTeX_funs
  import Common.Prec
  import qualified Common.Lib.Pretty as Pretty
  
  import Data.Char
  import Data.List
  import Data.Maybe
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  infixr 6 <+>
  infixl 5 $+$
  infixl 5 $++$
  
  -- * the data type
  
  data LabelKind = IdDecl | IdAppl deriving (Show, Eq)
  
  data TextKind =
      IdKind | IdSymb | Symbol | Comment | Keyword | TopKey Int
             | Indexed | StructId | Native | HetsLabel
             | IdLabel LabelKind TextKind Id deriving Show
  
  data Format = Small | FlushRight deriving Show
  
  data ComposeKind
      = Vert   -- ($+$) (no support for $$!)
      | Horiz  -- (<>)
      | HorizOrVert -- either Horiz or Vert
      | Fill
        deriving (Eq, Show)
  
  -- | an abstract data type
  data Doc
      = Empty          -- creates an empty line if composed vertically
      | AnnoDoc Annotation -- we know how to print annotations
      | IdDoc LabelKind Id -- for plain ids outside applications
      | IdApplDoc Bool Id [Doc] -- for mixfix applications and literal terms
      | Text TextKind String -- non-empty and no white spaces inside
      | Cat ComposeKind [Doc]
      | Attr Format Doc      -- for annotations
      | ChangeGlobalAnnos (GlobalAnnos -> GlobalAnnos) Doc
  
  showRawList :: [Doc] -> String
  showRawList l = "[" ++ intercalate ", " (map showRaw l) ++ "]"
  
  showRaw :: Doc -> String
  showRaw gd =
      case gd of
        Empty -> "Empty"
        AnnoDoc an -> "AnnoDoc(" ++ show an ++ ")"
        IdDoc lk n -> "IdDoc" ++ show (lk, n)
        IdApplDoc b n l ->
          "IdApplDoc(" ++ show b ++ ", " ++ show n ++ ", " ++ showRawList l ++ ")"
        Text tk s -> "Text(" ++ show tk ++ ", " ++ s ++ ")"
        Cat ck l ->
          "Cat(" ++ show ck ++ ", " ++ showRawList l ++ ")"
        Attr fm d -> "Attr(" ++ show fm ++ ", " ++ showRaw d ++ ")"
        ChangeGlobalAnnos _ d -> "ChangeGlobalAnnos(" ++ showRaw d ++ ")"
  
  textStyle :: Pretty.Style
  textStyle = Pretty.style
    { Pretty.ribbonsPerLine = 1.19
    , Pretty.lineLength = 80 }
  
  renderText :: GlobalAnnos -> Doc -> String
  renderText = renderExtText $ StripComment False
  
  renderExtText :: StripComment -> GlobalAnnos -> Doc -> String
  renderExtText stripCs ga =
    id . Pretty.renderStyle textStyle . toText stripCs ga
  
  instance Show Doc where
      show = renderText emptyGlobalAnnos
  
  renderHtml :: GlobalAnnos -> Doc -> String
  renderHtml = renderExtHtml (StripComment False) $ MkLabel False
  
  renderExtHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> String
  renderExtHtml stripCs lbl ga = replSpacesForHtml 0
    . Pretty.renderStyle textStyle . toHtml stripCs lbl ga
  
  replSpacesForHtml :: Int -> String -> String
  replSpacesForHtml n s = case s of
    "" -> ""
    c : r -> case c of
      '\n' -> c : "<br />" ++ replSpacesForHtml 0 r
      ' ' -> replSpacesForHtml (n + 1) r
      _ -> (case n of
        0 -> (c :)
        1 -> ([' ', c] ++)
        _ -> ((' ' : concat (replicate n "&nbsp; ") ++ [c]) ++))
        $ replSpacesForHtml 0 r
  
  isEmpty :: Doc -> Bool
  isEmpty d = case d of
                Empty -> True
                Cat _ [] -> True
                _ -> False
  
  
  -- * the visible interface
  
  empty :: Doc                 -- ^ An empty document
  empty = Empty
  
  plainText :: String -> Doc
  plainText = Text IdKind
  
  text :: String -> Doc
  text s = case lines s of
      [] -> Text IdKind ""
      [x] -> Text IdKind x
      l -> vcat $ map (Text IdKind) l
  
  semi :: Doc                 -- ^ A ';' character
  semi = text ";"
  
  comma :: Doc                 -- ^ A ',' character
  comma = text ","
  
  colon :: Doc                 -- ^ A ':' character
  colon = symbol colonS
  
  -- the only legal white space within Text
  space :: Doc                 -- ^ A horizontal space (omitted at end of line)
  space = text " "
  
  equals :: Doc                 -- ^ A '=' character
  equals = symbol equalS
  
  -- use symbol for signs that need to be put in mathmode for latex
  symbol :: String -> Doc
  symbol = Text Symbol
  
  -- for text within comments
  commentText :: String -> Doc
  commentText = Text Comment
  
  -- put this string into math mode for latex and don't escape it
  native :: String -> Doc
  native = Text Native
  
  lparen, rparen, lbrack, rbrack, lbrace, rbrace, quote, doubleQuote :: Doc
  
  lparen = text "("
  rparen = text ")"
  lbrack = text "["
  rbrack = text "]"
  lbrace = symbol "{"  -- to allow for latex translations
  rbrace = symbol "}"
  quote = symbol "\'"
  doubleQuote = symbol "\""
  
  parens :: Doc -> Doc     -- ^ Wrap document in @(...)@
  parens d = hcat [lparen, d, rparen]
  
  brackets :: Doc -> Doc     -- ^ Wrap document in @[...]@
  brackets d = hcat [lbrack, d, rbrack]
  
  braces :: Doc -> Doc     -- ^ Wrap document in @{...}@
  braces d = hcat [lbrace, d, rbrace]
  
  specBraces :: Doc -> Doc     -- ^ Wrap document in @{...}@
  specBraces d = cat [addLBrace d, rbrace]
  
  -- | move the opening brace inwards
  addLBrace :: Doc -> Doc
  addLBrace d = case d of
      Cat k (e : r) -> Cat k $ addLBrace e : r
      ChangeGlobalAnnos f e -> ChangeGlobalAnnos f $ addLBrace e
      _ -> lbrace <> d
  
  quotes :: Doc -> Doc     -- ^ Wrap document in @\'...\'@
  quotes d = hcat [quote, d, quote]
  
  doubleQuotes :: Doc -> Doc     -- ^ Wrap document in @\"...\"@
  doubleQuotes d = hcat [doubleQuote, d, doubleQuote]
  
  instance Semigroup Doc where
    a <> b = hcat [a, b]
  
  rmEmpties :: [Doc] -> [Doc]
  rmEmpties = filter (not . isEmpty)
  
  hcat :: [Doc] -> Doc          -- ^List version of '<>'
  hcat = Cat Horiz . rmEmpties
  
  (<+>) :: Doc -> Doc -> Doc     -- ^Beside, separated by space
  a <+> b = hsep [a, b]
  
  punctuate :: Doc -> [Doc] -> [Doc]
  punctuate d l = case l of
       x : r@(_ : _) -> (x <> d) : punctuate d r
       _ -> l
  
  hsep :: [Doc] -> Doc         -- ^List version of '<+>'
  hsep = Cat Horiz . punctuate space . rmEmpties
  
  ($+$) :: Doc -> Doc -> Doc    -- ^Above, without dovetailing.
  a $+$ b = vcat [a, b]
  
  -- | vertical composition with a specified number of blank lines
  aboveWithNLs :: Int -> Doc -> Doc -> Doc
  aboveWithNLs n d1 d2
    | isEmpty d2 = d1
    | isEmpty d1 = d2
    | otherwise = d1 $+$ foldr ($+$) d2 (replicate n $ text "")
  
  -- | vertical composition with one blank line
  ($++$) :: Doc -> Doc -> Doc
  ($++$) = aboveWithNLs 1
  
  -- | list version of '($++$)'
  vsep :: [Doc] -> Doc
  vsep = foldr ($++$) empty
  
  vcat :: [Doc] -> Doc          -- ^List version of '$+$'
  vcat = Cat Vert . rmEmpties
  
  cat :: [Doc] -> Doc          -- ^ Either hcat or vcat
  cat = Cat HorizOrVert . rmEmpties
  
  sep :: [Doc] -> Doc          -- ^ Either hsep or vcat
  sep = Cat HorizOrVert . punctuate space . rmEmpties
  
  fcat :: [Doc] -> Doc          -- ^ \"Paragraph fill\" version of cat
  fcat = Cat Fill . rmEmpties
  
  fsep :: [Doc] -> Doc          -- ^ \"Paragraph fill\" version of sep
  fsep = Cat Fill . punctuate space . rmEmpties
  
  keyword, topSigKey, topKey, indexed, structId :: String -> Doc
  keyword = Text Keyword
  indexed = Text Indexed
  structId = Text StructId
  topKey = Text (TopKey 4)
  topSigKey = Text (TopKey 5)
  
  lambdaSymb, daggerS, vdashS, dashvS, breveS :: String
  lambdaSymb = "\\"
  daggerS = "!"
  vdashS = "|-"
  dashvS = "-|"
  breveS = "~"
  
  -- docs possibly rendered differently for Text or LaTeX
  quMarkD, dot, bullet, defn, less, greater, lambda, mapsto, funArrow, pfun,
     cfun, pcfun, exequal, forallDoc, exists, unique, cross, bar, notDoc,
     inDoc, andDoc, orDoc, implies, equiv, prefix_proc, sequential,
     interleave, synchronous, genpar_open, genpar_close, alpar_open,
     alpar_sep, alpar_close, external_choice, internal_choice, hiding_proc,
     ren_proc_open, ren_proc_close, dagger, vdash, dashv, breve, prettyAt,
     prettyHere, prettyBind, prettyUniv, prettyExist :: Doc
  
  quMarkD = text quMark
  dot = text dotS
  bullet = symbol dotS
  defn = symbol defnS
  less = symbol lessS
  greater = symbol greaterS
  lambda = symbol lambdaSymb
  mapsto = symbol mapsTo
  funArrow = symbol funS
  pfun = symbol pFun
  cfun = symbol contFun
  pcfun = symbol pContFun
  exequal = symbol exEqual
  forallDoc = symbol forallS
  exists = symbol existsS
  unique = symbol existsUnique
  cross = symbol prodS
  bar = symbol barS
  notDoc = symbol notS
  inDoc = symbol inS
  andDoc = symbol lAnd
  orDoc = symbol lOr
  implies = symbol implS
  equiv = symbol equivS
  prefix_proc = symbol prefix_procS
  sequential = text sequentialS
  interleave = symbol interleavingS
  synchronous = symbol synchronousS
  genpar_open = symbol genpar_openS
  genpar_close = symbol genpar_closeS
  alpar_open = symbol alpar_openS
  -- note that alpar_sepS and synchronousS are equal
  alpar_sep = symbol alpar_sepS
  alpar_close = symbol alpar_closeS
  external_choice = symbol external_choiceS
  internal_choice = symbol internal_choiceS
  hiding_proc = text hiding_procS -- otherwise it clashes with lambda
  ren_proc_open = symbol ren_proc_openS
  ren_proc_close = symbol ren_proc_closeS
  dagger = symbol daggerS
  vdash = symbol vdashS
  dashv = symbol dashvS
  breve = symbol breveS
  -- * for hybrid casl
  prettyAt = symbol asP
  prettyHere = symbol "Here"
  prettyBind = symbol "Bind"
  prettyUniv = symbol "Univ"
  prettyExist = symbol "Exist"
  -- | we know how to print annotations
  annoDoc :: Annotation -> Doc
  annoDoc = AnnoDoc
  
  -- | for plain ids outside of terms
  idDoc :: Id -> Doc
  idDoc = IdDoc IdAppl
  
  -- | for newly declared ids
  idLabelDoc :: Id -> Doc
  idLabelDoc = IdDoc IdDecl
  
  -- | for mixfix applications and literal terms (may print \"\" for empty)
  idApplDoc :: Id -> [Doc] -> Doc
  idApplDoc = IdApplDoc False
  
  -- | for mixfix applications of predicate identifiers
  predIdApplDoc :: Id -> [Doc] -> Doc
  predIdApplDoc = IdApplDoc True
  
  -- | put document as far to the right as fits (for annotations)
  flushRight :: Doc -> Doc
  flushRight = Attr FlushRight
  
  small :: Doc -> Doc
  small = Attr Small
  
  -- * folding stuff
  
  data DocRecord a = DocRecord
      { foldEmpty :: Doc -> a
      , foldAnnoDoc :: Doc -> Annotation -> a
      , foldIdDoc :: Doc -> LabelKind -> Id -> a
      , foldIdApplDoc :: Doc -> Bool -> Id -> [a] -> a
      , foldText :: Doc -> TextKind -> String -> a
      , foldCat :: Doc -> ComposeKind -> [a] -> a
      , foldAttr :: Doc -> Format -> a -> a
      , foldChangeGlobalAnnos :: Doc -> (GlobalAnnos -> GlobalAnnos) -> a -> a
      }
  
  foldDoc :: DocRecord a -> Doc -> a
  foldDoc r d = case d of
      Empty -> foldEmpty r d
      AnnoDoc a -> foldAnnoDoc r d a
      IdDoc l i -> foldIdDoc r d l i
      IdApplDoc b i l -> foldIdApplDoc r d b i $ map (foldDoc r) l
      Text k s -> foldText r d k s
      Cat k l -> foldCat r d k $ map (foldDoc r) l
      Attr a e -> foldAttr r d a $ foldDoc r e
      ChangeGlobalAnnos f e -> foldChangeGlobalAnnos r d f $ foldDoc r e
  
  idRecord :: DocRecord Doc
  idRecord = DocRecord
      { foldEmpty = const Empty
      , foldAnnoDoc = const AnnoDoc
      , foldIdDoc = const IdDoc
      , foldIdApplDoc = const IdApplDoc
      , foldText = const Text
      , foldCat = const Cat
      , foldAttr = const Attr
      , foldChangeGlobalAnnos = const ChangeGlobalAnnos
      }
  
  anyRecord :: DocRecord a
  anyRecord = DocRecord
      { foldEmpty = error "anyRecord.Empty"
      , foldAnnoDoc = error "anyRecord.AnnoDoc"
      , foldIdDoc = error "anyRecord.IdDoc"
      , foldIdApplDoc = error "anyRecord.IdApplDoc"
      , foldText = error "anyRecord.Text"
      , foldCat = error "anyRecord.Cat"
      , foldAttr = error "anyRecord.Attr"
      , foldChangeGlobalAnnos = error "anyRecord.ChangeGlobalAnnos"
      }
  
  newtype Label = MkLabel Bool
  
  newtype StripComment = StripComment Bool
  
  -- * conversion to plain text
  
  -- | simple conversion to a standard text document
  toText :: StripComment -> GlobalAnnos -> Doc -> Pretty.Doc
  toText stripCs ga = toTextAux . codeOut stripCs ga
    (mkPrecIntMap $ prec_annos ga) Nothing Map.empty
  
  toTextAux :: Doc -> Pretty.Doc
  toTextAux = foldDoc anyRecord
      { foldEmpty = const Pretty.empty
      , foldText = \ _ k s -> case k of
            TopKey n -> Pretty.text $ s ++ replicate (n - length s) ' '
            _ -> Pretty.text s
      , foldCat = \ d c l -> case d of
          Cat _ ds@(_ : _) -> if all hasSpace $ init ds then
            (case c of
            Vert -> Pretty.vcat
            Horiz -> Pretty.hsep
            HorizOrVert -> Pretty.sep
            Fill -> Pretty.fsep) $ map (toTextAux . rmSpace) ds
            else (case c of
            Vert -> Pretty.vcat
            Horiz -> Pretty.hcat
            HorizOrVert -> Pretty.cat
            Fill -> Pretty.fcat) l
          _ -> Pretty.empty
      , foldAttr = \ _ k d -> case k of
            FlushRight -> let l = length $ show d in
              if l < 66 then Pretty.nest (66 - l) d else d
            _ -> d
      , foldChangeGlobalAnnos = \ _ _ d -> d
      }
  
  -- * conversion to html
  
  -- | conversion to html
  toHtml :: StripComment -> Label -> GlobalAnnos -> Doc -> Pretty.Doc
  toHtml stripCs lbl ga d = let
    dm = Map.map (Map.! DF_HTML)
         . Map.filter (Map.member DF_HTML) $ display_annos ga
    dis = getDeclIds d
    in foldDoc (toHtmlRecord lbl dis) $ codeOut stripCs ga
                   (mkPrecIntMap $ prec_annos ga) (Just DF_HTML) dm d
  
  toHtmlRecord :: Label -> Set.Set Id -> DocRecord Pretty.Doc
  toHtmlRecord lbl dis = anyRecord
      { foldEmpty = const Pretty.empty
      , foldText = const $ textToHtml lbl dis
      , foldCat = \ d c l -> case d of
          Cat _ ds@(_ : _) -> if all hasSpace $ init ds then
            (case c of
            Vert -> Pretty.vcat
            Horiz -> Pretty.hsep
            HorizOrVert -> Pretty.sep
            Fill -> Pretty.fsep)
              $ map (foldDoc (toHtmlRecord lbl dis) . rmSpace) ds
            else (case c of
            Vert -> Pretty.vcat
            Horiz -> Pretty.hcat
            HorizOrVert -> Pretty.cat
            Fill -> Pretty.fcat) l
          _ -> Pretty.empty
      , foldAttr = \ a k d -> case k of
            FlushRight ->
                let Attr _ o = a
                    l = length $ show $ toTextAux o
                in if l < 66 then Pretty.nest (66 - l) d else d
            _ -> d
      , foldChangeGlobalAnnos = \ _ _ d -> d
      }
  
  textToHtml :: Label -> Set.Set Id -> TextKind -> String -> Pretty.Doc
  textToHtml lbl@(MkLabel mkLbl) dis k s = let
    e = escapeHtml s ""
    h = Pretty.text e
    zeroText = Pretty.sizedText 0
    tagB t = '<' : t ++ ">"
    tagE t = tagB $ '/' : t
    tag t d = Pretty.hcat [zeroText (tagB t), d, zeroText (tagE t) ]
    tagBold = tag "strong"
    hi = tag "em" h
   in case k of
      Native -> Pretty.text s
      Keyword -> tagBold h
      TopKey n -> let l = n - length s in
        tagBold $ h Pretty.<> Pretty.text (replicate l ' ')
      Comment -> tag "small" h
      Indexed -> hi
      StructId -> hi
      HetsLabel -> tag "small" hi
      IdLabel appl tk i -> let
          d = textToHtml lbl dis tk s
          si = escapeHtml (showId i "") ""
          in if mkLbl && Set.member i dis then Pretty.hcat
          [zeroText $ "<a " ++ (if appl == IdAppl then "href=\"#" else "name=\"")
          ++ si ++ "\">", d, zeroText "</a>"]
          else d
      _ -> h
  
  escChar :: Char -> ShowS
  escChar c = case c of
    '\'' -> showString "&#39;"
    '<' -> showString "&lt;"
    '>' -> showString "&gt;"
    '&' -> showString "&amp;"
    '"' -> showString "&quot;"
    _ -> showChar c
  
  escapeHtml :: String -> ShowS
  escapeHtml cs rs = foldr escChar rs cs
  
  -- * conversion to latex
  
  toLatex :: GlobalAnnos -> Doc -> Pretty.Doc
  toLatex = toLatexAux (StripComment False) $ MkLabel False
  
  toLatexAux :: StripComment -> Label -> GlobalAnnos -> Doc -> Pretty.Doc
  toLatexAux stripCs lbl ga d = let
    dm = Map.map (Map.! DF_LATEX) .
                        Map.filter (Map.member DF_LATEX) $ display_annos ga
    dis = getDeclIds d
      in foldDoc (toLatexRecord lbl dis False)
             . makeSmallMath False False $ codeOut stripCs ga
                   (mkPrecIntMap $ prec_annos ga) (Just DF_LATEX) dm d
  
  -- avoid too many tabs
  toLatexRecord :: Label -> Set.Set Id -> Bool -> DocRecord Pretty.Doc
  toLatexRecord lbl dis tab = anyRecord
      { foldEmpty = const Pretty.empty
      , foldText = const $ textToLatex lbl dis False
      , foldCat = \ o _ _ -> case o of
          Cat c os@(d : r)
            | any isNative os -> Pretty.hcat $
               latex_macro "{\\Ax{"
               : map (foldDoc (toLatexRecord lbl dis False)
                         { foldText = \ _ k s ->
                            case k of
                              Native -> Pretty.sizedText (axiom_width s) s
                              IdLabel _ Native _ ->
                                  Pretty.sizedText (axiom_width s) s
                              IdKind | s == " " ->
                                  Pretty.sizedText (axiom_width s) "\\,"
                              _ -> textToLatex lbl dis False k s
                          }) os
                ++ [latex_macro "}}"]
            | null r -> foldDoc (toLatexRecord lbl dis tab) d
            | otherwise -> (if tab && c /= Horiz then
                               (latex_macro setTab Pretty.<>)
                           . (latex_macro startTab Pretty.<>)
                           . (Pretty.<> latex_macro endTab)
                          else id)
                          $ (case c of
                               Vert -> Pretty.vcat
                               Horiz -> Pretty.hcat
                               HorizOrVert -> Pretty.cat
                               Fill -> Pretty.fcat)
                          $ case c of
                              Vert ->
                                map (foldDoc $ toLatexRecord lbl dis False) os
                              _ -> foldDoc (toLatexRecord lbl dis False) d :
                                map (foldDoc $ toLatexRecord lbl dis True) r
          _ -> Pretty.empty
      , foldAttr = \ o k d -> case k of
            FlushRight -> flushright d
            Small -> case o of
                Attr Small (Text j s) -> textToLatex lbl dis True j s
                _ -> makeSmallLatex True d
      , foldChangeGlobalAnnos = \ _ _ d -> d
      }
  
  -- | move a small attribute inwards but not into mathmode bits
  makeSmallMath :: Bool -> Bool -> Doc -> Doc
  makeSmallMath smll math =
      foldDoc idRecord
      { foldAttr = \ o _ _ -> case o of
                         Attr Small d -> makeSmallMath True math d
                         Attr k d -> Attr k $ makeSmallMath smll math d
                         _ -> error "makeSmallMath.foldAttr"
      , foldCat = \ o _ _ -> case o of
                    Cat c l
                      | any isNative l ->
                          (if smll then Attr Small else id)
                          -- flatten math mode bits
                             $ Cat Horiz $ map
                                   (makeSmallMath False True . rmSpace) l
                      | math -> Cat Horiz
                           $ map (makeSmallMath False True) l
                      | smll && allHoriz o ->
                      -- produce fewer small blocks with wrong size though
                               Attr Small $ Cat Horiz $
                                map (makeSmallMath False math) l
                      | otherwise -> Cat c $ map (makeSmallMath smll math) l
                    _ -> error "makeSmallMath.foldCat"
      , foldText = \ d _ _ -> if smll then Attr Small d else d
      }
  
  -- | check for unbalanced braces
  needsMathMode :: Int -> String -> Bool
  needsMathMode i s = case s of
      [] -> i > 0
      '{' : r -> needsMathMode (i + 1) r
      '}' : r -> i == 0 || needsMathMode (i - 1) r
      _ : r -> needsMathMode i r
  
  isMathLatex :: Doc -> Bool
  isMathLatex d = case d of
                 Text Native s -> needsMathMode 0 s
                 Text (IdLabel _ Native _) s -> needsMathMode 0 s
                 Attr Small f -> isMathLatex f
                 _ -> False
  
  isNative :: Doc -> Bool
  isNative d = case d of
                 Cat Horiz [t, _] -> isMathLatex t
                 _ -> isMathLatex d
  
  -- | remove the spaces inserted by punctuate
  rmSpace :: Doc -> Doc
  rmSpace = snd . anaSpace
  
  hasSpace :: Doc -> Bool
  hasSpace = fst . anaSpace
  
  anaSpace :: Doc -> (Bool, Doc)
  anaSpace d = case d of
                Cat Horiz [t, Text IdKind s] | s == " " -> (True, t)
                _ -> (False, d)
  
  allHoriz :: Doc -> Bool
  allHoriz d = case d of
                 Text _ _ -> True
                 Cat Horiz l -> all allHoriz l
                 Attr _ f -> allHoriz f
                 Empty -> True
                 _ -> False
  
  makeSmallLatex :: Bool -> Pretty.Doc -> Pretty.Doc
  makeSmallLatex b d = if b then
      Pretty.hcat [latex_macro startAnno, d, latex_macro endAnno] else d
  
  symbolToLatex :: String -> Pretty.Doc
  symbolToLatex s =
      Map.findWithDefault (hc_sty_axiom $ escapeSpecial s) s latexSymbols
  
  getDeclIds :: Doc -> Set.Set Id
  getDeclIds = foldDoc anyRecord
      { foldEmpty = const Set.empty
      , foldText = \ _ _ _ -> Set.empty
      , foldCat = \ _ _ -> Set.unions
      , foldAttr = \ _ _ d -> d
      , foldChangeGlobalAnnos = \ _ _ d -> d
      , foldIdDoc = \ _ lk i ->
            if lk == IdDecl then Set.singleton i else Set.empty
      , foldIdApplDoc = \ _ _ _ _ -> Set.empty
      , foldAnnoDoc = \ _ _ -> Set.empty
      }
  
  textToLatex :: Label -> Set.Set Id -> Bool -> TextKind -> String -> Pretty.Doc
  textToLatex lbl@(MkLabel mkLbl) dis b k s = case s of
    "" -> Pretty.text ""
    h : _ -> let e = escapeLatex s in case k of
      IdKind -> makeSmallLatex b $ if elem s $ map (: []) ",;[]() "
                then casl_normal_latex s
                else hc_sty_id e
      IdSymb -> makeSmallLatex b $ if s == "__" then symbolToLatex s
                else if isAlpha h || elem h "._'" then hc_sty_id e
                else hc_sty_axiom (escapeSpecial s)
      Symbol -> makeSmallLatex b $ symbolToLatex s
      Comment -> makeSmallLatex b $ casl_comment_latex e
                 -- multiple spaces should be replaced by \hspace
      Keyword -> (if b then makeSmallLatex b . hc_sty_small_keyword
                  else hc_sty_plain_keyword) s
      TopKey _ -> hc_sty_casl_keyword s
      Indexed -> hc_sty_structid_indexed s
      StructId -> hc_sty_structid s
      Native -> hc_sty_axiom s
      HetsLabel -> let d = textToLatex lbl dis b Comment s in
         if mkLbl then Pretty.hcat [ latex_macro "\\HetsLabel{", d
                                   , latex_macro $ "}{" ++ escapeLabel s ++ "}" ]
         else d
      -- HetsLabel may be avoided by the Label case
      IdLabel appl tk i -> let
          d = textToLatex lbl dis b tk s
          si = showId i ""
          in if b || not mkLbl || appl == IdAppl && not (Set.member i dis)
                 || not (isLegalLabel si)
             -- make this case True to avoid labels
             then d else Pretty.hcat
              [ latex_macro $ '\\' : shows appl "Label{"
              , d
              , latex_macro $ "}{" ++ escapeLabel si ++ "}" ]
  
  escapeLabel :: String -> String
  escapeLabel = map ( \ c -> if c == '_' then ':' else c)
  
  latexSymbols :: Map.Map String Pretty.Doc
  latexSymbols = Map.union (Map.fromList
      [ ("{", casl_normal_latex "\\{")
      , ("}", casl_normal_latex "\\}")
      , (barS, casl_normal_latex "\\AltBar{}")
      , (percentS, hc_sty_small_keyword "%")
      , (percents, hc_sty_small_keyword "%%")
      , (exEqual, Pretty.sizedText (axiom_width "=") "\\Ax{\\stackrel{e}{=}}") ])
      $ Map.map hc_sty_axiom $ Map.fromList
      [ (dotS, "\\bullet")
      , (diamondS, "\\Diamond")
      , ("__", "\\_\\_")
      , (lambdaSymb, "\\lambda")
      , (mapsTo, "\\mapsto")
      , (funS, "\\rightarrow")
      , (pFun, "\\rightarrow?")
      , (contFun, "\\stackrel{c}{\\rightarrow}")
      , (pContFun, "\\stackrel{c}{\\rightarrow}?")
      , (forallS, "\\forall")
      , (existsS, "\\exists")
      , (existsUnique, "\\exists!")
      , (prodS, "\\times")
      , (notS, "\\neg")
      , (inS, "\\in")
      , (lAnd, "\\wedge")
      , (lOr, "\\vee")
      , (daggerS, "\\dag")
      , (vdashS, "\\vdash")
      , (dashvS, "\\dashv")
      , (breveS, "\\breve{~}")
      , (implS, "\\Rightarrow")
      , (equivS, "\\Leftrightarrow")
      , (interleavingS, "{|}\\mkern-2mu{|}\\mkern-2mu{|}")
      , (synchronousS, "\\parallel")
      , (external_choiceS, "\\Box")
      , (internal_choiceS, "\\sqcap")
      , (ren_proc_openS, "[\\mkern-2mu{[}")
      , (ren_proc_closeS, "]\\mkern-2mu{]}")
      ]
  
  -- * coding out stuff
  
  {- | transform document according to a specific display map and other
  global annotations like precedences, associativities, and literal
  annotations. -}
  codeOut :: StripComment -> GlobalAnnos -> PrecMap -> Maybe Display_format
          -> Map.Map Id [Token] -> Doc -> Doc
  codeOut stripCs ga precs d m = foldDoc idRecord
      { foldAnnoDoc = \ _ -> small . codeOutAnno stripCs m
      , foldIdDoc = \ _ lk -> codeOutId lk m
      , foldIdApplDoc = \ o _ _ -> codeOutAppl stripCs ga precs d m o
      , foldChangeGlobalAnnos = \ o _ _ ->
            let ChangeGlobalAnnos fg e = o
                ng = fg ga
            in codeOut stripCs ng (mkPrecIntMap $ prec_annos ng) d
               (maybe m (\ f -> Map.map (Map.! f) .
                        Map.filter (Map.member f) $ display_annos ng) d) e
      }
  
  codeToken :: String -> Doc
  codeToken = Text IdSymb
  
  codeOrigId :: LabelKind -> Map.Map Id [Token] -> Id -> [Doc]
  codeOrigId lk m i@(Id ts cs _) = let
      (toks, places) = splitMixToken ts
      conv = reverse . snd . foldl ( \ (b, l) t ->
             let s = tokStr t
             in if isPlace t then (b, symbol s : l)
                else (True, (if b then codeToken s else makeLabel lk IdSymb s i)
                              : l)) (False, [])
      in if null cs then conv ts
         else conv toks ++ codeCompIds m cs : conv places
  
  cCommaT :: Map.Map Id [Token] -> [Id] -> [Doc]
  cCommaT m = punctuate comma . map (codeOutId IdAppl m)
  
  codeCompIds :: Map.Map Id [Token] -> [Id] -> Doc
  codeCompIds m = brackets . fcat . cCommaT m
  
  codeOutId :: LabelKind -> Map.Map Id [Token] -> Id -> Doc
  codeOutId lk m i = fcat $ case Map.lookup i m of
      Nothing -> codeOrigId lk m i
      Just ts -> reverse $ snd $ foldl ( \ (b, l) t ->
          let s = tokStr t
          in if isPlace t then (b, symbol s : l) else
              (True, (if b then native s else
                          makeLabel lk Native s i) : l)) (False, []) ts
  
  makeLabel :: LabelKind -> TextKind -> String -> Id -> Doc
  makeLabel l k s i = Text (IdLabel l k i) s
  
  annoLine :: String -> Doc
  annoLine w = percent <> keyword w
  
  annoLparen :: String -> Doc
  annoLparen w = percent <> keyword w <> lparen
  
  wrapLines :: TextKind -> Doc -> [String] -> Doc -> Doc
  wrapLines k a l b = let p = (null (head l), null (last l)) in
    case map (Text k) l of
      [] -> a <> b
      [x] -> hcat [a, x, b]
      [x, y] -> case p of
          (True, c) -> a $+$ if c then b else y <> b
          (False, True) -> a <> x $+$ b
          _ -> a <> (x $+$ y <> b)
      x : r -> let
        m = init r
        y = last r
        xm = x : m
        am = a : m
        yb = [y <> b]
        in case p of
          (True, c) -> vcat $ am ++ if c then [b] else yb
          (False, True) -> a <> vcat xm $+$ b
          _ -> a <> vcat (xm ++ yb)
  
  wrapAnnoLines :: Doc -> [String] -> Doc -> Doc
  wrapAnnoLines = wrapLines Comment
  
  percent :: Doc
  percent = symbol percentS
  
  annoRparen :: Doc
  annoRparen = rparen <> percent
  
  hCommaT :: Map.Map Id [Token] -> [Id] -> Doc
  hCommaT m = hsep . cCommaT m
  
  fCommaT :: Map.Map Id [Token] -> [Id] -> Doc
  fCommaT m = fsep . cCommaT m
  
  codeOutAnno :: StripComment -> Map.Map Id [Token] -> Annotation -> Doc
  codeOutAnno (StripComment stripCs) m a = case a of
      Unparsed_anno aw at _ -> if stripCs then empty else case at of
          Line_anno s -> (case aw of
              Annote_word w -> annoLine w
              Comment_start -> symbol percents) <> commentText s
          Group_anno l -> case aw of
              Annote_word w -> wrapAnnoLines (annoLparen w) l annoRparen
              Comment_start -> wrapAnnoLines (percent <> lbrace) l
                               $ rbrace <> percent
      Display_anno i ds _ -> annoLparen displayS <> fsep
          ( fcat (codeOrigId IdAppl m i) :
            map ( \ (df, s) -> percent <> commentText (lookupDisplayFormat df)
                  <+> maybe (commentText s) (const $ codeOutId IdAppl m i)
                      (Map.lookup i m)) ds) <> annoRparen
      List_anno i1 i2 i3 _ -> annoLine listS <+> hCommaT m [i1, i2, i3]
      Number_anno i _ -> annoLine numberS <+> codeOutId IdAppl m i
      Float_anno i1 i2 _ -> annoLine floatingS <+> hCommaT m [i1, i2]
      String_anno i1 i2 _ -> annoLine stringS <+> hCommaT m [i1, i2]
      Prec_anno p l1 l2 _ -> annoLparen precS <>
          fsep [ braces $ fCommaT m l1
               , case p of
                   Lower -> less
                   Higher -> greater
                   BothDirections -> less <> greater
                   NoDirection -> greater <> less
               , braces $ fCommaT m l2
               ] <> annoRparen
      Assoc_anno s l _ -> annoLparen (case s of
                            ALeft -> left_assocS
                            ARight -> right_assocS)
                          <> fCommaT m l <> annoRparen
      Label l _ -> wrapLines (case l of
                    [x] -> if isLegalLabel x then HetsLabel else Comment
                    _ -> Comment) (percent <> lparen) l annoRparen
      Prefix_anno pm _ -> annoLparen prefixS <> vcat
          (map ( \ (s, i) -> text (s ++ ":")
                  <+> text (iriToStringUnsecure $ setAngles True i)) pm)
          <> annoRparen
      Semantic_anno sa _ -> annoLine $ lookupSemanticAnno sa
  
  isLegalLabel :: String -> Bool
  isLegalLabel r = not (null r) && all ( \ c -> isAlphaNum c || elem c "_" ) r
  
  splitDoc :: Doc -> Maybe (Id, [Doc])
  splitDoc d = case d of
      IdApplDoc _ i l -> Just (i, l)
      _ -> Nothing
  
  sepByCommas :: [Doc] -> Doc
  sepByCommas = fsep . punctuate comma
  
  sepBySemis :: [Doc] -> Doc
  sepBySemis = fsep . punctuate semi
  
  data Weight = Weight Int Id Id Id -- top, left, right
  
  parenAppl :: GlobalAnnos -> PrecMap -> Doc -> [Bool] -> Doc -> [Bool]
  parenAppl ga precs origDoc l arg = case origDoc of
    IdApplDoc isPred i _ -> let
      pa = prec_annos ga
      assocs = assoc_annos ga
      mx = maxWeight precs
      pm = precMap precs
      e = Map.findWithDefault mx eqId pm
      p = Map.findWithDefault (if isInfix i then e else mx) i pm
      in case getWeight ga precs arg of
                  Nothing -> False : l
                  Just (Weight q ta la ra) ->
                      let d = isBoth pa i ta
                          oArg = (q < e || p >= e &&
                                           (notElem i [eqId, exEq]
                                           || elem ta [eqId, exEq]))
                                    && isDiffAssoc assocs pa i ta
                                  || d
                      in (if isLeftArg i l then
                       if checkArg ARight ga (i, p) (ta, q) ra
                         then oArg
                         else not (isPred || isSafeLhs i ta) || d
                      else if isRightArg i l then
                         if checkArg ALeft ga (i, p) (ta, q) la
                         then oArg
                         else (applId == i || isInfix ta)
                                  && not isPred || d
                       else d) : l
    _ -> False : l
  
  parenApplArgs :: GlobalAnnos -> PrecMap -> Doc -> [Bool]
  parenApplArgs ga precs origDoc = case origDoc of
    IdApplDoc _ _ aas -> reverse $ foldl (parenAppl ga precs origDoc) [] aas
    _ -> []
  
  -- print literal terms and mixfix applications
  codeOutAppl :: StripComment -> GlobalAnnos -> PrecMap -> Maybe Display_format
              -> Map.Map Id [Token] -> Doc -> [Doc] -> Doc
  codeOutAppl stripCs ga precs md m origDoc args = case origDoc of
    IdApplDoc _ i@(Id ts cs _) aas ->
      let mk = codeToken . tokStr
          doSplit = fromMaybe (error "doSplit") . splitDoc
          mkList op largs cl = fsep $ codeOutId IdAppl m op : punctuate comma
            (map (codeOut stripCs ga precs md m) largs)
            ++ [codeOutId IdAppl m cl]
      in if isGenNumber splitDoc ga i aas then
               mk $ toNumber doSplit i aas
           else if isGenFrac splitDoc ga i aas then
               mk $ toFrac doSplit aas
           else if isGenFloat splitDoc ga i aas then
               mk $ toFloat doSplit ga aas
           else if isGenString splitDoc ga i aas then
               mk $ toString doSplit ga i aas
           else if isGenList splitDoc ga i aas then
               toMixfixList mkList doSplit ga i aas
           else if null args || length args /= placeCount i then
               codeOutId IdAppl m i <> if null args then empty else
                                    parens (sepByCommas args)
           else let
               pars = parenApplArgs ga precs origDoc
               parArgs = zipWith (\ b -> if b then parens else id) pars args
               (fts, ncs, cFun) = case Map.lookup i m of
                              Nothing ->
                                  (fst $ splitMixToken ts, cs, IdSymb)
                              Just nts -> (nts, [], Native)
               ((_, rArgs), fArgs) = mapAccumL ( \ (b, ac) t ->
                 if isPlace t then case ac of
                   hd : tl -> ((b, tl), (False, hd))
                   _ -> error "Common.Doc.codeOutAppl1"
                   else ((True, ac), (True,
                         let s = tokStr t in
                         if b then Text cFun s else makeIdApplLabel cFun s i)))
                                                    (False, parArgs) fts
              in fsep $ hgroup $
                 (if null ncs then fArgs
                  else if null fArgs then error "Common.Doc.codeOutAppl2"
                       else init fArgs ++
                                [(True, snd (last fArgs) <> codeCompIds m cs)])
                 ++ map ( \ d -> (False, d)) rArgs
    _ -> error "Common.Doc.codeOutAppl2"
  
  hgroup :: [(Bool, Doc)] -> [Doc]
  hgroup l = case l of
    (True, d1) : (False, d2) : r -> hsep [d1, d2] : hgroup r
    (_, d) : r -> d : hgroup r
    [] -> []
  
  makeIdApplLabel :: TextKind -> String -> Id -> Doc
  makeIdApplLabel k s i = Text (IdLabel IdAppl k i) s
  
  getWeight :: GlobalAnnos -> PrecMap -> Doc -> Maybe Weight
  getWeight ga precs d = let
      m = precMap precs
      in case d of
      IdApplDoc _ i aas@(hd : _) ->
          let p = Map.findWithDefault
                (if begPlace i || endPlace i then Map.findWithDefault 0 eqId m
                 else maxWeight precs)
                i m in
          if isGenLiteral splitDoc ga i aas then Nothing else
          let pars@(par : _) = parenApplArgs ga precs d
              lw = case getWeight ga precs hd of
                     Just (Weight _ _ l _) -> nextWeight ALeft ga i l
                     Nothing -> i
              rw = case getWeight ga precs $ last aas of
                     Just (Weight _ _ _ r) -> nextWeight ARight ga i r
                     Nothing -> i
              in Just $ Weight p i (if par then i else lw)
                 $ if last pars then i else rw
      _ -> Nothing
  
  {- checkArg allows any nested infixes that are not listed in the
     precedence graph in order to report ambiguities when parsed. The
     following case require parens when printed. -}
  isDiffAssoc :: AssocMap -> PrecedenceGraph -> Id -> Id -> Bool
  isDiffAssoc assocs precs op arg = isInfix op && isInfix arg &&
              if op /= arg then
                 arg /= applId && case precRel precs op arg of
                 Lower -> False
                 _ -> True
              else not $ Map.member arg assocs
  
  -- no need for parens in the following cases
  isSafeLhs :: Id -> Id -> Bool
  isSafeLhs op arg = applId /= op &&
      (applId == arg || isPostfix arg || endPlace op && not (isInfix arg))
  
  isBoth :: PrecedenceGraph -> Id -> Id -> Bool
  isBoth precs op arg = case precRel precs op arg of
                      BothDirections -> True
                      _ -> False
  
  -- | change top-level to plain keywords
  rmTopKey :: Doc -> Doc
  rmTopKey = foldDoc idRecord
      { foldText = \ d k s -> case k of
            TopKey _ -> Text Keyword s
            _ -> d
      }
  
  -- | add global annotations for proper mixfix printing
  changeGlobalAnnos :: (GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
  changeGlobalAnnos = ChangeGlobalAnnos
  