Idris2Doc : CyBy.Draw.MoleculeCanvas

CyBy.Draw.MoleculeCanvas

(source)
Definitions
record DepNode : Type
  Record pairing graph with one of its node's index

  Totality: total
  Visibility: public export
  Constructor: 
DN : (graph : CDGraph) -> Fin (graph .order) -> DepNode

  Projections:
  
.graph : DepNode -> CDGraph
  
.node : ({rec:0} : DepNode) -> Fin ((graph {rec:0}) .order)

  Hints:
  
Eq DepNode
  
Show DepNode
.graph : DepNode -> CDGraph
  Totality: total
  Visibility: public export
graph : DepNode -> CDGraph
  Totality: total
  Visibility: public export
.node : ({rec:0} : DepNode) -> Fin ((graph {rec:0}) .order)
  Totality: total
  Visibility: public export
node : ({rec:0} : DepNode) -> Fin ((graph {rec:0}) .order)
  Totality: total
  Visibility: public export
data Mode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Select : Mode
  
Erase : Mode
  
Draw : Mode
  
SetAtom : Isotope -> Mode
  
SetAbbr : Abbreviation -> Mode
  
SetTempl : CDGraph -> Mode
  
RotTempl : Point Mol -> CDGraph -> Mode
  
RotTemplAtm : DepNode -> CDGraph -> Mode
  
RotTemplOvp : DepNode -> DepNode -> Point Mol -> Mode
  
Selecting : Point Id -> Mode
  
Erasing : Point Id -> Mode
  
Dragging : Point Mol -> Mode
  
Rotating : Point Mol -> Mode
  
Translating : Mode -> Mode
  
Drawing : Maybe Abbreviation -> Mode
  
PTable : Maybe Elem -> Mode

  Hints:
  
Eq Mode
  
Show Mode
record DrawState : Type
  Totality: total
  Visibility: public export
  Constructor: 
ST : SceneDims -> (transform : AffineTransformation) -> Point transform -> CDGraph -> List CDGraph -> List CDGraph -> Mode -> Modifier -> MolBond -> Maybe Abbreviation -> Bool -> Maybe Elem -> String -> String -> DrawState

  Projections:
  
.abbr : DrawState -> Maybe Abbreviation
  
.bond : DrawState -> MolBond
  
.curPos : ({rec:0} : DrawState) -> Point (transform {rec:0})
  
.curSVG : DrawState -> String
  Current SVG scene rendered to a string
  We keep track of this and the previous one to easily
  decide when to redraw the scene.
  
.dims : DrawState -> SceneDims
  
.hasFocus : DrawState -> Bool
  
.mode : DrawState -> Mode
  
.modifier : DrawState -> Modifier
  
.mol : DrawState -> CDGraph
  
.prevSVG : DrawState -> String
  Previous SVG scene rendered to a string
  
.ptable : DrawState -> Maybe Elem
  
.redos : DrawState -> List CDGraph
  
.transform : DrawState -> AffineTransformation
  
.undos : DrawState -> List CDGraph
.dims : DrawState -> SceneDims
  Totality: total
  Visibility: public export
dims : DrawState -> SceneDims
  Totality: total
  Visibility: public export
.transform : DrawState -> AffineTransformation
  Totality: total
  Visibility: public export
transform : DrawState -> AffineTransformation
  Totality: total
  Visibility: public export
.curPos : ({rec:0} : DrawState) -> Point (transform {rec:0})
  Totality: total
  Visibility: public export
curPos : ({rec:0} : DrawState) -> Point (transform {rec:0})
  Totality: total
  Visibility: public export
.mol : DrawState -> CDGraph
  Totality: total
  Visibility: public export
mol : DrawState -> CDGraph
  Totality: total
  Visibility: public export
.undos : DrawState -> List CDGraph
  Totality: total
  Visibility: public export
undos : DrawState -> List CDGraph
  Totality: total
  Visibility: public export
.redos : DrawState -> List CDGraph
  Totality: total
  Visibility: public export
redos : DrawState -> List CDGraph
  Totality: total
  Visibility: public export
.mode : DrawState -> Mode
  Totality: total
  Visibility: public export
mode : DrawState -> Mode
  Totality: total
  Visibility: public export
.modifier : DrawState -> Modifier
  Totality: total
  Visibility: public export
modifier : DrawState -> Modifier
  Totality: total
  Visibility: public export
.bond : DrawState -> MolBond
  Totality: total
  Visibility: public export
bond : DrawState -> MolBond
  Totality: total
  Visibility: public export
.abbr : DrawState -> Maybe Abbreviation
  Totality: total
  Visibility: public export
abbr : DrawState -> Maybe Abbreviation
  Totality: total
  Visibility: public export
.hasFocus : DrawState -> Bool
  Totality: total
  Visibility: public export
hasFocus : DrawState -> Bool
  Totality: total
  Visibility: public export
.ptable : DrawState -> Maybe Elem
  Totality: total
  Visibility: public export
ptable : DrawState -> Maybe Elem
  Totality: total
  Visibility: public export
.curSVG : DrawState -> String
  Current SVG scene rendered to a string
  We keep track of this and the previous one to easily
  decide when to redraw the scene.

  Totality: total
  Visibility: public export
curSVG : DrawState -> String
  Current SVG scene rendered to a string
  We keep track of this and the previous one to easily
  decide when to redraw the scene.

  Totality: total
  Visibility: public export
.prevSVG : DrawState -> String
  Previous SVG scene rendered to a string

  Totality: total
  Visibility: public export
prevSVG : DrawState -> String
  Previous SVG scene rendered to a string

  Totality: total
  Visibility: public export
toMol : DrawState -> MolfileAT
  Totality: total
  Visibility: export
toMolStr : DrawState -> String -> String
  Totality: total
  Visibility: export
.imol : (s : DrawState) -> CDIGraph ((s .mol) .order)
  Totality: total
  Visibility: export
emptyGraph : DrawState -> Bool
  True, if the current mol graph is the empty graph.

  Totality: total
  Visibility: export
data ScaleMode : Type
  Mode used to scale a molecule.
  
  This is used when centering a molecule, for instance, when we begin
  drawing, or when we just display a molecule and want to zoom in for it
  to fill the whole scene.

  Totality: total
  Visibility: public export
  Constructors:
  
Init : ScaleMode
  Scale mode used when initializing a scene for drawing
  
Reset : ScaleMode
  Scale mode used when centering the molecule (by pressing the "reset" button)
  
Fill : ScaleMode
  Scale mode used when displaying a molecule so that it fills the whole
  scene
scaleAt : DrawSettings => Point Id -> Scale -> DrawState -> DrawState
  Totality: total
  Visibility: export
scaleAtPos : DrawSettings => Scale -> DrawState -> DrawState
  Scales the molecule at the current mouse position.

  Totality: total
  Visibility: export
scaleAtCenter : DrawSettings => Scale -> DrawState -> DrawState
  Scales the molecule at the center of the scene

  Totality: total
  Visibility: export
.posId : DrawState -> Point Id
  Totality: total
  Visibility: export
.posMol : DrawState -> Point Mol
  Totality: total
  Visibility: export
applyWhenSel : DrawSettings => DrawState -> Lazy a -> Lazy a -> Lazy a -> a
  Totality: total
  Visibility: export
toTransform : AffineTransformation -> Transform
  Convert an `AffineTransformation` to a transformation to be
  used in an SVG element.

  Totality: total
  Visibility: export
update : DrawSettings => DrawEvent -> DrawState -> DrawState
  Totality: total
  Visibility: export
initMol : DrawSettings => SceneDims -> ScaleMode -> Bool -> String -> CDGraph -> DrawState
  Initializes the drawing state for the given mol graph.
  
  The `SceneDims` are used for centering the molecule, as well
  as for scaling it to fill the scene. The `metadata` flag is
  used to decide if the graph is atached to the SVG in form of
  a MOL file string.

  Totality: total
  Visibility: export
init : DrawSettings => SceneDims -> ScaleMode -> String -> DrawState
  Totality: total
  Visibility: export
fromMol : DrawSettings => SceneDims -> ScaleMode -> MolGraphAT -> DrawState
  Totality: total
  Visibility: export
exportSVGPair : DrawSettings => Bool -> String -> DrawState -> (SceneDims, String)
  Generates a string holding the SVG-encoded molecular structur
  together with the dimensions of the SVG-scnene.
  
  The `metadata` flag indicates, whether a `<metadata>` tag
  containing the molecular structure in `.mol` format should be
  included in the SVG content.

  Totality: total
  Visibility: export
exportSVG : DrawSettings => DrawState -> String
  Generates an SVG string out of the current DrawState. The
  graph is included as MOL file string inside the metadata tag.
  The border margin depends on the `CoreDims`s `selectBufferSize`
  field value.

  Totality: total
  Visibility: export