Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/dist-template/properties/jedit.props
author wenzelm
Sat, 20 Dec 2008 17:53:00 +0100
changeset 34425 1a574ef87254
parent 34423 ec74cd63f7cb
child 34512 14d70378f1c7
permissions -rw-r--r--
tuned sidekick properties;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34334
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     1
 
#jEdit properties
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     2
 
buffer.deepIndent=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     3
 
buffer.encoding=UTF-8
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     4
 
buffer.indentSize=2
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     5
 
buffer.lineSeparator=\n
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     6
 
buffer.maxLineLen=100
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     7
 
buffer.noTabs=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     8
 
buffer.tabSize=2
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
     9
 
fallbackEncodings=US-ASCII ISO-8859-15
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    10
 
encodingDetectors=BOM XML-PI buffer-local-property
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    11
 
delete-line.shortcut=A+d
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    12
 
delete.shortcut2=C+d
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    13
 
view.antiAlias=standard
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    14
 
view.blockCaret=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    15
 
view.caretBlink=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    16
 
view.eolMarkers=false
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    17
 
view.extendedState=0
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    18
 
view.font=Lucida Sans Typewriter
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    19
 
view.fontsize=18
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    20
 
view.fracFontMetrics=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    21
 
view.gutter.fontsize=12
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    22
 
view.middleMousePaste=true
68e172602b86 essential default properties for jEdit;
wenzelm
parents:
diff changeset 
    23
 
view.showToolbar=false
34425
1a574ef87254 tuned sidekick properties;
wenzelm
parents: 34423
diff changeset 
    24
 
buffer.sidekick.keystroke-parse=true
1a574ef87254 tuned sidekick properties;
wenzelm
parents: 34423
diff changeset 
    25
 
sidekick.buffer-save-parse=true
34423
ec74cd63f7cb default docking of sidekick and isabelle-state;
wenzelm
parents: 34334
diff changeset 
    26
 
sidekick-tree.dock-position=right
ec74cd63f7cb default docking of sidekick and isabelle-state;
wenzelm
parents: 34334
diff changeset 
    27
 
isabelle-state.dock-position=bottom
isabelle