equal
deleted
inserted
replaced
38 |
38 |
39 @volatile var session: Session = new Session(JEdit_Resources.empty) |
39 @volatile var session: Session = new Session(JEdit_Resources.empty) |
40 |
40 |
41 def resources(): JEdit_Resources = |
41 def resources(): JEdit_Resources = |
42 session.resources.asInstanceOf[JEdit_Resources] |
42 session.resources.asInstanceOf[JEdit_Resources] |
43 |
|
44 def debugger: Debugger = session.debugger |
|
45 |
43 |
46 |
44 |
47 /* current document content */ |
45 /* current document content */ |
48 |
46 |
49 def snapshot(view: View): Document.Snapshot = GUI_Thread.now |
47 def snapshot(view: View): Document.Snapshot = GUI_Thread.now |