src/Pure/Thy/present.scala
changeset 65344 b99283eed13c
parent 65089 1d219d76873b
child 65376 4ad983094226
equal deleted inserted replaced
65343:0a8e30a7b10e 65344:b99283eed13c
    48   private def read_sessions(dir: Path): List[(String, String)] =
    48   private def read_sessions(dir: Path): List[(String, String)] =
    49   {
    49   {
    50     val path = dir + sessions_path
    50     val path = dir + sessions_path
    51     if (path.is_file) {
    51     if (path.is_file) {
    52       import XML.Decode._
    52       import XML.Decode._
    53       list(pair(string, string))(YXML.parse_body(File.read(path)))
    53       list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
    54     }
    54     }
    55     else Nil
    55     else Nil
    56   }
    56   }
    57 
    57 
    58   private def write_sessions(dir: Path, sessions: List[(String, String)])
    58   private def write_sessions(dir: Path, sessions: List[(String, String)])