# HG changeset patch
# User wenzelm
# Date 1489571034 -3600
# Node ID 8b776d12f6c05c6eff81017918b14646356346c1
# Parent  4b0a43afc3fb6275766c8cf22e78b2071196f996
map values statically;

diff -r 4b0a43afc3fb -r 8b776d12f6c0 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Mar 15 10:31:42 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Mar 15 10:43:54 2017 +0100
@@ -84,7 +84,8 @@
     val base =
       try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
       catch { case ERROR(_) => Sessions.Base.empty }
-    base.copy(known_theories = base.known_theories.mapValues(a => a.map(File.platform_path(_))))
+    base.copy(known_theories =
+      for ((a, b) <- base.known_theories) yield (a, b.map(File.platform_path(_))))
   }