Interfaces.Command

Description

Synopsis

• data GlobCmd
  • = Automatic
  • | GlobDecomp
  • | GlobSubsume
  • | LocalDecomp
  • | LocalInference
  • | CompositionProveEdges
  • | CompositionCreateEdges
  • | Conservativity
  • | ThmHideShift
  • | HideThmShift
  • | Colimit
  • | NormalForm
  • | TriangleCons
  • | Freeness
  • | ThmFreeShift
  • | QualifyNames
  • | UndoCmd
  • | RedoCmd
  • | Importing
  • | DisjointUnion
  • | Renaming
  • | Hiding
  • | Heterogeneity
  • | ProveCurrent
  • | DisproveCurrent
  • | CheckConsistencyCurrent
  • | CheckConservativityAll
  • | DropTranslation
• globCmdList :: [GlobCmd]
• menuTextGlobCmd :: GlobCmd -> String
• cmdlGlobCmd :: GlobCmd -> String
• isDgRule :: GlobCmd -> Bool
• isFlatteningCmd :: GlobCmd -> Bool
• isUndoOrRedo :: GlobCmd -> Bool
• describeGlobCmd :: GlobCmd -> String
• globCmdNameStr :: GlobCmd -> String
• data SelectCmd
  • = LibFile
  • | Lib
  • | Node
  • | ComorphismTranslation
  • | Prover
  • | Goal
  • | ConsistencyChecker
  • | Link
  • | ConservativityCheckerOpen
  • | ConservativityChecker
• selectCmdList :: [SelectCmd]
• selectCmdNameStr :: SelectCmd -> String
• describeSelectCmd :: SelectCmd -> String
• data InspectCmd
  • = Libs
  • | Nodes
  • | Edges
  • | UndoHist
  • | RedoHist
  • | EdgeInfo
  • | CurrentComorphism
  • | LocalAxioms
  • | NodeInfo
  • | ComorphismsTo
  • | TranslatedTheory
  • | Theory
  • | AllGoals
  • | ProvenGoals
  • | UnprovenGoals
  • | Axioms
  • | Taxonomy
  • | Concept
• inspectCmdList :: [InspectCmd]
• showInspectCmd :: InspectCmd -> String
• requiresNode :: InspectCmd -> Bool
• data ChangeCmd
  • = Expand
  • | AddView
• describeChangeCmd :: ChangeCmd -> String
• changeCmdList :: [ChangeCmd]
• changeCmdNameStr :: ChangeCmd -> String
• data Command
  • = GlobCmd GlobCmd
  • | SelectCmd SelectCmd String
  • | TimeLimit Int
  • | SetAxioms [String]
  • | ShowOutput Bool
  • | IncludeProvenTheorems Bool
  • | InspectCmd InspectCmd (Maybe String)
  • | CommentCmd String
  • | GroupCmd [Command]
  • | ChangeCmd ChangeCmd String
  • | HelpCmd
  • | ExitCmd
• eqCmd :: Command -> Command -> Bool
• mkSelectCmd :: SelectCmd -> Command
• mkChangeCmd :: ChangeCmd -> Command
• cmdInputStr :: Command -> String
• setInputStr :: String -> Command -> Command
• cmdNameStr :: Command -> String
• showCmd :: Command -> String
• describeCmd :: Command -> String
• commandList :: [Command]

Documentation