# HG changeset patch
# User wenzelm
# Date 1483269651 -3600
# Node ID 00f3c4bef2e07af2826b908fda98b22cfe799569
# Parent  84192ecae5827d31f6522015cf3a58398cb54ccb
tuned signature;

diff -r 84192ecae582 -r 00f3c4bef2e0 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Jan 01 12:10:21 2017 +0100
+++ b/src/Pure/Tools/build.scala	Sun Jan 01 12:20:51 2017 +0100
@@ -95,13 +95,19 @@
 
   /* source dependencies and static content */
 
+  object Session_Content
+  {
+    def empty: Session_Content =
+      Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty, Nil, Graph_Display.empty_graph)
+  }
+
   sealed case class Session_Content(
-    loaded_theories: Set[String] = Set.empty,
-    known_theories: Map[String, Document.Node.Name] = Map.empty,
-    keywords: Thy_Header.Keywords = Nil,
-    syntax: Outer_Syntax = Outer_Syntax.empty,
-    sources: List[(Path, SHA1.Digest)] = Nil,
-    session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+    loaded_theories: Set[String],
+    known_theories: Map[String, Document.Node.Name],
+    keywords: Thy_Header.Keywords,
+    syntax: Outer_Syntax,
+    sources: List[(Path, SHA1.Digest)],
+    session_graph: Graph_Display.Graph)
 
   sealed case class Deps(deps: Map[String, Session_Content])
   {
diff -r 84192ecae582 -r 00f3c4bef2e0 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Sun Jan 01 12:10:21 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sun Jan 01 12:20:51 2017 +0100
@@ -85,7 +85,7 @@
       try {
         Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
       }
-      catch { case ERROR(_) => Build.Session_Content() }
+      catch { case ERROR(_) => Build.Session_Content.empty }
     content.copy(known_theories =
       content.known_theories.mapValues(name => name.map(File.platform_path(_))))
   }