proper meta_digest: avoid non-portable position information;

--- a/src/Pure/Thy/sessions.scala	Thu Nov 19 22:05:34 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Nov 20 12:00:08 2020 +0100
@@ -577,7 +577,8 @@
       val meta_digest =
         SHA1.digest(
           (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
-            entry.theories_no_position, conditions, entry.document_theories, entry.document_files)
+            entry.theories_no_position, conditions, entry.document_theories_no_position,
+            entry.document_files)
           .toString)
 
       Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
@@ -877,6 +878,8 @@
   {
     def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
       theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
+    def document_theories_no_position: List[String] =
+      document_theories.map(_._1)
   }
 
   private object Parser extends Options.Parser