equal
deleted
inserted
replaced
179 expand-abbrev.shortcut2=CA+SPACE |
179 expand-abbrev.shortcut2=CA+SPACE |
180 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII |
180 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII |
181 firstTime=false |
181 firstTime=false |
182 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX |
182 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX |
183 foldPainter=Circle |
183 foldPainter=Circle |
|
184 gatchan.highlight.overview=false |
184 home.shortcut= |
185 home.shortcut= |
185 insert-newline-indent.shortcut= |
186 insert-newline-indent.shortcut= |
186 insert-newline.shortcut=ENTER |
187 insert-newline.shortcut=ENTER |
187 isabelle-debugger.dock-position=floating |
188 isabelle-debugger.dock-position=floating |
188 isabelle-documentation.dock-position=right |
189 isabelle-documentation.dock-position=right |