# HG changeset patch
# User wenzelm
# Date 1429129222 -7200
# Node ID 7bae727b7d89b28fdf20e4bced600c7b810921b6
# Parent  2cd500d08c3080c626bb3bb6bc3c38333cda3e43# Parent  ef5ead433951bf59f6c4cf4930b8cd1e207836b4
merged

diff -r 2cd500d08c30 -r 7bae727b7d89 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Apr 15 16:48:24 2015 +0200
+++ b/Admin/components/components.sha1	Wed Apr 15 22:20:22 2015 +0200
@@ -39,6 +39,7 @@
 ec740ee9ffd43551ddf1e5b91641405116af6291  jdk-7u6.tar.gz
 b66039bc6dc2bdb2992133743005e1e4fc58ae24  jdk-7u72.tar.gz
 d980055694ddfae430ee001c7ee877d535e97252  jdk-7u76.tar.gz
+baa6de37bb6f7a104ce5fe6506bca3d2572d601a  jdk-7u80.tar.gz
 7d5b152ac70f720bb9e783fa45ecadcf95069584  jdk-7u9.tar.gz
 5442f1015a0657259be0590b04572cd933431df7  jdk-8u11.tar.gz
 cfecb1383faaf027ffbabfcd77a0b6a6521e0969  jdk-8u20.tar.gz
diff -r 2cd500d08c30 -r 7bae727b7d89 Admin/components/main
--- a/Admin/components/main	Wed Apr 15 16:48:24 2015 +0200
+++ b/Admin/components/main	Wed Apr 15 22:20:22 2015 +0200
@@ -4,7 +4,7 @@
 e-1.8
 exec_process-1.0.3
 Haskabelle-2014
-jdk-7u76
+jdk-7u80
 jedit_build-20150228
 jfreechart-1.0.14-1
 jortho-1.0-2
diff -r 2cd500d08c30 -r 7bae727b7d89 Admin/java/build
--- a/Admin/java/build	Wed Apr 15 16:48:24 2015 +0200
+++ b/Admin/java/build	Wed Apr 15 22:20:22 2015 +0200
@@ -11,8 +11,8 @@
 
 ## parameters
 
-VERSION="7u76"
-FULL_VERSION="1.7.0_76"
+VERSION="7u80"
+FULL_VERSION="1.7.0_80"
 
 ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
 ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
@@ -35,7 +35,7 @@
 for the original downloads, which are covered by the Oracle Binary
 Code License Agreement for Java SE.
 
-Linux, Mac OS X, Windows work uniformly, depending on certain
+Linux, Windows Mac OS X, work uniformly, depending on certain
 platform-specific subdirectories.
 EOF
 
diff -r 2cd500d08c30 -r 7bae727b7d89 NEWS
--- a/NEWS	Wed Apr 15 16:48:24 2015 +0200
+++ b/NEWS	Wed Apr 15 22:20:22 2015 +0200
@@ -74,8 +74,10 @@
 * Less waste of vertical space via negative line spacing (see Global
 Options / Text Area).
 
-* Old graph browser (Java/AWT 1.1) is superseded by improved graphview
-panel, which also produces PDF output without external tools.
+* Improved graphview panel (with optional output of PNG or PDF)
+supersedes the old graph browser from 1996, but the latter remains
+available for some time as a fall-back. The old browser is still
+required for the massive graphs produced by 'thm_deps', for example.
 
 * Improved scheduling for asynchronous print commands (e.g. provers
 managed by the Sledgehammer panel) wrt. ongoing document processing.
diff -r 2cd500d08c30 -r 7bae727b7d89 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 15 16:48:24 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 15 22:20:22 2015 +0200
@@ -270,33 +270,22 @@
 
 (* display dependencies *)
 
-val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  let
-    val thy = Toplevel.theory_of state;
-    val thy_session = Present.session_name thy;
-  in
-    Theory.nodes_of thy
-    |> map (fn thy_node =>
-        let
-          val name = Context.theory_name thy_node;
-          val parents = map Context.theory_name (Theory.parents_of thy_node);
-          val session = Present.session_name thy_node;
-          val node =
-            Graph_Display.session_node
-              {name = name, directory = session, unfold = session = thy_session, path = ""};
-        in ((name, node), parents) end)
-    |> Graph_Display.display_graph
-  end);
+val thy_deps =
+  Toplevel.unknown_theory o
+  Toplevel.keep (fn st =>
+    let
+      val thy = Toplevel.theory_of st;
+      val parent_session = Session.get_name ();
+      val parent_loaded = is_some o Thy_Info.lookup_theory;
+    in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end);
 
-val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
-  let
-    val thy = Toplevel.theory_of state;
-  in
+val locale_deps =
+  Toplevel.unknown_theory o
+  Toplevel.keep (Toplevel.theory_of #> (fn thy =>
     Locale.pretty_locale_deps thy
     |> map (fn {name, parents, body} =>
       ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
-    |> Graph_Display.display_graph
-  end);
+    |> Graph_Display.display_graph));
 
 
 (* print theorems, terms, types etc. *)
diff -r 2cd500d08c30 -r 7bae727b7d89 src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Wed Apr 15 16:48:24 2015 +0200
+++ b/src/Pure/PIDE/session.ML	Wed Apr 15 22:20:22 2015 +0200
@@ -6,7 +6,7 @@
 
 signature SESSION =
 sig
-  val name: unit -> string
+  val get_name: unit -> string
   val welcome: unit -> string
   val get_keywords: unit -> Keyword.keywords
   val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -26,12 +26,14 @@
 val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
 val session_finished = Unsynchronized.ref false;
 
-fun name () = "Isabelle/" ^ #name (! session);
+fun get_name () = #name (! session);
+
+fun description () = "Isabelle/" ^ get_name ();
 
 fun welcome () =
   if Distribution.is_identified then
-    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
-  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
+    "Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")"
+  else "Unofficial version of " ^ description () ^ " (" ^ Distribution.version ^ ")";
 
 
 (* base syntax *)
@@ -44,7 +46,7 @@
 
 fun init build info info_path doc doc_output doc_variants doc_files graph_file
     parent (chapter, name) verbose =
-  if #name (! session) <> parent orelse not (! session_finished) then
+  if get_name () <> parent orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
   else
     let
diff -r 2cd500d08c30 -r 7bae727b7d89 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Apr 15 16:48:24 2015 +0200
+++ b/src/Pure/Thy/present.ML	Wed Apr 15 22:20:22 2015 +0200
@@ -7,6 +7,7 @@
 signature PRESENT =
 sig
   val session_name: theory -> string
+  val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
   val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
   val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -54,6 +55,28 @@
 val session_name = #name o Browser_Info.get;
 
 
+(* session graph *)
+
+fun session_graph parent_session parent_loaded =
+  let
+    val parent_session_name = "session." ^ parent_session;
+    val parent_session_node = Graph_Display.content_node ("[" ^ parent_session ^ "]") [];
+    fun node_name name = if parent_loaded name then parent_session_name else "theory." ^ name;
+    fun theory_entry thy =
+      let
+        val name = Context.theory_name thy;
+        val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
+      in
+        if parent_loaded name then NONE
+        else SOME ((node_name name, Graph_Display.content_node name []), deps)
+      end;
+  in
+    fn thy =>
+      ((parent_session_name, parent_session_node), []) ::
+        map_filter theory_entry (Theory.nodes_of thy)
+  end;
+
+
 
 (** global browser info state **)
 
@@ -366,4 +389,3 @@
   end);
 
 end;
-
diff -r 2cd500d08c30 -r 7bae727b7d89 src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Wed Apr 15 16:48:24 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Wed Apr 15 22:20:22 2015 +0200
@@ -17,6 +17,9 @@
 
 fun thm_deps thy thms =
   let
+    fun make_node name directory =
+      Graph_Display.session_node
+       {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
     fun add_dep ("", _, _) = I
       | add_dep (name, _, PBody {thms = thms', ...}) =
           let
@@ -30,16 +33,17 @@
                         "" => []
                       | session => [session])
                   | NONE => [])
-               | _ => ["global"]);
-            val directory = space_implode "/" (session @ prefix);
-            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
-          in
-            cons ((name, Graph_Display.session_node
-              {name = Long_Name.base_name name, directory = directory,
-                unfold = false, path = ""}), parents)
-          end;
+              | _ => ["global"]);
+            val node = make_node name (space_implode "/" (session @ prefix));
+            val deps = filter_out (fn s => s = "") (map (#1 o #2) thms');
+          in Symtab.update (name, (node, deps)) end;
+    val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
+    val entries1 =
+      Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab =>
+        if Symtab.defined tab d then tab
+        else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
   in
-    Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []
+    Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
     |> Graph_Display.display_graph
   end;
 
@@ -120,4 +124,3 @@
           end)));
 
 end;
-