src/Tools/jEdit/src/plugin.scala
changeset 43670 7f933761764b
parent 43661 39fdbd814c7f
child 43697 77ce24aa1770
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Jul 05 21:20:24 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Jul 05 21:32:48 2011 +0200
     1.3 @@ -300,7 +300,7 @@
     1.4    def start_session()
     1.5    {
     1.6      val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
     1.7 -    val modes = Isabelle_System.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
     1.8 +    val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     1.9      val logic = {
    1.10        val logic = Property("logic")
    1.11        if (logic != null && logic != "") logic