46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederDescription : xml output of Hets development graphs
46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederCopyright : (c) Ewaryst Schulz, Uni Bremen 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederMaintainer : Ewaryst.Schulz@dfki.de
46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederStability : provisional
46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederPortability : non-portable(Grothendieck)
46b207daf66b64930a59f3615c8b127aac0b8e43Christian MaederXml of Hets DGs
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder , showSymbols
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder , showSymbolsTh
486db0a875bcdd0b80cf0d447d14c9c00a92ae94Simon Ulbrichtimport Static.ComputeTheory (getImportNames)
863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maederimport qualified Common.OrderedMap as OMap
46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport qualified Data.Map as Map
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbrichtimport qualified Data.Set as Set (toList)
599f7489a5c8feeeebb6d63ddacf72443bb49adeTill Mossakowskiimport Data.Char (toLower)
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian MaederExport the development graph as xml. If the flag full is True then
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maedersymbols for all nodes are shown as declarations, otherwise (the
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maederdefault) only declaration for basic spec nodes are shown that are
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maedersufficient to reconstruct the development from the xml output. -}
034d9e2e9ada5aaa5665180720744d51166dacd4Christian MaederdGraph :: HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksadGraph opts lenv ln dg =
3ddbdc6f84dbf9a59e178575db8359d3aab1dd2fChristian Maeder let body = dgBody dg
46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder ga = globalAnnos dg
46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maeder lnodes = labNodes body
ac915973c15ca69c94cb2eaa3321c9e9d04e44e0Christian Maeder ledges = labEdges body
f318d03bd3eb55a9edfae36ffdc28737b71b4df5Simon Ulbricht in add_attrs [ mkAttr "filename" $ getFilePath ln
ab53b2d1773ac020b0df4cc9edeb0debe12e7a09cmaeder , mkAttr "mime-type" . fromMaybe "unknown" $ mimeType ln
01ddc4cad68fa84b4e9dd41089ad876329bae5b0Christian Maeder , mkAttr "libname" . show $ setAngles False $ getLibId ln
ac915973c15ca69c94cb2eaa3321c9e9d04e44e0Christian Maeder , mkAttr "dgnodes" . show $ length lnodes
ac915973c15ca69c94cb2eaa3321c9e9d04e44e0Christian Maeder , mkAttr "dgedges" . show $ length ledges
ac915973c15ca69c94cb2eaa3321c9e9d04e44e0Christian Maeder , mkAttr "nextlinkid" . showEdgeId $ getNewEdgeId dg ]
ac915973c15ca69c94cb2eaa3321c9e9d04e44e0Christian Maeder . unode "DGraph" $
ac915973c15ca69c94cb2eaa3321c9e9d04e44e0Christian Maeder subnodes "Global" (annotations ga . convertGlobalAnnos
46c318705d1532d90572abf9ee869016583d985bTill Mossakowski $ removeDOLprefixes ga)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ map (lnode opts ga lenv) lnodes
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ map (ledge opts ga dg) ledges
e26ecb5fd55a955c4c78ec69bb65b17fd06684edChristian Maedergmorph :: HetcatsOpts -> GlobalAnnos -> GMorphism -> Element
e26ecb5fd55a955c4c78ec69bb65b17fd06684edChristian Maedergmorph opts ga gm@(GMorphism cid (ExtSign ssig _) _ tmor _) =
f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder case map_sign cid ssig of
f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder Result _ mr -> case mr of
f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder Nothing -> error $ "Static.ToXml.gmorph: " ++ showGlobalDoc ga gm ""
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder Just (tsig, tsens) -> let
f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder tid = targetLogic cid
f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder sl = Map.toList . Map.filterWithKey (/=) $ symmap_of tid tmor
f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder in add_attr (mkNameAttr $ language_name cid)
f0d823af5e37881b77328bbcff8c96b58b92c89fChristian Maeder $ unode "GMorphism" $
e26ecb5fd55a955c4c78ec69bb65b17fd06684edChristian Maeder (if fullTheories opts then [] else subnodes "ComorphismAxioms"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ map (showSen opts (targetLogic cid) ga Nothing tsig) tsens)
e3305bbbe495bf8cb78de93b394d7ae02416e98dChristian Maeder ++ map (\ (s, t) -> unode "map" [showSym tid s, showSym tid t]) sl
081deee1bac477ab8db717646baba47f0fe95479Christian MaederprettyRangeElem :: (GetRange a, Pretty a) => String -> GlobalAnnos -> a
081deee1bac477ab8db717646baba47f0fe95479Christian MaederprettyRangeElem s ga a =
081deee1bac477ab8db717646baba47f0fe95479Christian Maeder add_attrs (rangeAttrs $ getRangeSpan a) $ prettyElem s ga a
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian MaederprettySymbol :: (GetRange a, Pretty a) => GlobalAnnos -> a -> Element
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian MaederprettySymbol = prettyRangeElem "Symbol"
034d9e2e9ada5aaa5665180720744d51166dacd4Christian Maederlnode :: HetcatsOpts -> GlobalAnnos -> LibEnv -> LNode DGNodeLab -> Element
ad9b8f3560ec449618d133d33beb179a6856e35cysengrimmlnode opts ga lenv (nodeId, lbl) =
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder let nm = dgn_name lbl
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder (spn, xp) = case reverse $ xpath nm of
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder ElemName s : t -> (s, showXPath t)
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder l -> ("?", showXPath l)
595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht in add_attrs (mkNameAttr (showName nm)
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder : rangeAttrs (srcRange nm)
4181ded0f1466b683557af18e8af5da2df6bab05ysengrimm ++ [mkAttr "id" $ show nodeId]
85688faec4e22ab1b6d328415e47063a42b98ec0ysengrimm ++ [mkAttr "internal" (map toLower $ show $ isInternal nm)]
764c796b88ef1d3921d7807683ee7bba3e764a29Christian Maeder ++ mkAttr "reference" (map toLower $ show $ isDGRef lbl)
cdaa846fedda6aae48cb4725bef801639154f9ceChristian Maeder : case signOf $ dgn_theory lbl of
595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht G_sign slid _ _ -> mkAttr "logic" (show slid)
cdaa846fedda6aae48cb4725bef801639154f9ceChristian Maeder : if not (isDGRef lbl) && dgn_origin lbl < DGProof then
595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht [mkAttr "refname" spn, mkAttr "relxpath" xp ]
4e1239f8b5fa139bd9be8d0431d711c7b88a58c2Christian Maeder $ unode "DGNode"
5b68f1141555736e0b7ddbe14218bcabcc44636fChristian Maeder $ case nodeInfo lbl of
863c98ae89e37c21c0c04b9b130b5136688976eeChristian Maeder DGRef li rf ->
01ddc4cad68fa84b4e9dd41089ad876329bae5b0Christian Maeder [ mkAttr "library" $ show $ setAngles False $ getLibId li
3d3529527fbd3645d25c9111c0ce5db0fd3d7efdChristian Maeder , mkAttr "location" $ getFilePath li
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maeder , mkAttr "node" $ getNameOfNode rf $ lookupDGraph li lenv ]
e4147f07c61def118b6052ccdf57207b0c113921Simon Ulbricht $ unode "Reference" () ]
595bf3e172e12ef62c72b9a87ff7aedbfed416ffSimon Ulbricht DGNode orig cs -> consStatus cs ++ case orig of
e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder DGBasicSpec _ (G_sign lid (ExtSign dsig _) _) _ ->
e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder subnodes "Declarations"
deb58cca57a0ec5eacf69ec6770d70b4701fa8b4Christian Maeder $ map (showSym lid)
e3d7fd1b63d824960b1c17b6c7009d52d7528c1eChristian Maeder $ mostSymsOf lid dsig
e46d78f7c6324ed9f1a191d46b6e5732e61e1835Simon Ulbricht DGRestriction _ hidSyms -> subnodes "Hidden"
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder $ map (prettySymbol ga)
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder ++ case dgn_theory lbl of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder G_theory lid _ (ExtSign sig _) _ thsens _ -> let
b96ff7f4ee9d433248311f6d0f25c84719dc4aafChristian Maeder (axs, thms) = OMap.partition isAxiom thsens in
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (if fullSign opts
b96ff7f4ee9d433248311f6d0f25c84719dc4aafChristian Maeder then subnodes "Symbols" (map (showSym lid) $ symlist_of lid sig)
b96ff7f4ee9d433248311f6d0f25c84719dc4aafChristian Maeder ++ subnodes "Axioms"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (map (showSen opts lid ga Nothing sig) $ toNamedList axs)
b96ff7f4ee9d433248311f6d0f25c84719dc4aafChristian Maeder ++ subnodes "Theorems"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (map (\ (s, t) -> showSen opts lid ga
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder (Just $ isProvenSenStatus t) sig $ toNamed s t)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ if fullTheories opts then case globalTheory lbl of
b96ff7f4ee9d433248311f6d0f25c84719dc4aafChristian Maeder Just (G_theory glid _ _ _ allSens _) -> case
b96ff7f4ee9d433248311f6d0f25c84719dc4aafChristian Maeder coerceThSens glid lid "xml-lnode" allSens of
b96ff7f4ee9d433248311f6d0f25c84719dc4aafChristian Maeder Just gsens -> subnodes "ImpAxioms"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ map (showSen opts lid ga Nothing sig) $ toNamedList
8c4c622824d516d1157913204737743f632473a4Christian Maeder $ OMap.filter ((`notElem` map sentence
8c4c622824d516d1157913204737743f632473a4Christian Maeder (OMap.elems thsens)) . sentence) gsens
34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder-- | a status may be open, proven or outdated
34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian MaedermkStatusAttr :: String -> Attr
34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian MaedermkStatusAttr = mkAttr "status"
34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian MaedermkProvenAttr :: Bool -> Attr
34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian MaedermkProvenAttr b = mkStatusAttr $ if b then "proven" else "open"
2fe147b05116aea0862eab9c0342b3c4be8ec1fdChristian MaederconsStatus :: ConsStatus -> [Element]
0607966fab6924a9fda8b55a9dccb28236a856deSimon UlbrichtconsStatus cs = case getConsOfStatus cs of
069541f0927770d9f3eded5e163a815f3e59767fChristian Maeder cStat -> [unode "ConsStatus" $ show cStat]
e26ecb5fd55a955c4c78ec69bb65b17fd06684edChristian Maederledge :: HetcatsOpts -> GlobalAnnos -> DGraph -> LEdge DGLinkLab -> Element
e26ecb5fd55a955c4c78ec69bb65b17fd06684edChristian Maederledge opts ga dg (f, t, lbl) = let
34db68bf7b0a0cb624373cc364a56442c1b3f0f7Christian Maeder typ = dgl_type lbl
e26ecb5fd55a955c4c78ec69bb65b17fd06684edChristian Maeder mor = gmorph opts ga $ dgl_morphism lbl
c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder mkMor n = add_attr (mkAttr "morphismsource" $ getNameOfNode n dg) mor
eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht lnkSt = case thmLinkStatus typ of
eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht Nothing -> []
dd8d2aeeb3648de87bd70d261a9e0a49b8239f4bSimon Ulbricht Just tls -> case tls of
dd8d2aeeb3648de87bd70d261a9e0a49b8239f4bSimon Ulbricht LeftOpen -> []
dd8d2aeeb3648de87bd70d261a9e0a49b8239f4bSimon Ulbricht Proven r ls -> dgrule r ++ map (\ e ->
eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht add_attr (mkAttr "linkref" $ showEdgeId e)
eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht $ unode "ProofBasis" ()) (Set.toList $ proofBasis ls)
bea536c79193020edac8fc6ebdd51b11f885b5afChristian Maeder ([ mkAttr "source" $ getNameOfNode f dg
54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder , mkAttr "target" $ getNameOfNode t dg
bea536c79193020edac8fc6ebdd51b11f885b5afChristian Maeder , mkAttr "linkid" $ showEdgeId $ dgl_id lbl
b6add2dd75c2a5a482f2d5fa133cfc1dc43e3429ysengrimm , mkAttr "id_source" $ show f
b6add2dd75c2a5a482f2d5fa133cfc1dc43e3429ysengrimm , mkAttr "id_target" $ show t
bea536c79193020edac8fc6ebdd51b11f885b5afChristian Maeder ] ++ case dgl_origin lbl of
e24ccbc27ab90aa0bdb7064fd42e3bb0e0da6174Christian Maeder DGLinkView i _ ->
01ddc4cad68fa84b4e9dd41089ad876329bae5b0Christian Maeder [mkNameAttr . iriToStringShortUnsecure $ setAngles False i]
4e1239f8b5fa139bd9be8d0431d711c7b88a58c2Christian Maeder $ unode "DGLink"
eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht $ unode "Type" (getDGLinkType lbl) : lnkSt
eccd7c7446e270bda674c07248d04fccc41cba0bSimon Ulbricht ++ consStatus (getLinkConsStatus typ)
c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder ++ [case typ of
c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder HidingFreeOrCofreeThm _ n _ _ -> mkMor n
c62c1b82e3316ff978475d6e61a5ed172fe60b0bChristian Maeder FreeOrCofreeDefLink _ (JustNode ns) -> mkMor $ getNode ns
54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maederdgrule :: DGRule -> [Element]
54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder unode "Rule" (dgRuleHeader r)
54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder DGRuleLocalInference m ->
54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder map (\ (s, t) -> add_attrs [mkNameAttr s, mkAttr "renamedTo" t]
54233d1f5ebf82ebb341a0f481e8ae657fc90e91Christian Maeder $ unode "MovedTheorems" ()) m
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder Composition es -> map (\ e ->
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder add_attr (mkAttr "linkref" $ showEdgeId e)
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder $ unode "Composition" ()) es
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder DGRuleWithEdge _ e ->
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder [ add_attr (mkAttr "linkref" $ showEdgeId e)
0a5165c161ce13d434b5c0488b533a8de98aafaaChristian Maeder $ unode "RuleTarget" () ]
486db0a875bcdd0b80cf0d447d14c9c00a92ae94Simon Ulbricht-- | collects all symbols from dg and displays them as xml
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksadgSymbols :: HetcatsOpts -> DGraph -> Element
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksadgSymbols opts dg = let ga = globalAnnos dg in unode "Ontologies"
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder $ map (\ (i, lbl) -> let ins = getImportNames dg i in
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa showSymbols opts ins ga lbl) $ labNodesDG dg
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbols :: HetcatsOpts -> [String] -> GlobalAnnos -> DGNodeLab -> Element
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbols opts ins ga lbl = showSymbolsTh opts ins (getDGNodeName lbl) ga
a7b34c1a61dabe150288424d90389d5988bf9d7aChristian Maeder $ dgn_theory lbl
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbolsTh :: HetcatsOpts -> [String] -> String -> GlobalAnnos -> G_theory -> Element
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSymbolsTh opts ins name ga th = case th of
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder G_theory lid _ (ExtSign sig _) _ sens _ -> add_attrs
a7b34c1a61dabe150288424d90389d5988bf9d7aChristian Maeder [ mkAttr "logic" $ language_name lid
a7b34c1a61dabe150288424d90389d5988bf9d7aChristian Maeder , mkNameAttr name ]
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder . unode "Ontology"
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder $ [ unode "Symbols" . map (showSym lid) $ symlist_of lid sig
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , unode "Axioms" . map (showSen opts lid ga Nothing sig) $ toNamedList sens ]
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder ++ map (unode "Import") ins
62631c8934cb171853a6c3d7910d1cd335007bf5Christian MaedershowSen :: ( GetRange sentence, Pretty sentence
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder , Sentences lid sentence sign morphism symbol) =>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa HetcatsOpts -> lid -> GlobalAnnos -> Maybe Bool -> sign -> Named sentence -> Element
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksashowSen opts lid ga mt sig ns =
6538c7b76c51c5c4de59b9cb19941cd2f4202ef3mcodescu let s = sentence ns in add_attrs
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder Nothing -> []
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder Just b -> [mkProvenAttr b]
6b528c4cf589cd5010c678770f023ae5250d6c67mcodescu ++ mkNameAttr (senAttr ns) : rangeAttrs (getRangeSpan s)
6538c7b76c51c5c4de59b9cb19941cd2f4202ef3mcodescu ++ case priority ns of
6b528c4cf589cd5010c678770f023ae5250d6c67mcodescu Just impo -> [mkPriorityAttr impo]
62631c8934cb171853a6c3d7910d1cd335007bf5Christian Maeder . unode (if isJust mt then "Theorem" else "Axiom") $ unode "Text"
acf3a7b84d7e077f693f3ca94d3c482a3ad33888Christian Maeder (show . useGlobalAnnos ga . print_named lid
acf3a7b84d7e077f693f3ca94d3c482a3ad33888Christian Maeder . makeNamed "" $ simplify_sen lid sig s)
a7338b15cbc9b513aaded07198c8666f0fa9d612Till Mossakowski : map (showSym lid) (symsOfSen lid sig s)
ba5846fc23b977b85874253d22d8de085c8aa006Christian Maeder ++ case senMark ns of
ba5846fc23b977b85874253d22d8de085c8aa006Christian Maeder m -> [unode "ComorphismOrigin" m]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ if printAST opts
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa then [unode "AST" $ asXml s]
fbb98c3714200d240ae693dc673cc36198cff2f5Till MossakowskishowSym :: (Sentences lid sentence sign morphism symbol) =>
fbb98c3714200d240ae693dc673cc36198cff2f5Till Mossakowski lid -> symbol -> Element
9f086fbf558eb1b21acbb2578661efbd2ce8d9f8notanartistshowSym lid s = add_attrs ((reverse
9f086fbf558eb1b21acbb2578661efbd2ce8d9f8notanartist . maybe id ((:) . mkAttr "label") (sym_label lid s))
9f086fbf558eb1b21acbb2578661efbd2ce8d9f8notanartist [ mkAttr "iri" $ fullSymName lid s
d6c22304918206b9dc0218673c83d976d7a14b77Christian Maeder , mkNameAttr . show $ sym_name lid s
9f086fbf558eb1b21acbb2578661efbd2ce8d9f8notanartist , mkAttr "kind" $ symKind lid s
9f086fbf558eb1b21acbb2578661efbd2ce8d9f8notanartist ]) $ prettySymbol emptyGlobalAnnos s