--- 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
--- 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
--- 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
--- 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.
--- 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. *)
--- 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
--- 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;
-
--- 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;
-