# HG changeset patch
# User wenzelm
# Date 1606658235 -3600
# Node ID a9ef3904111407416da55d8edbf15ee0a3545702
# Parent  72976a6bd2ba929434d31a5eabf5e3725eebf301
clarified signature;

diff -r 72976a6bd2ba -r a9ef39041114 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Nov 29 14:27:15 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 29 14:57:15 2020 +0100
@@ -415,7 +415,7 @@
       // inlined errors
       case Thy_Header.THEORY =>
         val reader = Scan.char_reader(Token.implode(span.content))
-        val header = resources.check_thy_reader(node_name, reader)
+        val header = resources.check_thy(node_name, reader)
         val imports_pos = header.imports_pos
         val raw_imports =
           try {
diff -r 72976a6bd2ba -r a9ef39041114 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Nov 29 14:27:15 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Sun Nov 29 14:57:15 2020 +0100
@@ -600,7 +600,7 @@
           progress.expose_interrupt()
           val text0 = File.read(path)
           val text = if (unicode_symbols) Symbol.decode(text0) else text0
-          val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
+          val node_header = resources.check_thy(node_name, Scan.char_reader(text))
           new Resources.Theory(node_name, node_header, text, true)
         }
 
diff -r 72976a6bd2ba -r a9ef39041114 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Nov 29 14:27:15 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Nov 29 14:57:15 2020 +0100
@@ -216,7 +216,7 @@
     else error ("Cannot load theory file " + path)
   }
 
-  def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
+  def check_thy(node_name: Document.Node.Name, reader: Reader[Char],
     start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
   {
     if (node_name.is_theory && reader.source.length > 0) {
@@ -248,10 +248,6 @@
     else Document.Node.no_header
   }
 
-  def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
-      strict: Boolean = true): Document.Node.Header =
-    with_thy_reader(name, check_thy_reader(name, _, start, strict))
-
 
   /* special header */
 
@@ -351,7 +347,10 @@
 
             progress.expose_interrupt()
             val header =
-              try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
+              try {
+                val start = Token.Pos.file(name.node)
+                with_thy_reader(name, check_thy(name, _, start = start)).cat_errors(message)
+              }
               catch { case ERROR(msg) => cat_error(msg, message) }
             val entry = Document.Node.Entry(name, header)
             dependencies1.require_thys(adjunct, header.imports_pos,
diff -r 72976a6bd2ba -r a9ef39041114 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Sun Nov 29 14:27:15 2020 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Sun Nov 29 14:57:15 2020 +0100
@@ -99,7 +99,7 @@
 
   def node_header: Document.Node.Header =
     resources.special_header(node_name) getOrElse
-      resources.check_thy_reader(node_name, Scan.char_reader(content.text))
+      resources.check_thy(node_name, Scan.char_reader(content.text))
 
 
   /* perspective */
diff -r 72976a6bd2ba -r a9ef39041114 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 29 14:27:15 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 29 14:57:15 2020 +0100
@@ -413,7 +413,7 @@
 
   def node_header: Document.Node.Header =
     PIDE.resources.special_header(node_name) getOrElse
-      PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false)
+      PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false)
 
 
   /* content */
@@ -485,7 +485,7 @@
 
     PIDE.resources.special_header(node_name) getOrElse
       JEdit_Lib.buffer_lock(buffer) {
-        PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
+        PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
       }
   }