# 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(_)))) }