equal
deleted
inserted
replaced
236 { |
236 { |
237 /* header */ |
237 /* header */ |
238 |
238 |
239 def node_header: Document.Node.Header = |
239 def node_header: Document.Node.Header = |
240 PIDE.resources.special_header(node_name) getOrElse |
240 PIDE.resources.special_header(node_name) getOrElse |
241 { |
241 PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false) |
242 if (is_theory) |
|
243 PIDE.resources.check_thy_reader( |
|
244 "", node_name, Scan.char_reader(content.text), strict = false) |
|
245 else Document.Node.no_header |
|
246 } |
|
247 |
242 |
248 |
243 |
249 /* content */ |
244 /* content */ |
250 |
245 |
251 def get_blob: Option[Document.Blob] = |
246 def get_blob: Option[Document.Blob] = |
303 def node_header(): Document.Node.Header = |
298 def node_header(): Document.Node.Header = |
304 { |
299 { |
305 GUI_Thread.require {} |
300 GUI_Thread.require {} |
306 |
301 |
307 PIDE.resources.special_header(node_name) getOrElse |
302 PIDE.resources.special_header(node_name) getOrElse |
308 { |
303 JEdit_Lib.buffer_lock(buffer) { |
309 if (is_theory) { |
304 PIDE.resources.check_thy_reader( |
310 JEdit_Lib.buffer_lock(buffer) { |
305 "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false) |
311 PIDE.resources.check_thy_reader( |
306 } |
312 "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false) |
|
313 } |
|
314 } |
|
315 else Document.Node.no_header |
|
316 } |
|
317 } |
307 } |
318 |
308 |
319 |
309 |
320 /* perspective */ |
310 /* perspective */ |
321 |
311 |