Changeset 12742

Show
Ignore:
Timestamp:
27.10.2009 15:43:56 (4 weeks ago)
Author:
maeder
Message:

adjusted display

Location:
trunk
Files:
3 modified

Legend:

Unmodified
Added
Removed

  • trunk/GUI/GraphLogic.hs

    r12730 r12742  
    169169             -> ([GA.NodeId], [(GA.NodeId, GA.NodeId, DGEdgeType, Bool)]) 
    170170hideNodesAux dg ignoreEdges = 
    171   let nodes = selectNodesByType dg [DGNodeType { nonRefType = NonRefType 
    172                                                  { isProvenCons = True 
    173                                                  , isInternalSpec = True} 
    174                                                , isLocallyEmpty = True}] 
     171  let nodes = selectNodesByType dg 
     172        (\ n -> isInternalSpec n && isProvenNode n && isProvenCons n) 
    175173      edges = getCompressedEdges dg nodes ignoreEdges 
    176174  in (nodes, edges) 
    … …  
    219217 
    220218-- | selects all nodes of a type with outgoing edges 
    221 selectNodesByType :: DGraph -> [DGNodeType] -> [Node] 
     219selectNodesByType :: DGraph -> (DGNodeType -> Bool) -> [Node] 
    222220selectNodesByType dg types = 
    223   filter (\ n -> (not . null $ outDG dg n) && filterInUnproven dg n) $ map fst 
    224   $ filter (\ (_, n) -> elem (getRealDGNodeType n) types) $ labNodesDG dg 
     221  filter (\ n -> not (null $ outDG dg n) && filterInUnproven dg n) $ map fst 
     222  $ filter (types . getRealDGNodeType . snd) $ labNodesDG dg 
    225223 
    226224filterInUnproven :: DGraph -> Node -> Bool 
    … …  
    241239-- | innDG with filter of not shown edges 
    242240fInnDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab] 
    243 fInnDG ignore dg = filter (\ (_,_,l) -> elem (dgl_id l) ignore) . innDG dg 
     241fInnDG ignore dg = filter (\ (_,_,l) -> notElem (dgl_id l) ignore) . innDG dg 
    244242 
    245243-- | outDG with filter of not shown edges 
    246244fOutDG :: [EdgeId] -> DGraph -> Node -> [LEdge DGLinkLab] 
    247 fOutDG ignore dg = filter (\ (_,_,l) -> elem (dgl_id l) ignore) . outDG dg 
     245fOutDG ignore dg = filter (\ (_,_,l) -> notElem (dgl_id l) ignore) . outDG dg 
    248246 
    249247-- | returns a list of compressed edges 

  • trunk/GUI/GraphMenu.hs

    r12740 r12742  
    5757              )] 
    5858nodeTypes opts = map 
    59   ( (\ (n, s) -> if isLocallyEmpty n then -- Add color 
    60       case nonRefType n of 
    61         NonRefType { isProvenCons = False } 
    62                 -> (n, s, getColor opts Yellow False True) 
    63         _       -> (n, s, getColor opts Green  True  False) 
    64       else case nonRefType n of 
    65         RefType -> (n, s, getColor opts Coral False False) 
    66         t       -> (n, s, getColor opts Coral False $ isProvenCons t) 
    67     ) 
    68   . (\ n -> case nonRefType n of -- Add shape 
    69       RefType -> (n, Box) 
    70       NonRefType {} -> (n, Ellipse) 
    71     ) 
     59  ((\ (n, s) -> if isProvenNode n then -- Add color 
     60      if isProvenCons n 
     61      then (n, s, getColor opts Green  True  False) 
     62      else (n, s, getColor opts Yellow False True) 
     63     else (n, s, getColor opts Coral False $ isProvenCons n)) 
     64  . \ n -> (n, if isRefType n then Box else Ellipse) -- Add shape 
    7265  ) listDGNodeTypes 
    7366 
    … …  
    292285  (\ (n, s, c) -> 
    293286    ( n 
    294     , case nonRefType n of 
    295         RefType -> createLocalMenuNodeTypeDgRef s c gInfo cGraph showLib 
    296         NonRefType { isInternalSpec = True } 
    297                 -> createLocalMenuNodeTypeInternal s c gInfo 
    298         NonRefType { isInternalSpec = False } 
    299                 -> createLocalMenuNodeTypeSpec s c gInfo 
    300     ) 
    301   ) $ nodeTypes opts 
     287    , if isRefType n 
     288      then createLocalMenuNodeTypeDgRef s c gInfo cGraph showLib 
     289      else if isInternalSpec n 
     290           then createLocalMenuNodeTypeInternal s c gInfo 
     291           else createLocalMenuNodeTypeSpec s c gInfo)) $ nodeTypes opts 
    302292 
    303293-- | the edge types (share strings to avoid typos) 
    … …  
    445435 
    446436createLocalEdgeMenu :: GInfo -> LocalMenu GA.EdgeValue 
    447 createLocalEdgeMenu gInfo = LocalMenu $ Menu (Just "short edge menu") 
    448   [createLocalMenuButtonShowEdgeInfo gInfo] 
     437createLocalEdgeMenu = LocalMenu . createLocalMenuButtonShowEdgeInfo 
    449438 
    450439createLocalEdgeMenuConsEdge :: GInfo -> LocalMenu GA.EdgeValue 
    … …  
    468457createLocalMenuValueTitleShowConservativity = ValueTitle 
    469458  (\ (_, _, maybeLEdge) -> case maybeLEdge of 
    470     Just (_,_,edgelab) -> case dgl_type edgelab of 
     459    Just (_, _, edgelab) -> case dgl_type edgelab of 
    471460      ScopedLink _ _ (ConsStatus c cp status) -> return (showCons c cp status) 
    472461      _ -> return "" 
    … …  
    486475    | otherwise          = do 
    487476                           dir <- getCurrentDirectory 
    488                            return $ dir ++ '/':f ++ ".hpf" 
     477                           return $ dir ++ '/' : f ++ ".hpf" 
    489478 
    490479 

  • trunk/Static/DevGraph.hs

    r12615 r12742  
    170170hasOpenGoals = hasSenKind (\ s -> not (isAxiom s) && not (isProvenSenStatus s)) 
    171171 
    172 -- | check if the node has an internal name (wrong for DGRef!) 
     172-- | check if the node has an internal name 
    173173isInternalNode :: DGNodeLab -> Bool 
    174 isInternalNode l@DGNodeLab {dgn_name = n} = not (isDGRef l) && isInternal n 
     174isInternalNode DGNodeLab {dgn_name = n} = isInternal n 
    175175 
    176176getNodeConsStatus :: DGNodeLab -> ConsStatus 
    … …  
    200200 
    201201data DGNodeType = DGNodeType 
    202   { nonRefType :: NonRefType 
    203   , isLocallyEmpty :: Bool } 
    204   deriving (Eq, Ord, Show) 
    205  
    206 data NonRefType = 
    207     RefType 
    208   | NonRefType { isProvenCons :: Bool 
    209                , isInternalSpec :: Bool } 
     202  { isRefType :: Bool 
     203  , isProvenNode :: Bool 
     204  , isProvenCons :: Bool 
     205  , isInternalSpec :: Bool } 
    210206  deriving (Eq, Ord, Show) 
    211207 
    … …  
    213209getRealDGNodeType :: DGNodeLab -> DGNodeType 
    214210getRealDGNodeType dgnlab = DGNodeType 
    215   { nonRefType = if isDGRef dgnlab then RefType else 
    216       NonRefType { isProvenCons = not $ hasOpenNodeConsStatus False dgnlab 
    217                  , isInternalSpec = isInternalNode dgnlab } 
    218   , isLocallyEmpty = not $ hasOpenGoals dgnlab 
    219   } 
     211  { isRefType = isDGRef dgnlab 
     212  , isProvenNode = not $ hasOpenGoals dgnlab 
     213  , isProvenCons = not $ hasOpenNodeConsStatus False dgnlab 
     214  , isInternalSpec = isInternalNode dgnlab } 
    220215 
    221216-- | Creates a list with all DGNodeType types 
    222217listDGNodeTypes :: [DGNodeType] 
    223 listDGNodeTypes = 
    224   [ DGNodeType { nonRefType = ref, isLocallyEmpty = isEmpty' } 
    225   | ref <- RefType : 
    226       [ NonRefType { isProvenCons = proven, isInternalSpec = spec } 
    227       | proven <- [True, False] 
    228       , spec <- [True, False] 
    229       ] 
    230   , isEmpty' <- [True, False] 
    231   ] 
     218listDGNodeTypes = let bs = [False, True] in 
     219  [ DGNodeType 
     220    { isRefType = ref 
     221    , isProvenNode = isEmpty' 
     222    , isProvenCons = proven 
     223    , isInternalSpec = spec } 
     224  | ref <- bs 
     225  , isEmpty' <- bs 
     226  , proven <- bs 
     227  , spec <- bs ] 
    232228 
    233229-- ** edge label types