Changeset 12744

Show
Ignore:
Timestamp:
27.10.2009 22:05:08 (4 weeks ago)
Author:
raider
Message:

shortened menus of nodes and edges. shortened function names. names of internal ref nodes are now show- and hideable.

Files:
1 modified

Legend:

Unmodified
Added
Removed

  • trunk/GUI/GraphMenu.hs

    r12742 r12744  
    283283                -> [(DGNodeType,DaVinciNodeTypeParms GA.NodeValue)] 
    284284createNodeTypes gInfo@(GInfo {hetcatsOpts = opts}) cGraph showLib = map 
    285   (\ (n, s, c) -> 
    286     ( n 
    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 
     285  (\ (n, s, c) -> (n, if isRefType n 
     286    then createMenuNodeRef s c gInfo cGraph showLib $ isInternalSpec n 
     287    else createMenuNode s c gInfo $ isInternalSpec n)) $ nodeTypes opts 
    292288 
    293289-- | the edge types (share strings to avoid typos) 
    … …  
    296292  map (\(title, look, color, hasCons) -> 
    297293        (title, look 
    298             $$$ Color color 
    299             $$$ (if hasCons then createLocalEdgeMenuConsEdge gInfo 
    300                   else createLocalEdgeMenu gInfo) 
    301             $$$ (if hasCons then createLocalMenuValueTitleShowConservativity 
    302                   $$$ emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue 
    303                   else 
    304                     emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue)) 
     294          $$$ Color color 
     295          $$$ (if hasCons then createEdgeMenuConsEdge gInfo 
     296                else createEdgeMenu gInfo) 
     297          $$$ (if hasCons then createMenuValueTitleShowConservativity 
     298                $$$ emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue 
     299                else emptyArcTypeParms :: DaVinciArcTypeParms GA.EdgeValue)) 
    305300      ) $ edgeTypes opts 
    306301 
    307302-- * methods to create the local menus of the different nodetypes 
    308303 
    309 createLocalMenuNode :: GInfo -> DaVinciNodeTypeParms GA.NodeValue 
    310 createLocalMenuNode gInfo = LocalMenu (Menu (Just "node menu") $ map ($ gInfo) 
    311   [ createLocalMenuButtonShowNodeInfo 
    312   , createLocalMenuButtonShowTheory 
    313   , createLocalMenuButtonTranslateTheory 
    314   , createLocalMenuTaxonomy 
    315   , createLocalMenuButtonShowProofStatusOfNode 
    316   , createLocalMenuButtonProveAtNode 
    317   , createLocalMenuButtonProveStructured 
    318   , createLocalMenuButtonCheckCons 
    319   , createLocalMenuButtonCCCAtNode ]) $$$ emptyNodeTypeParms 
     304titleNormal :: forall t. ValueTitle (String, t) 
     305titleNormal = ValueTitle (\ (s,_) -> return s) 
     306 
     307titleInternal :: forall t. GInfo -> ValueTitleSource (String, t) 
     308titleInternal (GInfo { internalNames = updaterIORef }) = 
     309  ValueTitleSource (\ (s,_) -> do 
     310                     b <- newSimpleBroadcaster "" 
     311                     updater <- readIORef updaterIORef 
     312                     let upd = (s,applySimpleUpdate b) 
     313                     writeIORef updaterIORef $ upd:updater 
     314                     return $ toSimpleSource b) 
    320315 
    321316-- | local menu for the nodetypes spec and locallyEmpty_spec 
    322 createLocalMenuNodeTypeSpec :: Shape GA.NodeValue -> String -> GInfo 
    323                             -> DaVinciNodeTypeParms GA.NodeValue 
    324 createLocalMenuNodeTypeSpec shape color gInfo = 
    325                  shape $$$ Color color 
    326                  $$$ ValueTitle (\ (s,_) -> return s) 
    327                  $$$ createLocalMenuNode gInfo 
    328  
    329 -- | local menu for the nodetypes internal and locallyEmpty_internal 
    330 createLocalMenuNodeTypeInternal :: Shape GA.NodeValue -> String -> GInfo 
    331                                 -> DaVinciNodeTypeParms GA.NodeValue 
    332 createLocalMenuNodeTypeInternal shape color 
    333                gInfo@(GInfo { internalNames = updaterIORef }) = 
    334                  shape $$$ Color color 
    335                  $$$ ValueTitleSource (\ (s,_) -> do 
    336                        b <- newSimpleBroadcaster "" 
    337                        updater <- readIORef updaterIORef 
    338                        let upd = (s,applySimpleUpdate b) 
    339                        writeIORef updaterIORef $ upd:updater 
    340                        return $ toSimpleSource b) 
    341                  $$$ createLocalMenuNode gInfo 
     317createMenuNode :: Shape GA.NodeValue -> String -> GInfo -> Bool 
     318               -> DaVinciNodeTypeParms GA.NodeValue 
     319createMenuNode shape color gInfo internal = shape 
     320  $$$ Color color 
     321  $$$ (if internal then Just $ titleInternal gInfo else Nothing) 
     322  $$$? (if internal then Nothing else Just titleNormal) 
     323  $$$? LocalMenu (Menu Nothing (map ($ gInfo) 
     324        [ createMenuButtonShowNodeInfo 
     325        , createMenuButtonShowTheory 
     326        , createMenuButtonTranslateTheory 
     327        , createMenuTaxonomy 
     328        , createMenuButtonShowProofStatusOfNode 
     329        , createMenuButtonProveAtNode 
     330        , createMenuButtonProveStructured 
     331        , createMenuButtonCheckCons 
     332#ifndef GTKGLADE 
     333        , createMenuButtonCCCAtNode 
     334#endif 
     335        ])) 
     336  $$$ emptyNodeTypeParms 
     337 
    342338 
    343339-- | local menu for the nodetypes dg_ref and locallyEmpty_dg_ref 
    344 createLocalMenuNodeTypeDgRef :: Shape GA.NodeValue -> String -> GInfo 
    345                              -> ConvFunc -> LibFunc 
    346                              -> DaVinciNodeTypeParms GA.NodeValue 
    347 createLocalMenuNodeTypeDgRef shape color gInfo convGraph showLib = 
    348                  shape $$$ Color color 
    349                  $$$ ValueTitle (\ (s,_) -> return s) 
    350                  $$$ LocalMenu (Menu (Just "node menu") 
    351                    [createLocalMenuButtonShowNodeInfo gInfo, 
    352                     createLocalMenuButtonShowTheory gInfo, 
    353                     createLocalMenuButtonShowProofStatusOfNode gInfo, 
    354                     createLocalMenuButtonProveAtNode gInfo, 
    355                     Button "Show referenced library" 
    356                      (\ (_, descr) -> do 
    357                        showReferencedLibrary descr gInfo convGraph showLib 
    358                        return () 
    359                      )]) 
    360                  $$$ emptyNodeTypeParms 
     340createMenuNodeRef :: Shape GA.NodeValue -> String -> GInfo -> ConvFunc 
     341                  -> LibFunc -> Bool -> DaVinciNodeTypeParms GA.NodeValue 
     342createMenuNodeRef shape color gInfo convGraph showLib internal = shape 
     343  $$$ Color color 
     344  $$$ (if internal then Just $ titleInternal gInfo else Nothing) 
     345  $$$? (if internal then Nothing else Just titleNormal) 
     346  $$$? LocalMenu (Menu Nothing 
     347        [ createMenuButtonShowNodeInfo gInfo 
     348        , createMenuButtonShowTheory gInfo 
     349        , createMenuButtonShowProofStatusOfNode gInfo 
     350        , createMenuButtonProveAtNode gInfo 
     351        , Button "Show referenced library" 
     352            (\ (_, n) -> showReferencedLibrary n gInfo convGraph showLib) 
     353        ]) 
     354  $$$ emptyNodeTypeParms 
    361355 
    362356type ButtonMenu a = MenuPrim (Maybe String) (a -> IO ()) 
    … …  
    376370        return () 
    377371 
    378 createLocalMenuButtonShowTheory :: GInfo -> ButtonMenu GA.NodeValue 
    379 createLocalMenuButtonShowTheory gInfo = 
     372createMenuButtonShowTheory :: GInfo -> ButtonMenu GA.NodeValue 
     373createMenuButtonShowTheory gInfo = 
    380374  createMenuButton "Show theory" (getTheoryOfNode gInfo) gInfo 
    381375 
    382 createLocalMenuButtonTranslateTheory :: GInfo -> ButtonMenu GA.NodeValue 
    383 createLocalMenuButtonTranslateTheory gInfo = 
     376createMenuButtonTranslateTheory :: GInfo -> ButtonMenu GA.NodeValue 
     377createMenuButtonTranslateTheory gInfo = 
    384378  createMenuButton "Translate theory" (translateTheoryOfNode gInfo) gInfo 
    385379 
    386380-- | create a sub menu for taxonomy visualisation 
    387 createLocalMenuTaxonomy :: GInfo -> ButtonMenu GA.NodeValue 
    388 createLocalMenuTaxonomy gInfo = let 
    389     passTh displayFun descr _ = do 
    390       ost <- readIORef $ intState gInfo 
    391       case i_state ost of 
    392         Nothing -> return () 
    393         Just ist -> do 
    394           let Result ds res = computeTheory (i_libEnv ist) (libName gInfo) descr 
    395           showDiagMess (hetcatsOpts gInfo) ds 
    396           maybe (return ()) (displayFun $ show descr) res 
    397     in Menu (Just "Taxonomy graphs") 
     381createMenuTaxonomy :: GInfo -> ButtonMenu GA.NodeValue 
     382createMenuTaxonomy gInfo = let 
     383  passTh displayFun descr _ = do 
     384    ost <- readIORef $ intState gInfo 
     385    case i_state ost of 
     386      Nothing -> return () 
     387      Just ist -> do 
     388        let Result ds res = computeTheory (i_libEnv ist) (libName gInfo) descr 
     389        showDiagMess (hetcatsOpts gInfo) ds 
     390        maybe (return ()) (displayFun $ show descr) res 
     391  in Menu (Just "Taxonomy graphs") 
    398392    [ createMenuButton "Subsort graph" (passTh displaySubsortGraph) gInfo 
    399393    , createMenuButton "Concept graph" (passTh displayConceptGraph) gInfo ] 
    400394 
    401 createLocalMenuButtonShowProofStatusOfNode :: GInfo -> ButtonMenu GA.NodeValue 
    402 createLocalMenuButtonShowProofStatusOfNode gInfo = 
     395createMenuButtonShowProofStatusOfNode :: GInfo -> ButtonMenu GA.NodeValue 
     396createMenuButtonShowProofStatusOfNode gInfo = 
    403397  createMenuButton "Show proof status" (showProofStatusOfNode gInfo) gInfo 
    404398 
    405 createLocalMenuButtonProveAtNode :: GInfo -> ButtonMenu GA.NodeValue 
    406 createLocalMenuButtonProveAtNode gInfo = 
    407   createMenuButton "Prove" 
    408     (proveAtNode False gInfo) gInfo 
    409  
    410 createLocalMenuButtonProveStructured :: GInfo -> ButtonMenu GA.NodeValue 
    411 createLocalMenuButtonProveStructured gInfo = 
    412   createMenuButton "Prove VSE Structured" 
    413     (\ descr _ -> proveVSEStructured gInfo descr) gInfo 
    414  
    415 createLocalMenuButtonCheckCons :: GInfo -> ButtonMenu GA.NodeValue 
    416 createLocalMenuButtonCheckCons gInfo = 
     399createMenuButtonProveAtNode :: GInfo -> ButtonMenu GA.NodeValue 
     400createMenuButtonProveAtNode gInfo = 
     401  createMenuButton "Prove" (proveAtNode False gInfo) gInfo 
     402 
     403createMenuButtonProveStructured :: GInfo -> ButtonMenu GA.NodeValue 
     404createMenuButtonProveStructured gInfo = 
     405  createMenuButton "Prove VSE Structured" (\ descr _ -> 
     406    proofMenu gInfo (SelectCmd Prover $ "VSE structured: " ++ show descr) 
     407              $ VSE.prove (libName gInfo, descr)) gInfo 
     408 
     409createMenuButtonCheckCons :: GInfo -> ButtonMenu GA.NodeValue 
     410createMenuButtonCheckCons gInfo = 
    417411  createMenuButton "Check conservativity" 
    418412    (\ descr -> checkconservativityOfNode descr gInfo) gInfo 
    419413 
    420 -- | call VSE structured 
    421 proveVSEStructured :: GInfo -> Int -> IO () 
    422 proveVSEStructured gi n = 
    423   proofMenu gi (SelectCmd Prover $ "VSE structured: " ++ show n) 
    424     $ VSE.prove (libName gi, n) 
    425  
    426 createLocalMenuButtonCCCAtNode :: GInfo -> ButtonMenu GA.NodeValue 
    427 createLocalMenuButtonCCCAtNode gInfo = 
     414#ifndef GTKGLADE 
     415createMenuButtonCCCAtNode :: GInfo -> ButtonMenu GA.NodeValue 
     416createMenuButtonCCCAtNode gInfo = 
    428417  createMenuButton "Check consistency" (proveAtNode True gInfo) gInfo 
    429  
    430 createLocalMenuButtonShowNodeInfo :: GInfo -> ButtonMenu GA.NodeValue 
    431 createLocalMenuButtonShowNodeInfo = 
     418#endif 
     419 
     420createMenuButtonShowNodeInfo :: GInfo -> ButtonMenu GA.NodeValue 
     421createMenuButtonShowNodeInfo = 
    432422  createMenuButton "Show node info" showNodeInfo 
    433423 
    434424-- * methods to create the local menus for the edges 
    435425 
    436 createLocalEdgeMenu :: GInfo -> LocalMenu GA.EdgeValue 
    437 createLocalEdgeMenu = LocalMenu . createLocalMenuButtonShowEdgeInfo 
    438  
    439 createLocalEdgeMenuConsEdge :: GInfo -> LocalMenu GA.EdgeValue 
    440 createLocalEdgeMenuConsEdge gInfo = 
    441   LocalMenu (Menu (Just "egde menu") 
    442                   [ createLocalMenuButtonShowEdgeInfo gInfo 
    443                   , createLocalMenuButtonCheckconservativityOfEdge gInfo]) 
    444  
    445 createLocalMenuButtonShowEdgeInfo :: GInfo -> ButtonMenu GA.EdgeValue 
    446 createLocalMenuButtonShowEdgeInfo _ = Button "Show info" 
     426createEdgeMenu :: GInfo -> LocalMenu GA.EdgeValue 
     427createEdgeMenu = LocalMenu . createMenuButtonShowEdgeInfo 
     428 
     429createEdgeMenuConsEdge :: GInfo -> LocalMenu GA.EdgeValue 
     430createEdgeMenuConsEdge gInfo = LocalMenu $ Menu Nothing 
     431  [ createMenuButtonShowEdgeInfo gInfo 
     432  , createMenuButtonCheckconservativityOfEdge gInfo] 
     433 
     434createMenuButtonShowEdgeInfo :: GInfo -> ButtonMenu GA.EdgeValue 
     435createMenuButtonShowEdgeInfo _ = Button "Show info" 
    447436  (\ (_, (EdgeId descr), maybeLEdge) -> showEdgeInfo descr maybeLEdge) 
    448437 
    449 createLocalMenuButtonCheckconservativityOfEdge :: GInfo 
     438createMenuButtonCheckconservativityOfEdge :: GInfo 
    450439                                               -> ButtonMenu GA.EdgeValue 
    451 createLocalMenuButtonCheckconservativityOfEdge gInfo = 
     440createMenuButtonCheckconservativityOfEdge gInfo = 
    452441  Button "Check conservativity" 
    453442    (\ (_, (EdgeId descr), maybeLEdge)  -> 
    454443      checkconservativityOfEdge descr gInfo maybeLEdge) 
    455444 
    456 createLocalMenuValueTitleShowConservativity :: ValueTitle GA.EdgeValue 
    457 createLocalMenuValueTitleShowConservativity = ValueTitle 
     445createMenuValueTitleShowConservativity :: ValueTitle GA.EdgeValue 
     446createMenuValueTitleShowConservativity = ValueTitle 
    458447  (\ (_, _, maybeLEdge) -> case maybeLEdge of 
    459448    Just (_, _, edgelab) -> case dgl_type edgelab of 
    … …  
    472461getProofScriptFileName :: String -> IO FilePath 
    473462getProofScriptFileName f 
    474     | "/" `isPrefixOf` f = return $ f ++ ".hpf" 
    475     | otherwise          = do 
    476                            dir <- getCurrentDirectory 
    477                            return $ dir ++ '/' : f ++ ".hpf" 
     463 | "/" `isPrefixOf` f = return $ f ++ ".hpf" 
     464 | otherwise          = do 
     465                          dir <- getCurrentDirectory 
     466                          return $ dir ++ '/' : f ++ ".hpf" 
    478467 
    479468 
    480469-- | Displays a Save-As dialog and writes the proof-script. 
    481470askSaveProofScript :: GA.GraphInfo -> IORef IntState -> IO () 
    482 askSaveProofScript gi ch = 
    483     do 
    484     h <- readIORef ch 
    485     case undoList $ i_hist h of 
    486      [] -> infoDialog "Information" "The history is empty. No file written." 
    487      _ -> do 
    488       ff <- getProofScriptFileName $ rmSuffix $ filename h 
    489       maybeFilePath<- fileSaveDialog ff [("Proof Script",["*.hpf"]) 
    490                                          , ("All Files", ["*"])] Nothing 
    491       case maybeFilePath of 
    492         Just fPath -> do 
    493            GA.showTemporaryMessage gi "Saving proof script ..." 
    494            saveCommandHistory ch fPath 
    495            GA.showTemporaryMessage gi $ "Proof script saved to " ++ 
    496                                             fPath ++ "!" 
    497         Nothing -> GA.showTemporaryMessage gi "Aborted!" 
     471askSaveProofScript gi ch = do 
     472  h <- readIORef ch 
     473  case undoList $ i_hist h of 
     474   [] -> infoDialog "Information" "The history is empty. No file written." 
     475   _ -> do 
     476     ff <- getProofScriptFileName $ rmSuffix $ filename h 
     477     maybeFilePath <- fileSaveDialog ff [ ("Proof Script",["*.hpf"]) 
     478                                        , ("All Files", ["*"])] Nothing 
     479     case maybeFilePath of 
     480       Just fPath -> do 
     481         GA.showTemporaryMessage gi "Saving proof script ..." 
     482         saveCommandHistory ch fPath 
     483         GA.showTemporaryMessage gi $ "Proof script saved to " ++ fPath ++ "!" 
     484       Nothing -> GA.showTemporaryMessage gi "Aborted!" 
    498485 
    499486-- Saves the history of commands in a file. 
    500487saveCommandHistory :: IORef IntState -> String -> IO () 
    501488saveCommandHistory c f = do 
    502     h <- readIORef c 
    503     let history = ["# automatically generated hets proof-script", "", 
    504                   "use " ++ filename h, ""] 
    505           ++ reverse (map (showCmd . command) $ undoList $ i_hist h) 
    506     writeFile f $ unlines history 
     489  h <- readIORef c 
     490  let history = [ "# automatically generated hets proof-script", "" 
     491                , "use " ++ filename h, ""] 
     492                ++ reverse (map (showCmd . command) $ undoList $ i_hist h) 
     493  writeFile f $ unlines history