# HG changeset patch
# User wenzelm
# Date 1483818277 -3600
# Node ID c97296294f6dc7c041043a2a94f8e061efdf5efc
# Parent  e78b62c289bb77916c58baa338b104e38e74e9a3
clarified check_thy_reader: check node_name here;

diff -r e78b62c289bb -r c97296294f6d src/Pure/PIDE/resources.scala
--- 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
 
diff -r e78b62c289bb -r c97296294f6d src/Tools/VSCode/src/document_model.scala
--- 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 */
diff -r e78b62c289bb -r c97296294f6d src/Tools/jEdit/src/document_model.scala
--- 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
-    }
   }