equal
deleted
inserted
replaced
48 case None => null |
48 case None => null |
49 case Some(elems) => |
49 case Some(elems) => |
50 val sessions = JEdit_Sessions.sessions_structure() |
50 val sessions = JEdit_Sessions.sessions_structure() |
51 elems match { |
51 elems match { |
52 case Nil => |
52 case Nil => |
53 sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray |
53 sessions.chapters.sortBy(_.name).map(ch => make_entry(ch.name, is_dir = true)).toArray |
54 case List(chapter) => |
54 case List(chapter) => |
55 sessions.chapters.get(chapter) match { |
55 sessions.chapters.find(_.name == chapter) match { |
56 case None => null |
56 case None => null |
57 case Some(infos) => |
57 case Some(chapter_info) => |
58 infos.map(info => { |
58 chapter_info.sessions.map { session => |
59 val name = chapter + "/" + info.name |
59 val pos = sessions(session).pos |
|
60 val name = chapter_info.name + "/" + session |
60 val path = |
61 val path = |
61 Position.File.unapply(info.pos) match { |
62 Position.File.unapply(pos) match { |
62 case Some(path) => File.platform_path(path) |
63 case Some(path) => File.platform_path(path) |
63 case None => null |
64 case None => null |
64 } |
65 } |
65 val marker = |
66 val marker = |
66 Position.Line.unapply(info.pos) match { |
67 Position.Line.unapply(pos) match { |
67 case Some(line) => "+line:" + line |
68 case Some(line) => "+line:" + line |
68 case None => null |
69 case None => null |
69 } |
70 } |
70 new Session_Entry(name, path, marker) |
71 new Session_Entry(name, path, marker) |
71 }).toArray |
72 }.toArray |
72 } |
73 } |
73 case _ => null |
74 case _ => null |
74 } |
75 } |
75 } |
76 } |
76 } |
77 } |