# HG changeset patch
# User wenzelm
# Date 1606661923 -3600
# Node ID 164cb0806d0ab2d143da04a1ec1eb1555bcae4d6
# Parent  27a464537fb07146a02e0ae0003aec09b1ab78fc
proper positions for inlined command messages, e.g. for completion within theory header;

diff -r 27a464537fb0 -r 164cb0806d0a src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Nov 29 15:44:53 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Nov 29 15:58:43 2020 +0100
@@ -215,11 +215,11 @@
   }
 
   def check_thy(node_name: Document.Node.Name, reader: Reader[Char],
-    start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
+    command: Boolean = true, strict: Boolean = true): Document.Node.Header =
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
-        val header = Thy_Header.read(node_name, reader, start = start, strict = strict)
+        val header = Thy_Header.read(node_name, reader, command = command, strict = strict)
 
         val imports_pos =
           header.imports_pos.map({ case (s, pos) =>
@@ -335,8 +335,7 @@
             progress.expose_interrupt()
             val header =
               try {
-                val start = Token.Pos.file(name.node)
-                with_thy_reader(name, check_thy(name, _, start = start)).cat_errors(message)
+                with_thy_reader(name, check_thy(name, _, command = false)).cat_errors(message)
               }
               catch { case ERROR(msg) => cat_error(msg, message) }
             val entry = Document.Node.Entry(name, header)
diff -r 27a464537fb0 -r 164cb0806d0a src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:44:53 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:58:43 2020 +0100
@@ -214,14 +214,16 @@
   }
 
   def read(node_name: Document.Node.Name, reader: Reader[Char],
-    start: Token.Pos = Token.Pos.none,
+    command: Boolean = true,
     strict: Boolean = true): Thy_Header =
   {
     val (_, tokens0) = read_tokens(reader, true)
     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
 
-    val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
-    val pos = (start /: drop_tokens)(_.advance(_))
+    val (skip_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
+    val pos =
+      if (command) Token.Pos.command
+      else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _)
 
     Parser.parse_header(tokens, pos).check(node_name)
   }