# HG changeset patch
# User wenzelm
# Date 1507576342 -7200
# Node ID 4642cf4a7ebbcef9ce46046149e52c6d04534f95
# Parent  c0e8c199cb2e048341234580a0d087f0a520b227
tuned signature;

diff -r c0e8c199cb2e -r 4642cf4a7ebb src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Oct 09 20:26:02 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 21:12:22 2017 +0200
@@ -116,7 +116,7 @@
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
     sources: List[(Path, SHA1.Digest)] = Nil,
-    session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
+    session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil,
     imports: Option[Base] = None)
   {
@@ -253,7 +253,7 @@
                 progress, overall_syntax.keywords, check_keywords, theory_files)
             }
 
-            val session_graph: Graph_Display.Graph =
+            val session_graph_display: Graph_Display.Graph =
             {
               def session_node(name: String): Graph_Display.Node =
                 Graph_Display.Node("[" + name + "]", "session." + name)
@@ -303,7 +303,7 @@
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
                 sources = check_sources(session_files),
-                session_graph = session_graph,
+                session_graph_display = session_graph_display,
                 errors = thy_deps.errors ::: sources_errors,
                 imports = Some(imports_base))
 
diff -r c0e8c199cb2e -r 4642cf4a7ebb src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 09 20:26:02 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Oct 09 21:12:22 2017 +0200
@@ -198,7 +198,7 @@
       }
 
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
-    isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph)
+    isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
 
     private val future_result: Future[Process_Result] =
       Future.thread("build") {