src/Tools/jEdit/etc/options
changeset 56553 f56dfc30e4b6
parent 56551 d4da2b11c729
child 56554 7bef3cd6a69c
equal deleted inserted replaced
56552:76cf86240cb7 56553:f56dfc30e4b6
    55   -- "enable spell-checker for prose words within document text"
    55   -- "enable spell-checker for prose words within document text"
    56 
    56 
    57 public option spell_checker_language : string = "en"
    57 public option spell_checker_language : string = "en"
    58   -- "language for spell-checker locale and dictionary (en, de, fr)"
    58   -- "language for spell-checker locale and dictionary (en, de, fr)"
    59 
    59 
    60 public option spell_checker_elements : string = "words,ML_comment,SML_comment"
    60 public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
    61   -- "relevant markup elements for spell-checker, separated by commas"
    61   -- "relevant markup elements for spell-checker, separated by commas"
    62 
    62 
    63 
    63 
    64 section "Rendering of Document Content"
    64 section "Rendering of Document Content"
    65 
    65 
    78 option writeln_message_color : string = "F0F0F0FF"
    78 option writeln_message_color : string = "F0F0F0FF"
    79 option information_message_color : string = "C1DFEE32"
    79 option information_message_color : string = "C1DFEE32"
    80 option tracing_message_color : string = "F0F8FFFF"
    80 option tracing_message_color : string = "F0F8FFFF"
    81 option warning_message_color : string = "EEE8AAFF"
    81 option warning_message_color : string = "EEE8AAFF"
    82 option error_message_color : string = "FFC1C1FF"
    82 option error_message_color : string = "FFC1C1FF"
    83 option spell_checker_color : string = "B22222FF"
    83 option spell_checker_color : string = "0000FFFF"
    84 option bad_color : string = "FF6A6A64"
    84 option bad_color : string = "FF6A6A64"
    85 option intensify_color : string = "FFCC6664"
    85 option intensify_color : string = "FFCC6664"
    86 option quoted_color : string = "8B8B8B19"
    86 option quoted_color : string = "8B8B8B19"
    87 option antiquoted_color : string = "FFC83219"
    87 option antiquoted_color : string = "FFC83219"
    88 option antiquote_color : string = "6600CCFF"
    88 option antiquote_color : string = "6600CCFF"