PrintLaTeX.hs revision b4fbc96e05117839ca409f5f20f97b3ac872d1ed
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian Maeder Module : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian Maeder Copyright : (c) Klaus L�ttich, Christian Maeder and Uni Bremen 2002-2003
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian Maeder Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Maintainer : luettich@tzi.de
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian Maeder Stability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Portability : portable
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder This class needs to be instantiated for every datastructure in AS_*
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder for LaTeX pretty printing.
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder ( renderLatex
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , debugRenderLatex
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , PrintLaTeX(..)
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , renderLatexVerb
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder , startTab, endTab, setTab
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , setTabWithSpaces
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder , printToken_latex
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder , printDisplayToken_latex
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport Data.Char (isSpace,isAlphaNum,isDigit)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport Common.Lib.State (State(..),evalState,get,put)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport Data.List (isPrefixOf,isSuffixOf)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini----------------------------------------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- two Styles for Formatting (Standard is Style PageMode 100 1.5)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilatexStyle :: Style
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilatexStyle = textStyle { ribbonsPerLine = 1.1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , lineLength = calc_line_length "336.0pt"}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- a LatexRenderingState
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- field indentTabs : for the number of tab
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- stops set those need to be rendererd after every newline.
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- field recentlySet : number of setTab makros indentTabs is only
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- increased if recentlySet is 0
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata LRState = LRS { indentTabs :: ![Int]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , recentlySet
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , totalTabStops
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , setTabsThisLine
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , indentTabsWritten :: !Int
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , onlyTabs :: !Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , isSetLine :: !Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , collSpaceIndents :: ![Int]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , insideAnno :: Bool
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini deriving (Show)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- the initial state for using the state based rendering via LRState
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniinitialLRState :: LRState
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniinitialLRState = LRS { indentTabs = []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , recentlySet = 0
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , totalTabStops = 0
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , setTabsThisLine = 0
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , indentTabsWritten = 0
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , onlyTabs = False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , isSetLine = False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , collSpaceIndents = []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , insideAnno = False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- a function that knows how to print LaTeX TextDetails
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinilatex_txt :: TextDetails -> State LRState ShowS -> State LRState ShowS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinilatex_txt (Chr c) cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | c == '\n' = do annoBrace <- endOfLine
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini indent <- getIndent
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder return (annoBrace . showString "\\\\".
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini showChar c . indent . s)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | otherwise = do s <- cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (showChar c . s)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinilatex_txt (Str s1) cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | null s1 = cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | all isSpace s1 = do s2 <- cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (showChar ' ' . s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | otherwise = do setOnlyTabs False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (showString s1 . s2)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederlatex_txt (PStr s1) cont
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | s1 == startTab = do indent <- addTabStop
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (indent . s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s1 == endTab = do subTabStop
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s1 == setTab = do state <- get
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let (eAn,sAn) = if insideAnno state
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then (showChar '}',
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini showString startAnno)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (eAn. showString s1 . sAn. s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini s1 = do addTabWithSpaces s1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s1== startAnno = do setInsideAnno True
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (showString s1 . s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s1 == endAnno = do setInsideAnno False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (showChar '}' . s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s1 == "\n" = do annoBrace <- endOfLine
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini indent <- getIndent
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (annoBrace . showString "\\\\\n" .
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini s1 = do indent <- getIndent
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (showString s1 .
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | otherwise = do setOnlyTabs False
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (showString s1 . s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- a function that knows how to print LaTeX TextDetails
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidebug_latex_txt :: TextDetails -> State LRState String -> State LRState String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidebug_latex_txt (Chr c) cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | c == '\n' = do state <- get
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini annoBrace <- endOfLine
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini indent <- getIndent
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (annoBrace "\\\\%"++show (state::LRState)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++c:(indent s))
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder | otherwise = do s <- cont
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederdebug_latex_txt (Str s1) cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | null s1 = cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | all isSpace s1 = do s2 <- cont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return ( ' ':s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | otherwise = do setOnlyTabs False
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini return (s1 ++ s2)
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrinidebug_latex_txt (PStr s1) cont
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini | s1 == startTab = do indent <- addTabStop
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder return (s1 ++ indent s2)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder | s1 == endTab = do subTabStop
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder return (s1 ++ s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s1 == setTab = do state <- get
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let (eAn,sAn) = if insideAnno state
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then (showChar '}',
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini showString startAnno)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (eAn s1 ++ sAn s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini s1 = do addTabWithSpaces s1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (s1 ++ s2)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini | s1== startAnno = do setInsideAnno True
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return (s1 ++ s2)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini | s1 == endAnno = do setInsideAnno False
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return ('}' : s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | s1 == "\n" = do state <- get
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini annoBrace <- endOfLine
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini indent <- getIndent
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return (annoBrace "\\\\%"++show (state::LRState)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ++s1++indent s2)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini | otherwise = do setOnlyTabs False
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini return (s1 ++ s2)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetOnlyTabs :: Bool -> State LRState ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetOnlyTabs b = do state <- get
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini put $ state {onlyTabs = b}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetInsideAnno :: Bool -> State LRState ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetInsideAnno b = do state <- get
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini put $ state {insideAnno = b}
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- a function to produce a String containing the actual tab stops in use
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinigetIndent :: State LRState ShowS
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinigetIndent = do state <- get
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini let indentTabsSum = foldl (+) 0 (indentTabs state)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini put $ state { indentTabsWritten = indentTabsSum
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , collSpaceIndents = []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , onlyTabs = True
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , totalTabStops = max (totalTabStops state)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (indentTabsSum +
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (collSpaceIndents state))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let indent_fun = foldl (.) id (replicate indentTabsSum
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (showString "\\>"))
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini new_tab_line = foldl space_format id
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (collSpaceIndents state)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini . showString "\\kill\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sAnno = (if insideAnno state
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then showString startAnno
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return ( (if null (collSpaceIndents state) then
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini indent_fun . new_tab_line . indent_fun)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder where space_format :: (ShowS) -> Int -> ShowS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini space_format sf1 i = sf1 . showString (replicate i '~')
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder . showString "\\="
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniendOfLine :: State LRState ShowS
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederendOfLine = do state <- get
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder put $ state { isSetLine = False
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , setTabsThisLine = 0
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder return (if insideAnno state then showChar '}' else id)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetTabStop :: State LRState ()
603e326e7b189de8c1e4ea8c89470b3a61154019Christian MaedersetTabStop = State (\state -> ( ()
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , let new_setTabsThisLine =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder succ $ setTabsThisLine state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder recentlySet = succ $ recentlySet state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , setTabsThisLine = new_setTabsThisLine
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , totalTabStops =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder max (totalTabStops state)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (new_setTabsThisLine +
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini indentTabsWritten state)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , isSetLine = True}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniaddTabWithSpaces :: String -> State LRState ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniaddTabWithSpaces s = let delayed_indent :: Int
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder delayed_indent =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder (read . reverse . fst
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder . span isDigit . tail . reverse) s
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder in State (\state -> ( ()
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder , state { collSpaceIndents =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder collSpaceIndents state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder ++ [delayed_indent]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- increase the indentTabs in the state by 1
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederaddTabStop :: State LRState ShowS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniaddTabStop = State (\state -> let (new_indentTabs,newTabs) =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder let nT = if isSetLine state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder then recentlySet state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder in (condAdd_indentTabs nT, nT)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder indentTabsSum = foldl (+) 0
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini condAdd_indentTabs i =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder if i + indentTabsSum
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (indentTabs state)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder totalTabStops state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder then indentTabs state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder else indentTabs state ++ [i]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini new_recentlySet =
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder if isSetLine state
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else recentlySet state
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder inTabs nT = foldl (.) id
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (replicate nT $ showString "\\>")
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder new_indentTabsWritten) =
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder if indentTabsSum
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder new_indentTabs
a2e8cca8a8217b158b0b7a760e8234c03186456dChristian Maeder indentTabsWritten state
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder && not (isSetLine state)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder && onlyTabs state
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder then (inTabs newTabs,
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder indentTabsWritten state)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini indentTabsWritten state)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in (indent_fun
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ,state { recentlySet = new_recentlySet
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , indentTabs = new_indentTabs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , indentTabsWritten =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini new_indentTabsWritten
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- decrease the indentTabs in the state by 1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisubTabStop :: State LRState ()
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisubTabStop = do state <- get
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let l_itabs = last itabs
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder itabs = indentTabs state
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder indentTabs' = if null $ indentTabs state
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else if l_itabs == 1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then init itabs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else init itabs -- ++ [l_itabs -1]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini put (state {indentTabs = indentTabs'})
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder-- a constant String for starting a LaTeX indentation with tab stop
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederstartTab :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinistartTab = "\\@begT@"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- a constant String for releasing a LaTeX indentation with tab stop
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniendTab :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniendTab = "\\@endT@"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- a constant String to set a tab stop and enable it
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetTab :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetTab = "\\="
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | a constant String indicating the start of a space based indentation
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetTabWSp :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetTabWSp = "\\@setTS@{"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | function to set up a space based indentation macro
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetTabWithSpaces :: Int -> String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisetTabWithSpaces i = (showString setTabWSp . shows i) "}"
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder-- functions for producing IO printable Strings
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinirenderLatex, renderLatexVerb :: Maybe Int -> Doc -> String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinirenderLatex mi d = ((showString "\\begin{hetcasl}\n") .
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder (evalState (fullRender (mode latexStyle')
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder (lineLength latexStyle')
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (ribbonsPerLine latexStyle')
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini initialLRState)) "\n\\end{hetcasl}\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini where -- d' = ptext "\\begin{hetcasl}" $+$ d $+$ ptext "\\end{hetcasl}"
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder latexStyle' = latexStyle {lineLength =
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder Nothing -> lineLength latexStyle
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder Just l -> l) }
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidebugRenderLatex :: Maybe Int -> Doc -> String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidebugRenderLatex mi d = evalState (fullRender (mode latexStyle')
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder (lineLength latexStyle')
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder (ribbonsPerLine latexStyle')
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini debug_latex_txt
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini initialLRState
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini where d' = ptext "\\begin{hetcasl}" $+$ d $+$ ptext "\\end{hetcasl}"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini latexStyle' = latexStyle {lineLength =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Nothing -> lineLength latexStyle
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder Just l -> l) }
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder-- this lacks some environment starting and closing LaTeX commands
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinirenderLatexVerb mi d = renderStyle textStyle' d'
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini where d' = text "\\begin{verbatim}" $+$ d $+$ text "\\end{verbatim}"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini textStyle' = textStyle {lineLength =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Nothing -> lineLength textStyle
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just l -> l) }
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- moved instance from Id.hs (to avoid cyclic imports via GlobalAnnotations)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniinstance PrintLaTeX Token where
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini printLatex0 ga t = printToken_latex casl_axiom_latex t'
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini where i = Id [t] [] []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini t' = maybe t (\ ts -> if isMixfix (Id ts [] [])
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini else head ts)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini (lookupDisplay ga DF_LATEX i)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniisLaTeXmacro :: String -> Bool
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniisLaTeXmacro s = or ['\\' `elem` s,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini '^' `elem` s,
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini '_' `elem` s]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprintToken_latex :: (String -> Doc) -> Token -> Doc
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprintToken_latex strConvDoc_fun t =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let s = tokStr t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini esc = escape_latex s
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in if s `elem` map (:[]) "[](),;"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then strConvDoc_fun s
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini else if isPlace t || s `elem` map (:[]) "{}"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then strConvDoc_fun esc
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else if all isAlphaNum s
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini || ('\\' `elem` esc && not ('\\' `elem` s)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini && not ('~' `elem` s))
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini then (\x -> latex_macro "\\Id{"<>x<>latex_macro "}")
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini $ strConvDoc_fun esc
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini else (\x -> latex_macro "\\Ax{"<>x<>latex_macro "}")
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini $ strConvDoc_fun s
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederprintDisplayToken_latex :: (String -> Doc) -> Token -> Doc
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniprintDisplayToken_latex strConvDoc_fun t =
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini if isLaTeXmacro str && not (isPlace t)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini then latex_macro "\\Ax{"<>strConvDoc_fun str<>latex_macro "}"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini else printToken_latex strConvDoc_fun t
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini where str = tokStr t
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maederinstance PrintLaTeX Id where
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini printLatex0 ga i = printId printLatex0 ga (Just DF_LATEX)
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder (hcat . map (printDisplayToken_latex casl_axiom_latex)) i