Include file:
#include "mcrl2/gui/codeeditor.h
mcrl2::gui::qt::
CodeEditor
¶The CodeEditor class defines a text editor for code (used for specification and properties)
mcrl2::gui::qt::CodeEditor::
codeFont
¶mcrl2::gui::qt::CodeEditor::
highlighter
¶mcrl2::gui::qt::CodeEditor::
isSpecificationEditor
¶mcrl2::gui::qt::CodeEditor::
lightPalette
¶mcrl2::gui::qt::CodeEditor::
lineNumberArea
¶mcrl2::gui::qt::CodeEditor::
lineNumberFont
¶mcrl2::gui::qt::CodeEditor::
zoomInAction
¶mcrl2::gui::qt::CodeEditor::
zoomOutAction
¶changeHighlightingRules
()¶changeHighlightingRules Change the highlighting rules depending on the purpose of the code editor and its colour palette
CodeEditor
(QWidget *parent = 0)¶CodeEditor Constructor.
Parameters:
parent The parent of this widget
lineNumberAreaPaintEvent
(QPaintEvent *event)¶lineNumberAreaPaintEvent Paints the line number area on the screen
Parameters:
event A paint event
lineNumberAreaWidth
()¶lineNumberAreaWidth Computes the width needed for the line number area
Returns: The width needed for the line number area
setPurpose
(bool isSpecificationEditor)¶setPurpose Set whether this code editor is for editing specifications or mu-calculus formulae
Parameters:
isSpecificationEditor Whether this code editor is for editing specifications
~CodeEditor
()¶mcrl2::gui::qt::CodeEditor::deleteChar
deleteChar Allows the user to delete text
mcrl2::gui::qt::CodeEditor::zoomIn
zoomIn Allows the user to zoom in on the text
Parameters:
range How much to zoom in
mcrl2::gui::qt::CodeEditor::zoomOut
zoomOut Allows the user to zoom out from the text
Parameters:
range How much to zoom out
changeEvent
(QEvent *event) override¶changeEvent Changes the syntax highlighting when the colour palette of the window changes
event The change event
keyPressEvent
(QKeyEvent *event) override¶keyPressEvent Adds key events for zooming
Parameters:
event The key event
paintEvent
(QPaintEvent *event) override¶paintEvent Adds placeholder text
Parameters:
event The paint event
resizeEvent
(QResizeEvent *event) override¶resizeEvent Resizes the line number area when the window is resized
Parameters:
event The resize event
wheelEvent
(QWheelEvent *event) override¶wheelEvent Adds mouse wheel events for zooming
Parameters:
event The mouse wheel event
characterIsCommentedOut
(const QString &text, int pos)¶characterIsCommentedOut Checks whether the character at the given position in the given string is commented out
Parameters:
text The text to check the character in
pos The position of the character to check for in the text return Whether the character is commented out
highlightCurrentLine
()¶highlightCurrentLine Highlights the line the cursor is on
highlightParentheses
()¶highlightParentheses Highlights the parenthesis that corresponds to the one the cursor is next to
matchingParenthesisPosition
(int toMatchPos, int direction)¶matchingParenthesisPosition Finds the position of the parenthesis that matches the one on the given position in the given direction
Parameters:
toMatchPos The position in the text of the parenthesis to match with
direction In which direction to look for the matching parenthesis. Equals 1 if we need to look forward for a ‘)’, equals -1 if we need to look back for a ‘(‘.
parenthesisHighlighting
(int position)¶parenthesisHighlighting Creates a highlighting for a single character on a given position for highlighting matching parentheses
Parameters:
position The position of the character to highlight
Returns: A selection that defines a highlighted parenthesis
setFontSize
(int pixelSize)¶setFontSize Sets the font size and tab width
Parameters:
pixelSize The desired font size in pixels
mcrl2::gui::qt::CodeEditor::showContextMenu
showContextMenu Creates and shows a context menu
Parameters:
position The position where to create the context menu
mcrl2::gui::qt::CodeEditor::updateLineNumberArea
updateLineNumberArea Updates the line number area after the scrollbar has been used
Parameters:
rect The rectangle that covers the line number area
dy The amount of pixels scrolled
mcrl2::gui::qt::CodeEditor::updateLineNumberAreaWidth
updateLineNumberAreaWidth Updates the width of the line number area