2012-01-07 18:36:58 +01:00
|
|
|
TerminalLabel < UILabel
|
2013-02-28 22:39:27 +01:00
|
|
|
font: terminus-10px
|
2012-03-26 20:33:00 +02:00
|
|
|
text-wrap: true
|
|
|
|
text-auto-resize: true
|
2013-02-28 22:39:27 +01:00
|
|
|
phantom: true
|
|
|
|
|
|
|
|
TerminalSelectText < UITextEdit
|
|
|
|
font: terminus-10px
|
|
|
|
text-wrap: true
|
|
|
|
text-align: bottomLeft
|
|
|
|
editable: false
|
|
|
|
change-cursor-image: false
|
|
|
|
cursor-visible: false
|
|
|
|
selection-color: black
|
|
|
|
selection-background-color: white
|
|
|
|
color: alpha
|
|
|
|
focusable: false
|
|
|
|
auto-scroll: false
|
2011-08-20 22:30:41 +02:00
|
|
|
|
2012-03-26 20:33:00 +02:00
|
|
|
UIWindow
|
|
|
|
id: terminalWindow
|
2011-08-20 22:30:41 +02:00
|
|
|
background-color: #000000
|
2012-01-10 23:13:40 +01:00
|
|
|
opacity: 0.85
|
2012-03-26 20:33:00 +02:00
|
|
|
clipping: true
|
2011-08-20 22:30:41 +02:00
|
|
|
anchors.fill: parent
|
2013-03-01 00:10:36 +01:00
|
|
|
border: 0 white
|
|
|
|
$on:
|
|
|
|
border: 1 black
|
|
|
|
|
|
|
|
Label
|
|
|
|
id: titleBar
|
|
|
|
!text: tr('Terminal')
|
|
|
|
border: 1 black
|
|
|
|
color: white
|
|
|
|
anchors.top: parent.top
|
|
|
|
anchors.left: parent.left
|
|
|
|
anchors.right: parent.right
|
|
|
|
background-color: #ffffff11
|
|
|
|
text-align: left
|
|
|
|
text-offset: 4 0
|
|
|
|
height: 18
|
|
|
|
visible: false
|
2011-08-20 22:30:41 +02:00
|
|
|
|
2013-02-28 22:39:27 +01:00
|
|
|
ScrollablePanel
|
2013-03-01 01:35:14 +01:00
|
|
|
id: terminalBuffer
|
2011-10-31 07:04:08 +01:00
|
|
|
focusable: false
|
2011-08-29 01:04:36 +02:00
|
|
|
anchors.left: parent.left
|
2013-02-28 22:39:27 +01:00
|
|
|
anchors.right: terminalScroll.left
|
2013-03-01 00:10:36 +01:00
|
|
|
anchors.top: terminalScroll.top
|
2015-03-07 16:32:45 +01:00
|
|
|
anchors.bottom: commandTextEdit.top
|
2013-03-01 01:35:14 +01:00
|
|
|
layout:
|
|
|
|
type: verticalBox
|
|
|
|
align-bottom: true
|
2013-02-28 22:39:27 +01:00
|
|
|
vertical-scrollbar: terminalScroll
|
|
|
|
inverted-scroll: true
|
2011-11-17 22:41:02 +01:00
|
|
|
margin-left: 2
|
2011-08-29 01:04:36 +02:00
|
|
|
|
2013-03-01 01:35:14 +01:00
|
|
|
TerminalSelectText
|
|
|
|
id: terminalSelectText
|
|
|
|
anchors.fill: terminalBuffer
|
|
|
|
focusable: false
|
2013-02-28 22:39:27 +01:00
|
|
|
|
|
|
|
VerticalScrollBar
|
|
|
|
id: terminalScroll
|
|
|
|
anchors.top: parent.top
|
|
|
|
anchors.bottom: parent.bottom
|
|
|
|
anchors.right: parent.right
|
|
|
|
step: 48
|
|
|
|
pixels-scroll: true
|
|
|
|
|
2011-08-20 22:30:41 +02:00
|
|
|
UILabel
|
2011-08-23 03:08:36 +02:00
|
|
|
id: commandSymbolLabel
|
2013-02-28 22:39:27 +01:00
|
|
|
size: 12 12
|
2011-11-17 22:41:02 +01:00
|
|
|
fixed-size: true
|
2011-08-20 22:30:41 +02:00
|
|
|
anchors.bottom: parent.bottom
|
|
|
|
anchors.left: parent.left
|
2011-11-17 22:41:02 +01:00
|
|
|
margin-left: 2
|
2013-02-28 22:39:27 +01:00
|
|
|
font: terminus-10px
|
2012-05-11 11:13:44 +02:00
|
|
|
text: >
|
2011-08-20 22:30:41 +02:00
|
|
|
|
2012-03-31 15:43:01 +02:00
|
|
|
UITextEdit
|
|
|
|
id: commandTextEdit
|
2015-03-07 16:32:45 +01:00
|
|
|
background: #aaaaaa11
|
|
|
|
border-color: #aaaaaa88
|
|
|
|
&baseHeight: 12
|
2011-08-20 22:30:41 +02:00
|
|
|
anchors.bottom: parent.bottom
|
2011-08-26 17:06:52 +02:00
|
|
|
anchors.left: commandSymbolLabel.right
|
2015-03-07 16:32:45 +01:00
|
|
|
anchors.right: terminalScroll.left
|
2013-02-28 22:39:27 +01:00
|
|
|
margin-left: 1
|
2015-03-07 16:32:45 +01:00
|
|
|
padding-left: 2
|
2013-02-28 22:39:27 +01:00
|
|
|
font: terminus-10px
|
2013-01-25 12:44:15 +01:00
|
|
|
selection-color: black
|
|
|
|
selection-background-color: white
|
2015-03-07 16:32:45 +01:00
|
|
|
border-width-left: 0
|
|
|
|
border-width-top: 0
|
|
|
|
multiline: false
|
|
|
|
|
|
|
|
$on:
|
|
|
|
border-width-left: 1
|
|
|
|
border-width-top: 1
|
|
|
|
multiline: true
|
2012-03-26 20:33:00 +02:00
|
|
|
|
2012-03-27 00:24:01 +02:00
|
|
|
ResizeBorder
|
|
|
|
id: bottomResizeBorder
|
|
|
|
anchors.bottom: parent.bottom
|
|
|
|
anchors.left: parent.left
|
|
|
|
anchors.right: parent.right
|
|
|
|
enabled: false
|
|
|
|
|
|
|
|
ResizeBorder
|
|
|
|
id: rightResizeBorder
|
|
|
|
anchors.right: parent.right
|
|
|
|
anchors.top: parent.top
|
|
|
|
anchors.bottom: parent.bottom
|
|
|
|
enabled: false
|