equal
deleted
inserted
replaced
58 |
58 |
59 class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name) |
59 class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name) |
60 { |
60 { |
61 /* header */ |
61 /* header */ |
62 |
62 |
63 def node_header(): Exn.Result[Thy_Header] = |
63 def node_header(): Document.Node_Header = |
64 { |
64 { |
65 Swing_Thread.require() |
65 Swing_Thread.require() |
66 Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) } |
66 // FIXME assert(Isabelle.jedit_buffer(name.node) == Some(buffer)) |
|
67 Exn.capture { session.thy_load.check_thy(name) } |
67 } |
68 } |
68 |
69 |
69 |
70 |
70 /* perspective */ |
71 /* perspective */ |
71 |
72 |