GraphMenu.hs revision 5ee9c3b2afb91936242d34ebb8bd370b8080bcd9
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# OPTIONS -cpp #-}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederModule : $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederDescription : Menu creation functions for the Graphdisplay
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Thiemo Wiedemeyer, Uni Bremen 2002-2008
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : raider@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable (imports Logic)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ( createGraph )
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport qualified GUI.GraphAbstraction as GA
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport GUI.ShowLogicGraph(showLogicGraph)
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder#ifdef GTKGLADE
9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maederimport Data.List (isSuffixOf)
5e5d3e82af3bc2834f8718a52d9f45da80220273Dominik Lueckeimport Data.Char (toLower)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Proofs.Automatic(automatic)
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maederimport Proofs.Global(globSubsume, globDecomp)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Proofs.Local(localInference, locDecomp)
8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport Proofs.Composition(composition, compositionCreatingEdges)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederimport Proofs.HideTheoremShift(interactiveHideTheoremShift)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Proofs.TheoremHideShift(theoremHideShift)
8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport Proofs.ComputeColimit(computeColimit)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederimport Driver.ReadFn(libNameToFile)
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maederimport FileDialog(fileDialogStr, newFileDialogStr)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederimport GraphDisp(emptyArcTypeParms, emptyNodeTypeParms)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport GraphConfigure
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederimport DaVinciGraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Broadcaster(newSimpleBroadcaster,applySimpleUpdate)
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederimport Sources(toSimpleSource)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport qualified HTk
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- | A List of all linktypes and their properties. Hierarchy = Order
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian MaederlinkTypes :: HetcatsOpts
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder -> [(DGEdgeType, EdgePattern GA.EdgeValue, String, Bool, Bool)]
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian MaederlinkTypes opts = [
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder-- Name Lineformat Color Thm Other
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (GlobalDefNoInc, Solid, blackB c, False, False),
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (GlobalDefInc, Solid, blackD c, False, False),
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder (LocalDefNoInc, Dashed, blackB c, False, False),
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder (LocalDefInc, Dashed, blackD c, False, False),
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder (DefNoInc, Solid, blue1B c, False, False),
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder (DefInc, Solid, blue1D c, False, False),
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder (HidingDefNoInc, Solid, blue2B c, False, False),
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder (HidingDefInc, Solid, blue2D c, False, False),
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder (HetDefNoInc, Double, blackB c, False, False),
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (HetDefInc, Double, blackD c, False, False),
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder (ProvenThmNoInc, Solid, green1B c, True, True),
09d6f5d326545acfea43d3ffe1493c2176366475Christian Maeder (ProvenThmInc, Solid, green1D c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (UnprovenThmNoInc, Solid, coral1B c, True, True),
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder (UnprovenThmInc, Solid, coral1D c, True, True),
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder (LocalProvenThmNoInc, Dashed, green1B c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (LocalProvenThmInc, Dashed, green1D c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (LocalUnprovenThmNoInc, Dashed, coral1B c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (LocalUnprovenThmInc, Dashed, coral1D c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetProvenThmNoInc, Double, green1B c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetProvenThmInc, Double, green1D c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetUnprovenThmNoInc, Double, coral1B c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetUnprovenThmInc, Double, coral1D c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetLocalProvenThmNoInc, Double, green2B c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetLocalProvenThmInc, Double, green2D c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetLocalUnprovenThmNoInc, Double, coral2B c, True, True),
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder (HetLocalUnprovenThmInc, Double, coral2D c, True, True),
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder (UnprovenHidingThmNoInc, Solid, yellowB c, True, False),
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder (UnprovenHidingThmInc, Solid, yellowD c, True, False),
b9b331bded61b8860edacac91df16ee19e465b42Christian Maeder (ProvenHidingThmNoInc, Solid, green2B c, True, False),
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder (ProvenHidingThmInc, Solid, green2D c, True, False),
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder (ReferenceNoInc, Dotted, khakiB c, False, False),
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder (ReferenceInc, Dotted, khakiD c, False, False)]
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich c = colors opts
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder-- | A Map of all nodetypes and their properties.
8cacad2a09782249243b80985f28e9387019fe40Christian MaedermapLinkTypes :: HetcatsOpts
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder -> Map.Map DGEdgeType (EdgePattern GA.EdgeValue, String)
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian MaedermapLinkTypes opts = Map.fromList $ map (\(a, b, c, _, _) -> (a, (b,c)))
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder $ linkTypes opts
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich#ifdef GTKGLADE
797ccd67cb8ae127be097cd43448801b673e3b69Christian MaedermapLinkTypesToNames :: HetcatsOpts -> [String]
797ccd67cb8ae127be097cd43448801b673e3b69Christian MaedermapLinkTypesToNames = map (\ s -> map toLower $ take (length s - 5) s)
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder . filter (isSuffixOf "NoInc")
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder . map (\ (a, _, _, _, _) -> show a) . linkTypes
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | A List of all nodetypes and their properties.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedernodeTypes :: HetcatsOpts -> [(DGNodeType, String, Shape GA.NodeValue, String)]
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedernodeTypes opts = [
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- Name Type Shape Color
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (NotEmptyOpenConsSpec, "Spec", Ellipse, coral1D c),
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (NotEmptyProvenConsSpec, "Spec", Ellipse, coral1B c),
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (LocallyEmptyOpenConsSpec, "Spec", Ellipse, coral2D c),
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (LocallyEmptyProvenConsSpec, "Spec", Ellipse, green2B c),
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (NotEmptyOpenConsInternal, "Internal", Circle, coral1D c),
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang (NotEmptyProvenConsInternal, "Internal", Circle, coral1B c),
64d532f676706149814b58c97cd064ca5993cccfChristian Maeder (LocallyEmptyOpenConsInternal, "Internal", Circle, coral2D c),
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (LocallyEmptyProvenConsInternal, "Internal", Circle, green2B c),
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (NotEmptyDGRef, "Ref", Box, coral1D c),
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder (LocallyEmptyDGRef, "Ref", Box, green2D c)]
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder c = colors opts
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder-- | A Map of all nodetypes and their properties.
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedermapNodeTypes :: HetcatsOpts -> Map.Map DGNodeType (Shape GA.NodeValue, String)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermapNodeTypes opts = Map.fromList $ map (\(a, _, b, c) -> (a, (b,c)))
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder $ nodeTypes opts
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Creates the graph. Runs makegraph
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercreateGraph :: GInfo -> String -> ConvFunc -> LibFunc -> IO ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercreateGraph gInfo@(GInfo { gi_LIB_NAME = ln
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , gi_GraphInfo = actGraphInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , gi_hetcatsOpts = opts
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder }) title convGraph showLib = do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let file = rmSuffix (libNameToFile opts ln) ++ prfSuffix
03a6d8f77f588dc5d3dd6653797fa2362efa1751Christian Maeder (createOpen gInfo file convGraph showLib)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (createSave gInfo file)
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (createSaveAs gInfo file)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (createClose gInfo)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (Just (createExit gInfo))
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder (createGlobalMenu gInfo convGraph showLib)
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder (createNodeTypes gInfo convGraph showLib)
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder (createLinkTypes gInfo)
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder-- | Returns the open-function
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian MaedercreateOpen :: GInfo -> FilePath -> ConvFunc -> LibFunc -> Maybe (IO ())
2d130d212db7208777ca896a7ecad619a8944971Christian MaedercreateOpen gInfo file convGraph showLib = Just (
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder evnt <- fileDialogStr "Open..." file
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder maybeFilePath <- HTk.sync evnt
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder case maybeFilePath of
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder Just filePath -> do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder openProofStatus gInfo filePath convGraph showLib
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder Nothing -> fail "Could not open file."
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder-- | Returns the save-function
a9b59eb2ce961014974276cdae0e9df4419bd212Christian MaedercreateSave :: GInfo -> FilePath -> Maybe (IO ())
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedercreateSave gInfo file = Just (saveProofStatus gInfo file)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | Returns the saveas-function
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedercreateSaveAs :: GInfo -> FilePath -> Maybe (IO ())
88318aafc287e92931dceffbb943d58a9310001dChristian MaedercreateSaveAs gInfo file = Just (
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder evnt <- newFileDialogStr "Save as..." file
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder maybeFilePath <- HTk.sync evnt
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case maybeFilePath of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just filePath -> saveProofStatus gInfo filePath
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Nothing -> fail "Could not save file."
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- | Returns the save-function
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedercreateClose :: GInfo -> IO Bool
4017ebc0f692820736d796af3110c3b3018c108aChristian MaedercreateClose (GInfo { gi_LIB_NAME = ln
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder , libEnvIORef = ioRefProofStatus
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , windowCount = wc
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich , exitMVar = exit
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder le <- readIORef ioRefProofStatus
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just dgraph -> do
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder case openlock dgraph of
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder Just lock -> do
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder notopen <- isEmptyMVar lock
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder case notopen of
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder True -> error "development graph seems to be closed already"
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder False -> takeMVar lock
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> error $ "MVar of " ++ show ln ++ " not initialized"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> error $ "development graph with libname " ++ show ln
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ++" does not exist"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder count <- takeMVar wc
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder case count == 1 of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder True -> putMVar exit ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder False -> putMVar wc $ count - 1
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- | Returns the save-function
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedercreateExit :: GInfo -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedercreateExit (GInfo {exitMVar = exit}) = do
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder putMVar exit ()
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder-- | Creates the global menu
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian MaedercreateGlobalMenu :: GInfo -> ConvFunc -> LibFunc -> [GlobalMenu]
363939beade943a02b31004cea09dec34fa8a6d9Christian MaedercreateGlobalMenu gInfo@(GInfo { gi_LIB_NAME = ln
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder , gi_hetcatsOpts = opts
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder , commandHist = ch
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder }) convGraph showLib =
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder let ral x = runAndLock gInfo x in
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich [GlobalMenu (Menu Nothing
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder [ Button "Undo" $ ral $ undo gInfo True
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , Button "Redo" $ ral $ undo gInfo False
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich , Button "Reload" $ ral $ reload gInfo
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , Menu (Just "Unnamed nodes")
13731dfbb4b6a31b35dd210e832e920065b6ac45Christian Maeder [ Button "Hide/show names" $ ral $ hideShowNames gInfo True
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , Button "Hide nodes" $ ral $ hideNodes gInfo
b9b331bded61b8860edacac91df16ee19e465b42Christian Maeder , Button "Show nodes" $ ral $ showNodes gInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , Button "Focus node" $ ral $ focusNode gInfo
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder#ifdef GTKGLADE
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder , Button "Select Linktypes" $ showLinkTypeChoice (mapLinkTypesToNames opts)
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder , Menu (Just "Proofs") $ map ( \ (str, cmd) ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Button str $ (addMenuItemToHist ch str) >>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (ral $ performProofAction gInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ proofMenu gInfo $ return . return . cmd ln))
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [ ("Automatic", automatic)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , ("Global Subsumption", globSubsume)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder , ("Global Decomposition", globDecomp)
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder , ("Local Inference", localInference)
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder , ("Local Decomposition (merge of rules)", locDecomp)
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder , ("Composition (merge of rules)", composition)
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder , ("Composition - creating new links", compositionCreatingEdges)
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang [Button "Hide Theorem Shift" $
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett (addMenuItemToHist ch "Hide Theorem Shift") >>
c5f2c55174d98e1a4595e041ad4ce35a16be76fdChristian Maeder (ral $ performProofAction gInfo
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder $ proofMenu gInfo $ fmap return . interactiveHideTheoremShift ln)
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder map (\ (str, cmd) ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Button str $ (addMenuItemToHist ch str) >>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (ral $ performProofAction gInfo
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder $ proofMenu gInfo $ return . cmd ln))
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers [ ("Theorem Hide Shift", theoremHideShift)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder , ("Compute Colimit", computeColimit)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder [ Menu (Just "Flattening") $ map ( \ (str, cmd) ->
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Button str $ ral $ performProofAction gInfo
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder $ proofMenu gInfo $ return . cmd)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder [ ("Importings", libEnv_flattening2)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder , ("Disjoint unions", libEnv_flattening3)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder , ("Importings and renamings", libEnv_flattening4)
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder , ("Hiding", libEnv_flattening5)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , ("Heterogeneity", libEnv_flattening6)]]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , Button "Translate Graph" $ ral $ translateGraph gInfo convGraph showLib
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , Button "Show Logic Graph" $ ral $ showLogicGraph daVinciSort
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder , Button "Show Library Graph" $ ral $ showLibGraph gInfo showLib
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder , Button "Save Graph for uDrawGraph" $ ral
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder $ saveUDGraph gInfo (mapNodeTypes opts) $ mapLinkTypes opts
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder , Button "Save proof-script" $ ral $ askSaveProofScript gInfo
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder-- | Displays a Save-As dialog and writes the proof-script.
819e29dba060687cf391e444e0f6ff88c1908cc3Christian MaederaskSaveProofScript :: GInfo -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederaskSaveProofScript (GInfo { commandHist = ch }) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder file <- getProofScriptFileName ch
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder evnt <- newFileDialogStr "Save as..." file
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder maybeFilePath <- HTk.sync evnt
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case maybeFilePath of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just filePath -> saveCommandHistory ch filePath
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder Nothing -> fail "Could not save file."
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- | A list of all Node Types
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedercreateNodeTypes :: GInfo -> ConvFunc -> LibFunc
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> [(DGNodeType,DaVinciNodeTypeParms GA.NodeValue)]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedercreateNodeTypes gInfo@(GInfo {gi_hetcatsOpts = opts}) cGraph showLib =
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder map (\ (n, t, s, c) -> (n, menu t s c)) $ nodeTypes opts
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder "Spec" -> createLocalMenuNodeTypeSpec s c gInfo
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder "Internal" -> createLocalMenuNodeTypeInternal s c gInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "Ref" -> createLocalMenuNodeTypeDgRef s c gInfo cGraph showLib
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder _ -> error "CreateNodeTypes: Error in nodeTypes table: Type not known."
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | the link types (share strings to avoid typos)
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'ReillycreateLinkTypes :: GInfo -> [(DGEdgeType,DaVinciArcTypeParms GA.EdgeValue)]
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedercreateLinkTypes gInfo@(GInfo {gi_hetcatsOpts = opts}) =
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke map (\(title, look, color, thm, extra) ->
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder $$$ Color color
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder $$$ (if thm then createLocalEdgeMenuThmEdge gInfo
3a611630351f30bdd5b0ec4d812269b37545e5d3Dominik Luecke else createLocalEdgeMenu gInfo)
00ccf62b4570513e965eb156ab5916ec816c5d2bDominik Luecke $$$ (if extra then createLocalMenuValueTitleShowConservativity
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke $$$ emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue))
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski ) $ linkTypes opts
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- * methods to create the local menus of the different nodetypes
0b349288edfa50fdf38fda1a14e1562d03f92574Christian MaedercreateLocalMenuNode :: GInfo -> DaVinciNodeTypeParms GA.NodeValue
8c812cd83569e973f10cf69a342424ceabc07af9Christian MaedercreateLocalMenuNode gInfo = LocalMenu (Menu (Just "node menu") $ map ($ gInfo)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder [ createLocalMenuButtonShowNodeInfo
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke , createLocalMenuButtonShowTheory
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich , createLocalMenuButtonTranslateTheory
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang , createLocalMenuTaxonomy
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder , createLocalMenuButtonShowProofStatusOfNode
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder , createLocalMenuButtonProveAtNode
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich#ifdef GTKGLADE
c70ef4c3b3a62764f715510c9fd67dde3acfe454Christian Maeder , createLocalMenuButtonConsistencyChecker
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder , createLocalMenuButtonCCCAtNode ]) $$$ emptyNodeTypeParms
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- | local menu for the nodetypes spec and locallyEmpty_spec
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedercreateLocalMenuNodeTypeSpec :: Shape GA.NodeValue -> String -> GInfo
b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder -> DaVinciNodeTypeParms GA.NodeValue
18a4d5cb6828f080db9c5f9551785c5151027271Christian MaedercreateLocalMenuNodeTypeSpec shape color gInfo =
846d851fc0c2c49e949763cd3407634ba0f726c0Christian Maeder shape $$$ Color color
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder $$$ ValueTitle (\ (s,_) -> return s)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $$$ createLocalMenuNode gInfo
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- | local menu for the nodetypes internal and locallyEmpty_internal
8c812cd83569e973f10cf69a342424ceabc07af9Christian MaedercreateLocalMenuNodeTypeInternal :: Shape GA.NodeValue -> String -> GInfo
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder -> DaVinciNodeTypeParms GA.NodeValue
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedercreateLocalMenuNodeTypeInternal shape color
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder gInfo@(GInfo {internalNamesIORef = showInternalNames}) =
70731e5459a18fc473bdc962ca94d1c12de974afChristian Maeder shape $$$ Color color
edd1b7f4720bc2eea51fa0685417e1e4f3be4915Klaus Luettich $$$ ValueTitleSource (\ (s,_) -> do
7809fb14d290d257ed6d46a2dd563227e227fcf3Christian Maeder b <- newSimpleBroadcaster ""
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder intrn <- readIORef showInternalNames
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder let upd = (s,applySimpleUpdate b)
e059476130210dbb1896e753eb0a5e8c4f219f4aChristian Maeder writeIORef showInternalNames
e059476130210dbb1896e753eb0a5e8c4f219f4aChristian Maeder $ intrn {updater = upd:updater intrn}
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return $ toSimpleSource b)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder $$$ createLocalMenuNode gInfo
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- | local menu for the nodetypes dg_ref and locallyEmpty_dg_ref
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedercreateLocalMenuNodeTypeDgRef :: Shape GA.NodeValue -> String -> GInfo
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> ConvFunc -> LibFunc
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> DaVinciNodeTypeParms GA.NodeValue
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercreateLocalMenuNodeTypeDgRef shape color gInfo convGraph showLib =
8d401657e07a01e10400265f508f75353a9fba4cChristian Maeder shape $$$ Color color
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $$$ ValueTitle (\ (s,_) -> return s)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $$$ LocalMenu (Menu (Just "node menu")
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder [createLocalMenuButtonShowNodeInfo gInfo,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder createLocalMenuButtonShowTheory gInfo,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder createLocalMenuButtonShowProofStatusOfNode gInfo,
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich createLocalMenuButtonProveAtNode gInfo,
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder Button "Show referenced library"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (\ (_, descr) -> do
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder showReferencedLibrary descr gInfo convGraph showLib
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder $$$ emptyNodeTypeParms
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnketype ButtonMenu a = MenuPrim (Maybe String) (a -> IO ())
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke-- | menu button for local menus
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedercreateMenuButton :: String -> (Int -> DGraph -> IO ())
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke -> GInfo -> ButtonMenu GA.NodeValue
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedercreateMenuButton title menuFun gInfo =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (Button title
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (\ (_, descr) ->
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich do le <- readIORef $ libEnvIORef gInfo
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder let dGraph = lookupDGraph (gi_LIB_NAME gInfo) le
368c26b8ad68a4b2c42963626087667000c2eebfChristian Maeder menuFun descr dGraph
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian MaedercreateLocalMenuButtonShowTheory :: GInfo -> ButtonMenu GA.NodeValue
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian MaedercreateLocalMenuButtonShowTheory gInfo =
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski createMenuButton "Show theory" (getTheoryOfNode gInfo) gInfo
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaedercreateLocalMenuButtonTranslateTheory :: GInfo -> ButtonMenu GA.NodeValue
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaedercreateLocalMenuButtonTranslateTheory gInfo =
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder createMenuButton "Translate theory" (translateTheoryOfNode gInfo) gInfo
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder create a sub Menu for taxonomy visualisation
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder (added by KL)
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuTaxonomy :: GInfo -> ButtonMenu GA.NodeValue
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuTaxonomy ginfo@(GInfo { gi_LIB_NAME = ln
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder , libEnvIORef = le }) =
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder (Menu (Just "Taxonomy graphs")
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder [ createMenuButton "Subsort graph" (passTh displaySubsortGraph) ginfo
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder , createMenuButton "Concept graph" (passTh displayConceptGraph) ginfo
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder where passTh displayFun descr _ =
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder do r <- lookupTheoryOfNode le ln descr
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder Res.Result [] (Just (_le',n, gth)) ->
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder displayFun (showDoc n "") gth
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder -- le is the changed LibEnv, have to modify
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder Res.Result ds _ -> showDiags defaultHetcatsOpts ds
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedercreateLocalMenuButtonShowProofStatusOfNode :: GInfo -> ButtonMenu GA.NodeValue
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedercreateLocalMenuButtonShowProofStatusOfNode gInfo =
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder createMenuButton "Show proof status" (showProofStatusOfNode gInfo) gInfo
2a731d542987c87ba5ee1d8767d5cd61de8fdfc9Christian MaedercreateLocalMenuButtonProveAtNode :: GInfo -> ButtonMenu GA.NodeValue
215d42ce4d6397a453d5887292bc786e8fa9c1a2Christian MaedercreateLocalMenuButtonProveAtNode gInfo =
215d42ce4d6397a453d5887292bc786e8fa9c1a2Christian Maeder createMenuButton "Prove" (\descr dgraph -> performProofAction gInfo
215d42ce4d6397a453d5887292bc786e8fa9c1a2Christian Maeder (proveAtNode False gInfo descr dgraph)) gInfo
dc5779c9b7625d5d2fa8891c043cefc4cdfb0588Christian Maeder#ifdef GTKGLADE
dc5779c9b7625d5d2fa8891c043cefc4cdfb0588Christian MaedercreateLocalMenuButtonConsistencyChecker :: GInfo -> ButtonMenu GA.NodeValue
dc5779c9b7625d5d2fa8891c043cefc4cdfb0588Christian MaedercreateLocalMenuButtonConsistencyChecker gInfo =
dc5779c9b7625d5d2fa8891c043cefc4cdfb0588Christian Maeder createMenuButton "Consistency checker"
dc5779c9b7625d5d2fa8891c043cefc4cdfb0588Christian Maeder (\_ _ -> showConsistencyChecker gInfo) gInfo
dc5779c9b7625d5d2fa8891c043cefc4cdfb0588Christian MaedercreateLocalMenuButtonCCCAtNode :: GInfo -> ButtonMenu GA.NodeValue
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaedercreateLocalMenuButtonCCCAtNode gInfo =
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder createMenuButton "Check consistency" (proveAtNode True gInfo) gInfo
13731dfbb4b6a31b35dd210e832e920065b6ac45Christian MaedercreateLocalMenuButtonShowNodeInfo :: GInfo -> ButtonMenu GA.NodeValue
215d42ce4d6397a453d5887292bc786e8fa9c1a2Christian MaedercreateLocalMenuButtonShowNodeInfo gInfo =
215d42ce4d6397a453d5887292bc786e8fa9c1a2Christian Maeder createMenuButton "Show node info" showNodeInfo gInfo
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder-- * methods to create the local menus for the edges
ba3a7a915740c57c9cb3d2bec46b919fcba12692Christian MaedercreateLocalEdgeMenu :: GInfo -> LocalMenu GA.EdgeValue
2a731d542987c87ba5ee1d8767d5cd61de8fdfc9Christian MaedercreateLocalEdgeMenu gInfo =
ba3a7a915740c57c9cb3d2bec46b919fcba12692Christian Maeder LocalMenu (Menu (Just "edge menu")
ba3a7a915740c57c9cb3d2bec46b919fcba12692Christian Maeder [ createLocalMenuButtonShowEdgeInfo gInfo
ba3a7a915740c57c9cb3d2bec46b919fcba12692Christian Maeder , createLocalMenuButtonCheckconservativityOfEdge gInfo])
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalEdgeMenuThmEdge :: GInfo -> LocalMenu GA.EdgeValue
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalEdgeMenuThmEdge gInfo =
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder LocalMenu (Menu (Just "thm egde menu")
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder [ createLocalMenuButtonShowEdgeInfo gInfo
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder , createLocalMenuButtonCheckconservativityOfEdge gInfo])
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuButtonShowEdgeInfo :: GInfo -> ButtonMenu GA.EdgeValue
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuButtonShowEdgeInfo _ = Button "Show info"
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder (\ (_, (EdgeId descr), maybeLEdge) -> showEdgeInfo descr maybeLEdge)
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuButtonCheckconservativityOfEdge :: GInfo
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuButtonCheckconservativityOfEdge gInfo =
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder Button "Check conservativity (preliminary)"
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder (\ (_, (EdgeId descr), maybeLEdge) ->
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder checkconservativityOfEdge descr gInfo maybeLEdge)
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuValueTitleShowConservativity :: ValueTitle GA.EdgeValue
d0279930f87bf39843e0bd2992a4789322662144Christian MaedercreateLocalMenuValueTitleShowConservativity = ValueTitle
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder (\ (_, _, maybeLEdge) -> case maybeLEdge of
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder Just (_,_,edgelab) -> case dgl_type edgelab of
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder GlobalThm _ c status -> return (showCons c status)
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder LocalThm _ c status -> return (showCons c status)
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder _ -> return ""
b886e9e5db2098d0112cc4f70aeba232962939ddChristian Maeder Nothing -> return "")
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder showCons :: Conservativity -> ThmLinkStatus -> String
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder showCons c status = case (c, status) of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (None, _) -> ""
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder (_, LeftOpen) -> show c ++ "?"