equal
deleted
inserted
replaced
62 |
62 |
63 def node_header(): Document.Node_Header = |
63 def node_header(): Document.Node_Header = |
64 { |
64 { |
65 Swing_Thread.require() |
65 Swing_Thread.require() |
66 if (Isabelle.jedit_buffer(name.node) == Some(buffer)) |
66 if (Isabelle.jedit_buffer(name.node) == Some(buffer)) |
67 Exn.capture { session.thy_load.check_thy(name) } |
67 Exn.capture { Isabelle.thy_load.check_thy(name) } |
68 else Exn.Exn(ERROR("Bad theory header")) // FIXME odd race condition!? |
68 else Exn.Exn(ERROR("Bad theory header")) // FIXME odd race condition!? |
69 } |
69 } |
70 |
70 |
71 |
71 |
72 /* perspective */ |
72 /* perspective */ |