# HG changeset patch
# User wenzelm
# Date 1567417587 -7200
# Node ID f164cec7ac22c21c4e0733db1faba2d3f69c2cf2
# Parent  4c98d37e14482ade91000989dd27649c608a5595
clarified signature: prefer operations without position;

diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -512,16 +512,16 @@
       // inlined errors
       case Thy_Header.THEORY =>
         val reader = Scan.char_reader(Token.implode(span.content))
-        val imports = resources.check_thy_reader(node_name, reader).imports
+        val imports_pos = resources.check_thy_reader(node_name, reader).imports_pos
         val raw_imports =
           try {
-            val imports1 = Thy_Header.read(reader, Token.Pos.none).imports
-            if (imports.length == imports1.length) imports1.map(_._1) else error("")
+            val read_imports = Thy_Header.read(reader, Token.Pos.none).imports
+            if (imports_pos.length == read_imports.length) read_imports else error("")
           }
-          catch { case exn: Throwable => List.fill(imports.length)("") }
+          catch { case exn: Throwable => List.fill(imports_pos.length)("") }
 
         val errors =
-          for { ((import_name, pos), s) <- imports zip raw_imports if !can_import(import_name) }
+          for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
           yield {
             val completion =
               if (Thy_Header.is_base_name(s)) {
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -81,11 +81,13 @@
     /* header and name */
 
     sealed case class Header(
-      imports: List[(Name, Position.T)] = Nil,
+      imports_pos: List[(Name, Position.T)] = Nil,
       keywords: Thy_Header.Keywords = Nil,
       abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil)
     {
+      def imports: List[Name] = imports_pos.map(_._1)
+
       def append_errors(msgs: List[String]): Header =
         copy(errors = errors ::: msgs)
 
@@ -141,8 +143,6 @@
     {
       def map(f: String => String): Entry = copy(name = name.map(f))
 
-      def imports: List[Node.Name] = header.imports.map(_._1)
-
       override def toString: String = name.toString
     }
 
@@ -384,7 +384,7 @@
     def + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
-      val imports = node.header.imports.map(_._1)
+      val imports = node.header.imports
       val graph1 =
         (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -109,9 +109,8 @@
           if (commit.isDefined) {
             (already_committed /: dep_theories)({ case (committed, name) =>
               def parents_committed: Boolean =
-                version.nodes(name).header.imports.forall({ case (parent, _) =>
-                  resources.session_base.loaded_theory(parent) || committed.isDefinedAt(parent)
-                })
+                version.nodes(name).header.imports.forall(parent =>
+                  resources.session_base.loaded_theory(parent) || committed.isDefinedAt(parent))
               if (!committed.isDefinedAt(name) && parents_committed &&
                   state.node_consolidated(version, name))
               {
@@ -398,7 +397,7 @@
       {
         val entries =
           for ((name, theory) <- theories.toList)
-          yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_)))
+          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_)))
         Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering)
       }
 
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -301,7 +301,7 @@
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = File.standard_url(name.master_dir)
-              val imports = header.imports.map({ case (a, _) => a.node })
+              val imports = header.imports.map(_.node)
               val keywords =
                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
               (Nil,
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -181,20 +181,19 @@
         val header = Thy_Header.read(reader, start, strict)
 
         val base_name = node_name.theory_base_name
-        val (name, pos) = header.name
-        if (base_name != name)
-          error("Bad theory name " + quote(name) +
-            " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
-            Completion.report_theories(pos, List(base_name)))
+        if (base_name != header.name)
+          error("Bad theory name " + quote(header.name) +
+            " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) +
+            Completion.report_theories(header.pos, List(base_name)))
 
-        val imports =
-          header.imports.map({ case (s, pos) =>
+        val imports_pos =
+          header.imports_pos.map({ case (s, pos) =>
             val name = import_name(node_name, s)
             if (Sessions.exclude_theory(name.theory_base_name))
               error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
             (name, pos)
           })
-        Document.Node.Header(imports, header.keywords, header.abbrevs)
+        Document.Node.Header(imports_pos, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }
@@ -309,7 +308,7 @@
               try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
               catch { case ERROR(msg) => cat_error(msg, message) }
             val entry = Document.Node.Entry(name, header)
-            dependencies1.require_thys(adjunct, header.imports,
+            dependencies1.require_thys(adjunct, header.imports_pos,
               initiators = name :: initiators, progress = progress).cons(entry)
           }
           catch {
@@ -342,7 +341,7 @@
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       (session_base.loaded_theories /: entries)({ case (graph, entry) =>
         val name = entry.name.theory
-        val imports = entry.header.imports.map(p => p._1.theory)
+        val imports = entry.header.imports.map(_.theory)
 
         val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
         val graph2 = (graph1 /: imports)(_.add_edge(_, name))
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -123,7 +123,7 @@
     {
       val entries =
         for ((_, entry) <- theories.toList)
-        yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp._1.theory).name))
+        yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name))
       Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering)
     }
 
@@ -361,9 +361,7 @@
               (graph0 /: dependencies.entries)(
                 { case (g, entry) =>
                     val a = node(entry.name)
-                    val bs =
-                      entry.header.imports.map({ case (name, _) => node(name) }).
-                        filterNot(_ == a)
+                    val bs = entry.header.imports.map(node).filterNot(_ == a)
                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
             }
 
@@ -375,7 +373,7 @@
 
             val used_theories =
               for ((options, name) <- dependencies.adjunct_theories)
-              yield ((name, options), known.theories(name.theory).imports)
+              yield ((name, options), known.theories(name.theory).header.imports)
 
             val sources_errors =
               for (p <- session_files if !p.is_file) yield "No such file: " + p
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -224,7 +224,12 @@
 }
 
 sealed case class Thy_Header(
-  name: (String, Position.T),
-  imports: List[(String, Position.T)],
+  name_pos: (String, Position.T),
+  imports_pos: List[(String, Position.T)],
   keywords: Thy_Header.Keywords,
   abbrevs: Thy_Header.Abbrevs)
+{
+  def name: String = name_pos._1
+  def pos: Position.T = name_pos._2
+  def imports: List[String] = imports_pos.map(_._1)
+}
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -82,7 +82,7 @@
           node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
         if (update_header) {
           val node1 = node.update_header(header)
-          if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
+          if (node.header.imports != node1.header.imports ||
               node.header.keywords != node1.header.keywords ||
               node.header.abbrevs != node1.header.abbrevs ||
               node.header.errors != node1.header.errors) syntax_changed0 += name
@@ -102,8 +102,7 @@
           val header = node.header
           val imports_syntax =
             if (header.imports.nonEmpty) {
-              Outer_Syntax.merge(
-                header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
+              Outer_Syntax.merge(header.imports.map(resources.session_base.node_syntax(nodes, _)))
             }
             else resources.session_base.overall_syntax
           Some(imports_syntax + header)
diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/Tools/imports.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -191,7 +191,7 @@
               (for {
                 name <- session_base.known.theories_local.iterator.map(p => p._2.name)
                 if session_base.theory_qualifier(name) == info.name
-                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
+                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports_pos
                 upd <- update_name(session_base.overall_syntax.keywords, pos,
                   standard_import(session_base.theory_qualifier(name), name.master_dir, _))
               } yield upd).toList