--- a/src/Pure/PIDE/resources.scala Sat Jan 07 20:37:48 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Jan 07 20:44:37 2017 +0100
@@ -121,7 +121,7 @@
reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
: Document.Node.Header =
{
- if (reader.source.length > 0) {
+ if (node_name.is_theory && reader.source.length > 0) {
try {
val header = Thy_Header.read(reader, start, strict).decode_symbols
--- a/src/Tools/VSCode/src/document_model.scala Sat Jan 07 20:37:48 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Sat Jan 07 20:44:37 2017 +0100
@@ -43,11 +43,7 @@
def node_header: Document.Node.Header =
resources.special_header(node_name) getOrElse
- {
- if (is_theory)
- resources.check_thy_reader("", node_name, Scan.char_reader(doc.text))
- else Document.Node.no_header
- }
+ resources.check_thy_reader("", node_name, Scan.char_reader(doc.text))
/* perspective */
--- a/src/Tools/jEdit/src/document_model.scala Sat Jan 07 20:37:48 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sat Jan 07 20:44:37 2017 +0100
@@ -238,12 +238,7 @@
def node_header: Document.Node.Header =
PIDE.resources.special_header(node_name) getOrElse
- {
- if (is_theory)
- PIDE.resources.check_thy_reader(
- "", node_name, Scan.char_reader(content.text), strict = false)
- else Document.Node.no_header
- }
+ PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
/* content */
@@ -305,15 +300,10 @@
GUI_Thread.require {}
PIDE.resources.special_header(node_name) getOrElse
- {
- if (is_theory) {
- JEdit_Lib.buffer_lock(buffer) {
- PIDE.resources.check_thy_reader(
- "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
- }
+ JEdit_Lib.buffer_lock(buffer) {
+ PIDE.resources.check_thy_reader(
+ "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
}
- else Document.Node.no_header
- }
}