# HG changeset patch
# User wenzelm
# Date 1483814200 -3600
# Node ID 78df3d65a1cc518cf5f175364f6d8e91ee8472ee
# Parent  c8bac4b0ef079f983344201f29076a6634c42653
tuned signature;

diff -r c8bac4b0ef07 -r 78df3d65a1cc src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Jan 07 17:32:11 2017 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Jan 07 19:36:40 2017 +0100
@@ -351,8 +351,8 @@
       // inlined errors
       case Thy_Header.THEORY =>
         val header =
-          resources.check_thy_reader("", node_name,
-            new CharSequenceReader(Token.implode(span.content)), Token.Pos.command)
+          resources.check_thy_reader(
+            "", node_name, new CharSequenceReader(Token.implode(span.content)))
         val errors =
           for ((imp, pos) <- header.imports if !can_import(imp)) yield {
             val msg =
diff -r c8bac4b0ef07 -r 78df3d65a1cc src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Jan 07 17:32:11 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Jan 07 19:36:40 2017 +0100
@@ -118,7 +118,7 @@
   }
 
   def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
-    reader: Reader[Char], start: Token.Pos): Document.Node.Header =
+    reader: Reader[Char], start: Token.Pos = Token.Pos.command): Document.Node.Header =
   {
     if (reader.source.length > 0) {
       try {
@@ -140,7 +140,7 @@
     else Document.Node.no_header
   }
 
-  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos)
+  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos = Token.Pos.command)
     : Document.Node.Header =
     with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
 
diff -r c8bac4b0ef07 -r 78df3d65a1cc src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 17:32:11 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 19:36:40 2017 +0100
@@ -47,8 +47,7 @@
     resources.special_header(node_name) getOrElse
     {
       if (is_theory)
-        resources.check_thy_reader(
-          "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
+        resources.check_thy_reader("", node_name, new CharSequenceReader(doc.text))
       else Document.Node.no_header
     }
 
diff -r c8bac4b0ef07 -r 78df3d65a1cc src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 17:32:11 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 19:36:40 2017 +0100
@@ -242,8 +242,7 @@
     PIDE.resources.special_header(node_name) getOrElse
     {
       if (is_theory)
-        PIDE.resources.check_thy_reader(
-          "", node_name, new CharSequenceReader(content.text), Token.Pos.command)
+        PIDE.resources.check_thy_reader("", node_name, new CharSequenceReader(content.text))
       else Document.Node.no_header
     }
 
@@ -320,7 +319,7 @@
               case Some(offset) =>
                 val length = buffer.getLength - offset
                 PIDE.resources.check_thy_reader("", node_name,
-                  new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
+                  new CharSequenceReader(buffer.getSegment(offset, length)))
               case None =>
                 Document.Node.no_header
             }