src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34623 a356a8ee6f00
parent 34618 e45052ff7233
child 34624 5e4f33d033ba
equal deleted inserted replaced
34622:b1b88879c515 34623:a356a8ee6f00
    27 {
    27 {
    28   /* name */
    28   /* name */
    29 
    29 
    30   val NAME = "Isabelle"
    30   val NAME = "Isabelle"
    31   val VFS_PREFIX = "isabelle:"
    31   val VFS_PREFIX = "isabelle:"
       
    32 
       
    33   val ISABELLE_ENCODING = "UTF-8-Isabelle"
    32 
    34 
    33 
    35 
    34   /* properties */
    36   /* properties */
    35 
    37 
    36   val OPTION_PREFIX = "options.isabelle."
    38   val OPTION_PREFIX = "options.isabelle."