blob: 43883c5ff21ed57f7d71042456a5891aa7c89677 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
binding "text" {
bind "<ctrl>k" { "set-anchor" ()
"move-cursor" (display-lines,1,0)
"cut-clipboard" ()
}
bind "<ctrl>x" { }
bind "F13" {"insert-at-cursor" ("∀")}
bind "F14" {"insert-at-cursor" ("∃")}
}
class "GtkTextView" binding "text"
style "views" {
font_name = "Monospace 10"
}
class "GtkTextView" style "views"
widget "*.*.*.*.*.ScriptWindow" style "views"
widget "*.*.*.*.GoalWindow" style "views"
widget "*.*.*.*.MessageWindow" style "views"
style "menu" {
font_name = "Serif 10"
}
class "GtkLabel" style "menu"
gtk-key-theme-name = "Emacs"
|
