GraphMenu.hs revision 53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederModule : $Header$
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederDescription : Menu creation functions for the Graphdisplay
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Jorina Freya Gerken, Till Mossakowski, Uni Bremen 2002-2006
2725abe920f91de62ae5c0b7230c1627cccf5fabChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederMaintainer : till@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : non-portable (imports Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder (createGraph)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederimport GUI.DGTranslation(getDGLogic)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederimport GUI.ShowLogicGraph(showLogicGraph)
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaederimport GUI.ShowLibGraph(showLibGraph)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport Proofs.Automatic(automatic)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport Proofs.Global(globSubsume, globDecomp)
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistimport Proofs.Local(localInference, locDecomp)
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistimport Proofs.Composition(composition, compositionCreatingEdges)
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistimport Proofs.HideTheoremShift(interactiveHideTheoremShift)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport Proofs.SimpleTheoremHideShift(theoremHideShift)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified Data.Map as Map
91e24fc45834b35f2a3830d72565640251149bf3Christian Maederimport qualified Common.InjMap as InjMap
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport Driver.ReadFn(libNameToFile)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport FileDialog(fileDialogStr, newFileDialogStr)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport GraphDisp(emptyArcTypeParms, emptyNodeTypeParms)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport GraphConfigure
0130083f314580170af1195037be3325f125fbceChristian Maederimport DaVinciGraph
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport TextDisplay(createTextDisplay)
0130083f314580170af1195037be3325f125fbceChristian Maederimport Broadcaster(newSimpleBroadcaster,applySimpleUpdate)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport Sources(toSimpleSource)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maederimport qualified HTk
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian MaederlinkTypes :: HetcatsOpts
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder -> [(String, EdgePattern EdgeValue, String, Bool, Bool)]
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian MaederlinkTypes opts = [
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder ("globaldef", Solid, black, False, False),
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder ("def", Solid, steelblue, False, False),
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder ("hidingdef", Solid, lightblue, False, False),
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder ("hetdef", GraphConfigure.Double, black, False, False),
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder ("proventhm", Solid, green, True, True),
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder ("unproventhm", Solid, coral, True, True),
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder ("localproventhm", Dashed, green, True, True),
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ("localunproventhm", Dashed, coral, True, True),
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ("hetproventhm", GraphConfigure.Double, green, True, True),
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder ("hetunproventhm", GraphConfigure.Double, coral, True, True),
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ("hetlocalproventhm", GraphConfigure.Double, green, True, True),
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder ("hetlocalunproventhm", GraphConfigure.Double, coral, True, True),
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder ("unprovenhidingthm", Solid, yellow, True, False),
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ("provenhidingthm", Solid, lightgreen, True, False),
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder -- is grey the correct color for reference?
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder ("reference", Dotted, grey, False, False)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder coral = getColor opts "Coral"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder green = getColor opts "Green"
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder steelblue = getColor opts "Steelblue"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder lightblue = getColor opts "Lightblue"
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder yellow = getColor opts "Yellow"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder lightgreen = getColor opts "Lightgreen"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder grey = getColor opts "Grey"
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder black = getColor opts "Black"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercompTableEntries :: [String]
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaedercompTableEntries = ["globaldef",
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder "unproventhm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "localproventhm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "localunproventhm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "hetproventhm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "hetunproventhm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "hetlocalproventhm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "hetlocalunproventhm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "unprovenhidingthm",
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder "provenhidingthm",
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Converts colors to grey
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergetColor :: HetcatsOpts -> String -> String
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedergetColor opts color
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder | not $ uncolored opts = color
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder | color == "Coral" = "darkgrey"
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder | color == "Green" = "lightgrey"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | color == "Steelblue" = "steelgrey"
d81905a5b924415c524d702df26204683c82c12eChristian Maeder | color == "Lightblue" = "lightsteelgrey"
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder | color == "Yellow" = "darksteelgrey"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | color == "Lightgreen" = "grey"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | otherwise = "black"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateGraph :: GInfo -> String -> ConvFunc -> IO AGV.Result
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedercreateGraph gInfo@(GInfo {libEnvIORef = ioRefProofStatus,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder gi_LIB_NAME = ln,
cb2044812811d66efe038d914966e04290be93faChristian Maeder gi_GraphInfo = actGraphInfo,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder gi_hetcatsOpts = opts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder }) title convGraph = do
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder initEnv <- readIORef ioRefProofStatus
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder iorSTEvents <- newIORef (Map.empty::(Map.Map Descr Descr))
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder let file = rmSuffix (libNameToFile opts ln) ++ prfSuffix
6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu makegraph title
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu (createOpen gInfo file convGraph)
b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu (createSave gInfo file)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu (createSaveAs gInfo file)
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder (createGlobalMenu gInfo initEnv convGraph)
966519955f5f7111abac20118563132b9dd41165Christian Maeder (createNodeTypes gInfo iorSTEvents convGraph)
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder (createLinkTypes gInfo)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (createCompTable compTableEntries)
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaedercreateOpen :: GInfo -> FilePath -> ConvFunc -> Maybe (IO ())
33fcc19ef2b59493b4e91eebf701df95fd230765Christian MaedercreateOpen gInfo file convGraph = Just (
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder evnt <- fileDialogStr "Open..." file
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder maybeFilePath <- HTk.sync evnt
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder case maybeFilePath of
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder Just filePath -> do
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder openProofStatus gInfo filePath convGraph
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder Nothing -> fail "Could not open file."
a31430de8b0632d29f42634d6395e982bf31b14dChristian MaedercreateSave :: GInfo -> FilePath -> Maybe (IO ())
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaedercreateSave gInfo file = Just (saveProofStatus gInfo file)
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaedercreateSaveAs :: GInfo -> FilePath -> Maybe (IO ())
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedercreateSaveAs gInfo file = Just (
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder evnt <- newFileDialogStr "Save as..." file
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder maybeFilePath <- HTk.sync evnt
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder case maybeFilePath of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Just filePath -> saveProofStatus gInfo filePath
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder Nothing -> fail "Could not save file."
8865728716566f42fa73e7e0bc080ba3225df764Christian MaedercreateGlobalMenu :: GInfo -> LibEnv -> ConvFunc -> [GlobalMenu]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateGlobalMenu gInfo@(GInfo {libEnvIORef = ioRefProofStatus,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder descrIORef = event,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder graphId = gid,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder gi_GraphInfo = actGraphInfo,
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder internalNamesIORef = showInternalNames,
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder gi_LIB_NAME = ln,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder gi_hetcatsOpts = opts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder }) initEnv convGraph =
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder [GlobalMenu (Menu Nothing
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder [Button "undo" (undo gInfo initEnv),
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder Button "redo" (redo gInfo initEnv),
a9e804dbec424ec36e34bab955cbe90edac5baa6Christian Maeder Button "reload" (reload gInfo),
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz Menu (Just "Unnamed nodes")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder [Button "Hide/show names"
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik Luecke (intrn::InternalNames) <- readIORef showInternalNames
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich let showThem = not $ showNames intrn
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich showItrn s = if showThem then s else ""
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich mapM_ (\(s,upd) -> upd (\_ -> showItrn s)) $ updater intrn
2353f65833a3da763392f771223250cd50b8d873Christian Maeder writeIORef showInternalNames $ intrn {showNames = showThem}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder redisplay gid actGraphInfo
2353f65833a3da763392f771223250cd50b8d873Christian Maeder Button "Hide nodes"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder AGV.Result descr msg <- hideSetOfNodeTypes gid
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ["open_cons__internal",
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "locallyEmpty__open_cons__internal",
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder "proven_cons__internal",
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder "locallyEmpty__proven_cons__internal"]
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder writeIORef event descr
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> do redisplay gid actGraphInfo
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Just err -> putStrLn err
cb2044812811d66efe038d914966e04290be93faChristian Maeder Button "Show nodes"
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder descr <- readIORef event
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showIt gid descr actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder redisplay gid actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Menu (Just "Proofs") $ map ( \ (str, cmd) ->
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder Button str (performProofAction event gid actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (proofMenu gInfo (return . return . cmd ln))
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder [ ("Automatic", automatic)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , ("Global Subsumption", globSubsume)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , ("Global Decomposition", globDecomp)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , ("Local Inference", localInference)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , ("Local Decomposition (merge of rules)", locDecomp)
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder , ("Composition (merge of rules)", composition)
966519955f5f7111abac20118563132b9dd41165Christian Maeder , ("Composition - creating new links", compositionCreatingEdges)
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder , ("Theorem Hide Shift", theoremHideShift)
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder [Button "Hide Theorem Shift"(performProofAction event gid actGraphInfo
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder (proofMenu gInfo (fmap return . interactiveHideTheoremShift ln)))
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Button "Translate Graph"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder le <- readIORef ioRefProofStatus
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder openTranslateGraph le ln opts (getDGLogic le) convGraph
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder Button "Show Logic Graph" (showLogicGraph daVinciSort),
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder Button "Show Library Graph"
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder le <- readIORef $ libEnvIORef gInfo
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder showLibGraph opts ln le $ (\ str ln2 -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (gid2, gv, _) <- convGraph gInfo ln2 le opts str
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder redisplay gid2 gv
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaedercreateNodeTypes :: GInfo -> IORef (Map.Map Descr Descr) -> ConvFunc
2360728d4185c0c04279c999941c64d36626af79Christian Maeder -> [(String,DaVinciNodeTypeParms (String,Descr,Descr))]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateNodeTypes gInfo@(GInfo {gi_hetcatsOpts = opts}) iorSTEvents convGraph =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder [("open_cons__spec", createLocalMenuNodeTypeSpec coral iorSTEvents gInfo),
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder ("proven_cons__spec", createLocalMenuNodeTypeSpec coral iorSTEvents gInfo),
2360728d4185c0c04279c999941c64d36626af79Christian Maeder ("locallyEmpty__open_cons__spec",
2360728d4185c0c04279c999941c64d36626af79Christian Maeder createLocalMenuNodeTypeSpec coral iorSTEvents gInfo),
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ("locallyEmpty__proven_cons__spec",
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder createLocalMenuNodeTypeSpec green iorSTEvents gInfo),
2360728d4185c0c04279c999941c64d36626af79Christian Maeder ("open_cons__internal", createLocalMenuNodeTypeInternal coral gInfo),
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ("proven_cons__internal", createLocalMenuNodeTypeInternal coral gInfo),
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder ("locallyEmpty__open_cons__internal",
2360728d4185c0c04279c999941c64d36626af79Christian Maeder createLocalMenuNodeTypeInternal coral gInfo),
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ("locallyEmpty__proven_cons__internal",
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder createLocalMenuNodeTypeInternal green gInfo),
2360728d4185c0c04279c999941c64d36626af79Christian Maeder ("dg_ref", createLocalMenuNodeTypeDgRef coral gInfo convGraph),
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ("locallyEmpty__dg_ref", createLocalMenuNodeTypeDgRef green gInfo convGraph)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder coral = getColor opts "Coral"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder green = getColor opts "Green"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | the link types (share strings to avoid typos)
bc263f610d20a9cd3014ddfca903026127fa0d48Christian MaedercreateLinkTypes :: GInfo -> [(String,DaVinciArcTypeParms EdgeValue)]
966519955f5f7111abac20118563132b9dd41165Christian MaedercreateLinkTypes gInfo@(GInfo {gi_hetcatsOpts = opts}) =
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder map (\(title, look, color, thm, extra) ->
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder $$$ Color color
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder $$$ (if thm then createLocalEdgeMenuThmEdge gInfo
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder else createLocalEdgeMenu gInfo)
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas $$$ (if extra then createLocalMenuValueTitleShowConservativity
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder $$$ emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder emptyArcTypeParms :: DaVinciArcTypeParms EdgeValue))
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder ) $ linkTypes opts
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder-- | Generates the CompTable
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaedercreateCompTable :: [String] -> CompTable
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian MaedercreateCompTable ls =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder concat $ map (\ x -> makeComp x ls False ) ls
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder makeComp :: String -> [String] -> Bool -> CompTable
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder makeComp _ [] _ = []
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder makeComp s (xs:r) b = case b of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder True -> (s, xs, xs) : makeComp s r b
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder False -> (s, xs, s) : makeComp s r (s == xs)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- -------------------------------------------------------------
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder-- methods to create the local menus of the different nodetypes
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder-- -------------------------------------------------------------
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maedertype NodeDescr = (String, Descr, Descr)
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder-- | local menu for the nodetypes spec and locallyEmpty_spec
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaedercreateLocalMenuNodeTypeSpec :: String -> IORef (Map.Map Descr Descr) -> GInfo
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder -> DaVinciNodeTypeParms NodeDescr
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedercreateLocalMenuNodeTypeSpec color ioRefSubtreeEvents gInfo =
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder Ellipse $$$ Color color
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder $$$ ValueTitle (\ (s,_,_) -> return s)
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder $$$ LocalMenu (Menu (Just "node menu")
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder [createLocalMenuButtonShowSignature gInfo,
cb2044812811d66efe038d914966e04290be93faChristian Maeder createLocalMenuButtonShowLocalAx gInfo,
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder createLocalMenuButtonShowTheory gInfo,
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder createLocalMenuButtonTranslateTheory gInfo,
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder createLocalMenuTaxonomy gInfo,
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder createLocalMenuButtonShowSublogic gInfo,
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder createLocalMenuButtonShowNodeOrigin gInfo,
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder createLocalMenuButtonShowProofStatusOfNode gInfo,
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder createLocalMenuButtonProveAtNode gInfo,
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder createLocalMenuButtonCCCAtNode gInfo,
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder createLocalMenuButtonShowJustSubtree ioRefSubtreeEvents
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder createLocalMenuButtonUndoShowJustSubtree
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ioRefSubtreeEvents gInfo,
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder createLocalMenuButtonShowNumberOfNode
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder $$$ emptyNodeTypeParms
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder-- | local menu for the nodetypes internal and locallyEmpty_internal
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaedercreateLocalMenuNodeTypeInternal :: String -> GInfo
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder -> DaVinciNodeTypeParms NodeDescr
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaedercreateLocalMenuNodeTypeInternal color
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder gInfo@(GInfo {internalNamesIORef = showInternalNames}) =
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder Ellipse $$$ Color color
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $$$ ValueTitleSource (\ (s,_,_) -> do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder b <- newSimpleBroadcaster ""
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder intrn <- readIORef showInternalNames
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder let upd = (s,applySimpleUpdate b)
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder writeIORef showInternalNames
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder $ intrn {updater = upd:updater intrn}
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder return $ toSimpleSource b)
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder $$$ LocalMenu (Menu (Just "node menu")
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder [createLocalMenuButtonShowSpec gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonShowNumberOfNode,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createLocalMenuButtonShowSignature gInfo,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createLocalMenuButtonShowLocalAx gInfo,
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createLocalMenuButtonShowTheory gInfo,
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder createLocalMenuButtonTranslateTheory gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuTaxonomy gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonShowSublogic gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonShowProofStatusOfNode gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonProveAtNode gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonCCCAtNode gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonShowNodeOrigin gInfo])
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $$$ emptyNodeTypeParms
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder-- | local menu for the nodetypes dg_ref and locallyEmpty_dg_ref
966519955f5f7111abac20118563132b9dd41165Christian MaedercreateLocalMenuNodeTypeDgRef :: String -> GInfo -> ConvFunc
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder -> DaVinciNodeTypeParms NodeDescr
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuNodeTypeDgRef color
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gInfo@(GInfo {nextGraphId = nextId}) convGraph =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Box $$$ Color color
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder $$$ ValueTitle (\ (s,_,_) -> return s)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder $$$ LocalMenu (Menu (Just "node menu")
cb2044812811d66efe038d914966e04290be93faChristian Maeder [createLocalMenuButtonShowSignature gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonShowTheory gInfo,
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder createLocalMenuButtonProveAtNode gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonShowProofStatusOfNode gInfo,
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder createLocalMenuButtonShowNumberOfNode,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createLocalMenuButtonShowNumberOfRefNode gInfo,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Button "Show referenced library"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (\ (_, descr, _) ->
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder do (refDescr, newGraphInfo, _) <-
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showReferencedLibrary descr gInfo convGraph
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef nextId $ refDescr +1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder redisplay refDescr newGraphInfo
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder $$$ emptyNodeTypeParms
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maedertype ButtonMenu a = MenuPrim (Maybe String) (a -> IO ())
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | menu button for local menus
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedercreateMenuButton :: String -> (Descr -> DGraphAndAGraphNode -> DGraph -> IO ())
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> GInfo -> ButtonMenu NodeDescr
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras JakubauskascreateMenuButton title menuFun gInfo =
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder (Button title
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder (\ (_, descr, _) ->
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder do convMaps <- readIORef $ conversionMapsIORef gInfo
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ps <- readIORef $ libEnvIORef gInfo
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder let dGraph = lookupDGraph (gi_LIB_NAME gInfo) ps
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder menuFun descr
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (dgAndabstrNode convMaps)
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian MaedercreateLocalMenuButtonShowSpec :: GInfo -> ButtonMenu NodeDescr
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuButtonShowSpec = createMenuButton "Show spec" showSpec
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedercreateLocalMenuButtonShowSignature :: GInfo -> ButtonMenu NodeDescr
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedercreateLocalMenuButtonShowSignature =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createMenuButton "Show signature" getSignatureOfNode
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuButtonShowTheory :: GInfo -> ButtonMenu NodeDescr
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuButtonShowTheory gInfo =
0130083f314580170af1195037be3325f125fbceChristian Maeder createMenuButton "Show theory" (getTheoryOfNode gInfo) gInfo
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaedercreateLocalMenuButtonShowLocalAx :: GInfo -> ButtonMenu NodeDescr
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuButtonShowLocalAx gInfo =
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder createMenuButton "Show local axioms" (getLocalAxOfNode gInfo) gInfo
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuButtonTranslateTheory :: GInfo -> ButtonMenu NodeDescr
bc263f610d20a9cd3014ddfca903026127fa0d48Christian MaedercreateLocalMenuButtonTranslateTheory gInfo =
966519955f5f7111abac20118563132b9dd41165Christian Maeder createMenuButton "Translate theory" (translateTheoryOfNode gInfo) gInfo
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder create a sub Menu for taxonomy visualisation
2360728d4185c0c04279c999941c64d36626af79Christian Maeder (added by KL)
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedercreateLocalMenuTaxonomy :: GInfo -> ButtonMenu NodeDescr
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuTaxonomy ginfo =
2360728d4185c0c04279c999941c64d36626af79Christian Maeder (Menu (Just "Taxonomy graphs")
2360728d4185c0c04279c999941c64d36626af79Christian Maeder [createMenuButton "Subsort graph"
2360728d4185c0c04279c999941c64d36626af79Christian Maeder (passTh displaySubsortGraph) ginfo,
2360728d4185c0c04279c999941c64d36626af79Christian Maeder createMenuButton "Concept graph"
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder (passTh displayConceptGraph) ginfo])
8994ef587ce7c7c39ddd20f0f7e4575838a6694aChristian Maeder where passTh displayFun descr ab2dgNode dgraph =
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder do r <- lookupTheoryOfNode (libEnvIORef ginfo)
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder descr ab2dgNode dgraph
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder Res.Result [] (Just (n, gth)) ->
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder displayFun (showDoc n "") gth
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder showDiags defaultHetcatsOpts ds
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuButtonShowSublogic :: GInfo -> ButtonMenu NodeDescr
2360728d4185c0c04279c999941c64d36626af79Christian MaedercreateLocalMenuButtonShowSublogic gInfo =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createMenuButton "Show sublogic"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (getSublogicOfNode $ libEnvIORef gInfo) gInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateLocalMenuButtonShowNodeOrigin :: GInfo -> ButtonMenu NodeDescr
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateLocalMenuButtonShowNodeOrigin =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createMenuButton "Show origin" showOriginOfNode
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedercreateLocalMenuButtonShowProofStatusOfNode :: GInfo -> ButtonMenu NodeDescr
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuButtonShowProofStatusOfNode gInfo =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder createMenuButton "Show proof status" (showProofStatusOfNode gInfo) gInfo
91e24fc45834b35f2a3830d72565640251149bf3Christian MaedercreateLocalMenuButtonProveAtNode :: GInfo -> ButtonMenu NodeDescr
91e24fc45834b35f2a3830d72565640251149bf3Christian MaedercreateLocalMenuButtonProveAtNode gInfo =
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder createMenuButton "Prove" (proveAtNode False gInfo) gInfo
91e24fc45834b35f2a3830d72565640251149bf3Christian MaedercreateLocalMenuButtonCCCAtNode :: GInfo -> ButtonMenu NodeDescr
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateLocalMenuButtonCCCAtNode gInfo =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder createMenuButton "Check consistency" (proveAtNode True gInfo) gInfo
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateLocalMenuButtonShowJustSubtree :: IORef (Map.Map Descr Descr)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> GInfo -> ButtonMenu NodeDescr
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuButtonShowJustSubtree ioRefSubtreeEvents
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gInfo@(GInfo {visibleNodesIORef = ioRefVisibleNodes,
2360728d4185c0c04279c999941c64d36626af79Christian Maeder gi_GraphInfo = actGraphInfo}) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (Button "Show just subtree"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (\ (_, descr, gid) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do subtreeEvents <- readIORef ioRefSubtreeEvents
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case Map.lookup descr subtreeEvents of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just _ -> putStrLn $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder "it is already just the subtree of node "
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist ++ show descr ++" shown"
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder do (eventDescr, newVisibleNodes, errorMsg) <-
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova showJustSubtree descr gid gInfo
a166da43d4e8f9dfa7a2651d033c6bea02627ca6Mihai Codescu case errorMsg of
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder Nothing -> do let newSubtreeEvents =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder subtreeEvents
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz writeIORef ioRefSubtreeEvents
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder newSubtreeEvents
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef ioRefVisibleNodes
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz newVisibleNodes
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder redisplay gid actGraphInfo
a68ff26ddb1d300f7e16097edef615f130fcd5ceChristian Maeder Just stext -> putStrLn stext
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateLocalMenuButtonUndoShowJustSubtree :: IORef (Map.Map Descr Descr)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> GInfo -> ButtonMenu NodeDescr
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuButtonUndoShowJustSubtree ioRefSubtreeEvents
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (GInfo {visibleNodesIORef = ioRefVisibleNodes,
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder gi_GraphInfo = actGraphInfo}) =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (Button "Undo show just subtree"
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist (\ (_, descr, gid) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do visibleNodes <- readIORef ioRefVisibleNodes
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz case (tail visibleNodes) of
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder [] -> do putStrLn
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova "Complete graph is already shown"
22b772f8753f0cdb4508ba460356c238de2ee375Jonathan von Schroeder newVisibleNodes@(_ : _) ->
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von Schroeder do subtreeEvents <- readIORef ioRefSubtreeEvents
f730570f7c284b252ad2e24cf23cc594021f9e25Jonathan von Schroeder case Map.lookup descr subtreeEvents of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just hide_event ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder do showIt gid hide_event actGraphInfo
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder writeIORef ioRefSubtreeEvents
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder (Map.delete descr subtreeEvents)
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz writeIORef ioRefVisibleNodes
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder newVisibleNodes
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder redisplay gid actGraphInfo
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari Nothing -> do putStrLn "undo not possible"
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder-- | for debugging
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaedercreateLocalMenuButtonShowIDOfEdge :: GInfo -> ButtonMenu EdgeValue
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaedercreateLocalMenuButtonShowIDOfEdge _ =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (Button "Show ID of this edge"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (\ (_,descr,maybeLEdge) ->
897a04683fb30873e84dc3360dea770a4435971cChristian Maeder do showIDOfEdge descr maybeLEdge
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuButtonShowNumberOfNode :: ButtonMenu NodeDescr
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuButtonShowNumberOfNode =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (Button "Show number of node"
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist (\ (_, descr, _) ->
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist getNumberOfNode descr))
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalMenuButtonShowNumberOfRefNode :: GInfo -> ButtonMenu NodeDescr
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalMenuButtonShowNumberOfRefNode =
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist createMenuButton "Show number of referenced node" getNumberOfRefNode
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistgetNumberOfRefNode :: Descr -> DGraphAndAGraphNode -> DGraph -> IO ()
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistgetNumberOfRefNode descr dgAndabstrNodeMap dgraph =
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist case InjMap.lookupWithB descr dgAndabstrNodeMap of
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist Just (_, node) ->
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist let dgnode = lab' (contextDG dgraph node)
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist title = "Number of node"
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist in createTextDisplay title (show (dgn_node dgnode)) [HTk.size(10,10)]
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist Nothing -> nodeErr descr
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist-- -------------------------------------------------------------
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist-- methods to create the local menus for the edges
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist-- -------------------------------------------------------------
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalEdgeMenu :: GInfo -> LocalMenu EdgeValue
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalEdgeMenu gInfo =
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist LocalMenu (Menu (Just "edge menu")
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist [createLocalMenuButtonShowMorphismOfEdge gInfo,
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist createLocalMenuButtonShowOriginOfEdge gInfo,
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist createLocalMenuButtonCheckconservativityOfEdge gInfo,
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist createLocalMenuButtonShowIDOfEdge gInfo]
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalEdgeMenuThmEdge :: GInfo -> LocalMenu EdgeValue
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalEdgeMenuThmEdge gInfo =
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist LocalMenu (Menu (Just "thm egde menu")
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist [ createLocalMenuButtonShowMorphismOfEdge gInfo,
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist createLocalMenuButtonShowOriginOfEdge gInfo,
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist createLocalMenuButtonShowProofStatusOfThm gInfo,
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist createLocalMenuButtonCheckconservativityOfEdge gInfo,
12324a24aa5aa42edc749c7473fcf5264d4a81e4Christian Maeder createLocalMenuButtonShowIDOfEdge gInfo]
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalMenuButtonShowMorphismOfEdge :: GInfo -> ButtonMenu EdgeValue
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistcreateLocalMenuButtonShowMorphismOfEdge _ = Button "Show morphism"
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist ( \ (_, descr, maybeLEdge) -> showMorphismOfEdge descr maybeLEdge)
7bbfb15142ab4286dfc6fcde2fc94a5512297e41Jonathan von SchroedercreateLocalMenuButtonShowOriginOfEdge :: GInfo -> ButtonMenu EdgeValue
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian MaedercreateLocalMenuButtonShowOriginOfEdge _ = Button "Show origin"
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist ( \ (_, descr, maybeLEdge) -> showOriginOfEdge descr maybeLEdge)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercreateLocalMenuButtonCheckconservativityOfEdge :: GInfo -> ButtonMenu EdgeValue
818b228955ef40dd5a253bd942dd6ab8779ed713Christian MaedercreateLocalMenuButtonCheckconservativityOfEdge gInfo =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Button "Check conservativity (preliminary)"
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian Maeder ( \ (_, descr, maybeLEdge) ->
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich checkconservativityOfEdge descr gInfo maybeLEdge)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuButtonShowProofStatusOfThm :: GInfo -> ButtonMenu EdgeValue
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedercreateLocalMenuButtonShowProofStatusOfThm _ = Button "Show proof status"
2360728d4185c0c04279c999941c64d36626af79Christian Maeder ( \ (_, descr, maybeLEdge) -> showProofStatusOfThm descr maybeLEdge)
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichcreateLocalMenuValueTitleShowConservativity :: ValueTitle EdgeValue
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian MaedercreateLocalMenuValueTitleShowConservativity = ValueTitle
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ( \ (_, _, maybeLEdge) ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case maybeLEdge of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just (_,_,edgelab) ->
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder case dgl_type edgelab of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder GlobalThm _ c status -> return (showCons c status)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder LocalThm _ c status -> return (showCons c status)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder _ -> return ""
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist Nothing -> return "")
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze showCons :: Conservativity -> ThmLinkStatus -> String
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder showCons c status =
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder case (c, status) of
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder (None, _) -> show c
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz (_, LeftOpen) -> (show c) ++ "?"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ------------------------------
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- end of local menu definitions
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- ------------------------------