/*
** Program: Clean Prover System
** Module:  FormattedShow (.dcl)
** 
** Author:  Maarten de Mol
** Created: 22 August 2000
*/

definition module 
	FormattedShow

import 
	StdEnv,
	MarkUpText,
	CoreTypes,
	CoreAccess,
	Operate,
	Heaps

// -------------------------------------------------------------------------------------------------------------------------------------------------
LogicColour		:== RGB {r=  0, g=150, b= 75}				// fg; quantors + logical connectives
LogicDarkColour	:== RGB {r=  0, g=100, b= 25}
Brown			:== RGB {r=180, g=130, b=100}
DarkBrown		:== RGB {r=150, g=110, b= 70}
// -------------------------------------------------------------------------------------------------------------------------------------------------

// -------------------------------------------------------------------------------------------------------------------------------------------------
:: DisplayOptions =
// -------------------------------------------------------------------------------------------------------------------------------------------------
	{ optShowRecordFuns				:: !Bool
	, optShowRecordCreation			:: !Bool
	, optShowArrayFuns				:: !Bool
	, optShowTupleFuns				:: !Bool
	, optShowDictionaries			:: !Bool
	, optShowInstanceTypes			:: !Bool
	, optShowVariableIndexes		:: !Bool
	, optShowPatterns				:: !Bool
	, optShowLetsAndCases			:: !Bool
	, optShowSharing				:: !Bool
	, optAlwaysBrackets				:: !Bool
	, optShowIsTrue					:: !Bool
	, optExtendedForalls			:: !Bool

	, optDefinitionWindowBG			:: !ExtendedColour
	, optDefinitionListWindowBG		:: !ExtendedColour
	, optHintWindowBG				:: !ExtendedColour
	, optProjectCenterBG			:: !ExtendedColour
	, optProofWindowBG				:: !ExtendedColour
	, optSectionCenterBG			:: !ExtendedColour
	, optTacticDialogBG				:: !ExtendedColour
	, optTacticListBG				:: !ExtendedColour
	, optTheoremWindowBG			:: !ExtendedColour
	, optTheoremListWindowBG		:: !ExtendedColour
	
	, optStartWithAboutDialog		:: !Bool
	}
instance DummyValue DisplayOptions

// -------------------------------------------------------------------------------------------------------------------------------------------------
:: DisplaySpecial =
// -------------------------------------------------------------------------------------------------------------------------------------------------
	{ disForall						:: Bool -> (MarkUpText HeapPtr) -> (MarkUpText HeapPtr)
	, disExists						:: Bool -> (MarkUpText HeapPtr) -> (MarkUpText HeapPtr)
	, disAnd						:: (MarkUpText HeapPtr) -> (MarkUpText HeapPtr) -> (MarkUpText HeapPtr)
	, disOr							:: (MarkUpText HeapPtr) -> (MarkUpText HeapPtr) -> (MarkUpText HeapPtr)
	, disNot						:: (MarkUpText HeapPtr) -> (MarkUpText HeapPtr)
	, disImplies					:: Bool -> (MarkUpText HeapPtr) -> (MarkUpText HeapPtr) -> (MarkUpText HeapPtr)
	, disIff						:: (MarkUpText HeapPtr) -> (MarkUpText HeapPtr) -> (MarkUpText HeapPtr)
	, disBottom						:: MarkUpText HeapPtr
	, disIsSpecial					:: !Bool
	}
instance DummyValue DisplaySpecial
toColour :: !Int !ExtendedColour -> Colour

// ------------------------------------------------------------------------------------------------------------------------   
:: ExtendedColour =
// ------------------------------------------------------------------------------------------------------------------------   
	{ exRed					:: !Int
	, exGreen				:: !Int
	, exBlue				:: !Int
	, exHue					:: !Int
	, exLum					:: !Int
	, exSat					:: !Int
	}
instance DummyValue ExtendedColour
instance == ExtendedColour

// -------------------------------------------------------------------------------------------------------------------------------------------------
:: PropPosition =
// -------------------------------------------------------------------------------------------------------------------------------------------------
	  LeftOfAnd
	| RightOfAnd
	| LeftOfOr
	| RightOfOr
	| LeftOfImplies
	| RightOfImplies
	| LeftOfIff
	| RightOfIff
instance == PropPosition

// -------------------------------------------------------------------------------------------------------------------------------------------------
:: FormatInfo =
// -------------------------------------------------------------------------------------------------------------------------------------------------
	{	fiNeedBrackets				:: !Bool
	,	fiPreviousPriority			:: !Maybe !Int
	,	fiPreviousApplicationPtr	:: !Maybe HeapPtr
	,	fiPosition					:: !Maybe PropPosition
	,	fiOverrideNoBrackets		:: !Bool
	,	fiIsPattern					:: !Bool
	,	fiHeadPtr					:: !HeapPtr
	,	fiPassed					:: ![CSharedPtr]
	,	fiSpecial					:: !DisplaySpecial
	,	fiOptions					:: !DisplayOptions
	,	fiNextVarNum				:: !Int
	,	fiIndentQuantors			:: !Bool
	,	fiBigIndentSkip				:: !Bool
	,	fiIndentImplies				:: !Bool
	,	fiIndentEqual				:: !Bool
	,	fiPrettyTypes				:: ![CTypeH]						// used in AnnotatedShow
	}
instance DummyValue FormatInfo

changeColour		:: !Int !Colour -> Colour

storeExprVar		:: !CExprVarPtr !FormatInfo !*CHeaps -> (!FormatInfo, !*CHeaps)
storeExprVars		:: ![CExprVarPtr] !FormatInfo !*CHeaps -> (!FormatInfo, !*CHeaps)
storePropVar		:: !CPropVarPtr !FormatInfo !*CHeaps -> (!FormatInfo, !*CHeaps)
storePropVars		:: ![CPropVarPtr] !FormatInfo !*CHeaps -> (!FormatInfo, !*CHeaps)

ShowExprVar			:: !FormatInfo !Bool !CExprVarPtr !*CHeaps !*CProject -> (!Error, !MarkUpText HeapPtr, !*CHeaps, !*CProject)
ShowPropVar			:: !FormatInfo !Bool !CPropVarPtr !*CHeaps -> (!MarkUpText HeapPtr, !*CHeaps)

class FormattedShow cdef :: !FormatInfo !cdef !*CHeaps !*CProject -> (!Error, !MarkUpText !HeapPtr, !*CHeaps, !*CProject)

instance FormattedShow (CAlgPattern HeapPtr)
instance FormattedShow (CAlgTypeDef HeapPtr)
instance FormattedShow (CBasicPattern HeapPtr)
instance FormattedShow CBasicType
instance FormattedShow (CBasicValue HeapPtr)
instance FormattedShow (CCasePatterns HeapPtr)
instance FormattedShow (CClassDef HeapPtr)
instance FormattedShow (CClassRestriction HeapPtr)
instance FormattedShow (CDataConsDef HeapPtr)
instance FormattedShow (CExpr HeapPtr)
instance FormattedShow (CFunDef HeapPtr)
instance FormattedShow CInfix 
instance FormattedShow (CInstanceDef HeapPtr)
instance FormattedShow (CMemberDef HeapPtr)
instance FormattedShow (CProp HeapPtr)
instance FormattedShow (CRecordFieldDef HeapPtr)
instance FormattedShow (CRecordTypeDef HeapPtr)
instance FormattedShow (CSymbolType HeapPtr)
instance FormattedShow (CType HeapPtr)
instance FormattedShow TacticId

formattedShow :: !HeapPtr !FormatInfo !*CHeaps !*CProject -> (!Error, !MarkUpText HeapPtr, !*CHeaps, !*CProject)








:: Icon =
	  ApplyIcon
	| InfoIcon
	| HelpIcon
	| MoveIcon
	| ProveIcon
	| RecycleIcon
	| RenameIcon
	| RemoveIcon
	| SaveIcon
	| ViewContentsIcon

:: IconInfo item a =
	{ iiIcon				:: !Icon
	, iiLinkStyle			:: !Int
	, iiCommand				:: !(Ptr item) -> a
	}

IconSymbol			:: !Icon -> (!CName, !Int)
showIconList		:: ![Ptr item] ![IconInfo item a] !((Ptr item) -> item -> MarkUpText a) ![IconInfo item a] !*CHeaps -> (!MarkUpText a, !*CHeaps) | Pointer item
showIconList1		:: ![Ptr item] ![IconInfo item a] !((Ptr item) -> item -> MarkUpText a) ![IconInfo item a] !Colour !*CHeaps -> (!MarkUpText a, !*CHeaps) | Pointer item
