# HG changeset patch
# User boehmes
# Date 1420107135 -3600
# Node ID 839f4d1a74679730ae522069bf342f07e812744c
# Parent  436b7b0c94f6dc34e2f56acee954d842b58d2ab8# Parent  ecf64bc6977813369d0e1dfee297b3e10c3ac10d
merged

diff -r 436b7b0c94f6 -r 839f4d1a7467 NEWS
--- a/NEWS	Thu Jan 01 11:08:47 2015 +0100
+++ b/NEWS	Thu Jan 01 11:12:15 2015 +0100
@@ -255,6 +255,13 @@
 * Support for Proof General and Isar TTY loop has been discontinued.
 Minor INCOMPATIBILITY.
 
+* JVM system property "isabelle.threads" determines size of Scala thread
+pool, like Isabelle system option "threads" for ML.
+
+* JVM system property "isabelle.laf" determines the default Swing
+look-and-feel, via internal class name or symbolic name as in the jEdit
+menu Global Options / Appearance.
+
 * System option "pretty_margin" is superseded by "thy_output_margin",
 which is also accessible via document antiquotation option "margin".
 Only the margin for document output may be changed, but not the global
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Doc/Prog_Prove/Bool_nat_list.thy
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -159,6 +159,9 @@
 declare [[names_short]]
 (*>*)
 datatype 'a list = Nil | Cons 'a "'a list"
+(*<*)
+for map: map
+(*>*)
 
 text{*
 \begin{itemize}
@@ -395,8 +398,8 @@
 and the \indexed{@{const map}}{map} function that applies a function to all elements of a list:
 \begin{isabelle}
 \isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
-@{text"\""}@{thm list.map(1)}@{text"\" |"}\\
-@{text"\""}@{thm list.map(2)}@{text"\""}
+@{text"\""}@{thm list.map(1) [of f]}@{text"\" |"}\\
+@{text"\""}@{thm list.map(2) [of f x xs]}@{text"\""}
 \end{isabelle}
 
 \ifsem
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -297,7 +297,7 @@
 qed
 
 
-subsection  \<open>Alternative formulation\<close>
+subsection \<open>Alternative formulation\<close>
 
 text \<open>
   The following alternative formulation of the Hahn-Banach
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/Library/Quotient_Type.thy
--- a/src/HOL/Library/Quotient_Type.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/Library/Quotient_Type.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -2,63 +2,65 @@
     Author:     Markus Wenzel, TU Muenchen
 *)
 
-section {* Quotient types *}
+section \<open>Quotient types\<close>
 
 theory Quotient_Type
 imports Main
 begin
 
-text {*
- We introduce the notion of quotient types over equivalence relations
- via type classes.
-*}
+text \<open>We introduce the notion of quotient types over equivalence relations
+  via type classes.\<close>
+
 
-subsection {* Equivalence relations and quotient types *}
+subsection \<open>Equivalence relations and quotient types\<close>
 
-text {*
- \medskip Type class @{text equiv} models equivalence relations @{text
- "\<sim> :: 'a => 'a => bool"}.
-*}
+text \<open>Type class @{text equiv} models equivalence relations
+  @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close>
 
 class eqv =
-  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
+  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sim>" 50)
 
 class equiv = eqv +
   assumes equiv_refl [intro]: "x \<sim> x"
-  assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
-  assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
+    and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
+    and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
+begin
 
-lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
+lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x"
 proof -
-  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
-    by (rule contrapos_nn) (rule equiv_sym)
+  assume "\<not> x \<sim> y"
+  then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym)
 qed
 
-lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
+lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
 proof -
-  assume "\<not> (x \<sim> y)" and "y \<sim> z"
-  show "\<not> (x \<sim> z)"
+  assume "\<not> x \<sim> y" and "y \<sim> z"
+  show "\<not> x \<sim> z"
   proof
     assume "x \<sim> z"
-    also from `y \<sim> z` have "z \<sim> y" ..
+    also from \<open>y \<sim> z\<close> have "z \<sim> y" ..
     finally have "x \<sim> y" .
-    with `\<not> (x \<sim> y)` show False by contradiction
+    with \<open>\<not> x \<sim> y\<close> show False by contradiction
   qed
 qed
 
-lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
+lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
 proof -
-  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
-  also assume "x \<sim> y" then have "y \<sim> x" ..
-  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
+  assume "\<not> y \<sim> z"
+  then have "\<not> z \<sim> y" ..
+  also
+  assume "x \<sim> y"
+  then have "y \<sim> x" ..
+  finally have "\<not> z \<sim> x" .
+  then show "\<not> x \<sim> z" ..
 qed
 
-text {*
- \medskip The quotient type @{text "'a quot"} consists of all
- \emph{equivalence classes} over elements of the base type @{typ 'a}.
-*}
+end
 
-definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
+text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence
+  classes} over elements of the base type @{typ 'a}.\<close>
+
+definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
 
 typedef 'a quot = "quot :: 'a::eqv set set"
   unfolding quot_def by blast
@@ -66,38 +68,38 @@
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   unfolding quot_def by blast
 
-lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
-  unfolding quot_def by blast
+lemma quotE [elim]:
+  assumes "R \<in> quot"
+  obtains a where "R = {x. a \<sim> x}"
+  using assms unfolding quot_def by blast
 
-text {*
- \medskip Abstracted equivalence classes are the canonical
- representation of elements of a quotient type.
-*}
+text \<open>Abstracted equivalence classes are the canonical representation of
+  elements of a quotient type.\<close>
 
-definition
-  "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
-  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
+definition "class" :: "'a::equiv \<Rightarrow> 'a quot"  ("\<lfloor>_\<rfloor>")
+  where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
 
 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
 proof (cases A)
-  fix R assume R: "A = Abs_quot R"
-  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
+  fix R
+  assume R: "A = Abs_quot R"
+  assume "R \<in> quot"
+  then have "\<exists>a. R = {x. a \<sim> x}" by blast
   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
   then show ?thesis unfolding class_def .
 qed
 
-lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
+lemma quot_cases [cases type: quot]:
+  obtains a where "A = \<lfloor>a\<rfloor>"
   using quot_exhaust by blast
 
 
-subsection {* Equality on quotients *}
+subsection \<open>Equality on quotients\<close>
 
-text {*
- Equality of canonical quotient elements coincides with the original
- relation.
-*}
+text \<open>Equality of canonical quotient elements coincides with the original
+  relation.\<close>
 
-theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
+theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b"
 proof
   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   show "a \<sim> b"
@@ -131,11 +133,10 @@
 qed
 
 
-subsection {* Picking representing elements *}
+subsection \<open>Picking representing elements\<close>
 
-definition
-  pick :: "'a::equiv quot => 'a" where
-  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
+definition pick :: "'a::equiv quot \<Rightarrow> 'a"
+  where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
 
 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
 proof (unfold pick_def)
@@ -143,7 +144,8 @@
   proof (rule someI2)
     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
-    then have "a \<sim> x" .. then show "x \<sim> a" ..
+    then have "a \<sim> x" ..
+    then show "x \<sim> a" ..
   qed
 qed
 
@@ -155,17 +157,14 @@
   with a show ?thesis by simp
 qed
 
-text {*
- \medskip The following rules support canonical function definitions
- on quotient types (with up to two arguments).  Note that the
- stripped-down version without additional conditions is sufficient
- most of the time.
-*}
+text \<open>The following rules support canonical function definitions on quotient
+  types (with up to two arguments). Note that the stripped-down version
+  without additional conditions is sufficient most of the time.\<close>
 
 theorem quot_cond_function:
-  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
-    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
-      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
+  assumes eq: "\<And>X Y. P X Y \<Longrightarrow> f X Y \<equiv> g (pick X) (pick Y)"
+    and cong: "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
+      \<Longrightarrow> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> \<Longrightarrow> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"
     and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
 proof -
@@ -183,15 +182,15 @@
 qed
 
 theorem quot_function:
-  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
-    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
+  assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)"
+    and "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"
   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   using assms and TrueI
   by (rule quot_cond_function)
 
 theorem quot_function':
-  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
-    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
+  "(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow>
+    (\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow>
     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   by (rule quot_function) (simp_all only: quot_equality)
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/List.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -3836,7 +3836,7 @@
 text{* Courtesy of Matthias Daum: *}
 lemma append_replicate_commute:
   "replicate n x @ replicate k x = replicate k x @ replicate n x"
-apply (simp add: replicate_add [THEN sym])
+apply (simp add: replicate_add [symmetric])
 apply (simp add: add.commute)
 done
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -175,7 +175,7 @@
 lemma approx_stk_rev_lem:
   "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
   apply (unfold approx_stk_def approx_loc_def)
-  apply (simp add: rev_map [THEN sym])
+  apply (simp add: rev_map [symmetric])
   done
 
 lemma approx_stk_rev:
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -551,7 +551,7 @@
 apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
 apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map)
 apply (intro strip)
-apply (simp (no_asm_simp) only: append_Cons [THEN sym])
+apply (simp (no_asm_simp) only: append_Cons [symmetric])
 apply (rule progression_lvar_init_aux)
 apply (auto simp: unique_def map_of_in_set disjoint_varnames_def)
 done
@@ -648,8 +648,8 @@
 apply (rule_tac x3="fst s" and s3="snd s"and x'3="fst s'"  
   in eval_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]], simplified])
 apply assumption+
-apply (simp (no_asm_use) add: surjective_pairing [THEN sym])
-apply (simp only: surjective_pairing [THEN sym])
+apply (simp (no_asm_use) add: surjective_pairing [symmetric])
+apply (simp only: surjective_pairing [symmetric])
 apply (auto simp add: gs_def gx_def)
 done
 
@@ -662,9 +662,9 @@
 apply (frule eval_evals_exec_type_sound [THEN conjunct2 [THEN conjunct1 [THEN mp]]]) 
 apply (subgoal_tac "G \<turnstile> (gx s, (gh s, gl s)) -es[\<succ>]vs-> (gx s', (gh s', gl s'))")
 apply assumption
-apply (simp add: gx_def gh_def gl_def surjective_pairing [THEN sym])
+apply (simp add: gx_def gh_def gl_def surjective_pairing [symmetric])
 apply (case_tac E)
-apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [THEN sym])
+apply (simp add: gx_def gs_def gh_def gl_def surjective_pairing [symmetric])
 done
 
 lemma eval_of_class: "\<lbrakk> G \<turnstile> s -e\<succ>a'-> s'; E \<turnstile> e :: Class C; 
@@ -1062,7 +1062,7 @@
 apply (simp (no_asm_simp) only: env_of_jmb_fst, assumption, simp only: env_of_jmb_fst)
 
 (* establish \<exists> lc. a' = Addr lc *)
-apply (frule (5) eval_of_class, rule env_of_jmb_fst [THEN sym])
+apply (frule (5) eval_of_class, rule env_of_jmb_fst [symmetric])
 apply (subgoal_tac "G,h \<turnstile> a' ::\<preceq> Class C")
 apply (subgoal_tac "is_class G dynT")
 
@@ -1097,7 +1097,7 @@
 (* establish length pns = length pTs *)
 apply (frule method_preserves_length, assumption, assumption) 
 (* establish length pvs = length ps *)
-apply (frule evals_preserves_length [THEN sym])
+apply (frule evals_preserves_length [symmetric])
 
 (** start evaluating subexpressions **)
 apply (simp (no_asm_use) only: compExpr.simps compExprs.simps)
@@ -1179,10 +1179,10 @@
 apply (simp only: env_of_jmb_fst) 
 apply (simp add: conforms_def xconf_def gs_def)
 apply simp
-apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
+apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [symmetric])
 apply (simp (no_asm_use) only: ty_exprs_list_all2) apply simp
 apply simp
-apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [THEN sym])
+apply (simp (no_asm_use) only: gx_def gs_def surjective_pairing [symmetric])
     (* list_all2 (\<lambda>T T'. G \<turnstile> T \<preceq> T') pTsa pTs *)
     apply (rule max_spec_widen, simp only: env_of_jmb_fst)
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -89,7 +89,7 @@
 lemma map_of_rev: "unique xs \<Longrightarrow> map_of (rev xs) = map_of xs"
 apply (induct xs)
 apply simp
-apply (simp add: unique_def map_of_append map_of_as_map_upds [THEN sym]
+apply (simp add: unique_def map_of_append map_of_as_map_upds [symmetric]
                  Map.map_of_append[symmetric] del:Map.map_of_append)
 done
 
@@ -101,7 +101,7 @@
 apply (subgoal_tac "\<exists> x xr. xs = x # xr")
 apply clarify
 apply (drule_tac x=xr in spec)
-apply (simp add: map_upds_append [THEN sym])
+apply (simp add: map_upds_append [symmetric])
   (* subgoal *)
 apply (case_tac xs)
 apply auto
@@ -119,7 +119,7 @@
  apply (simp only: rev.simps)
  apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
   apply (simp split:split_if_asm)
- apply (simp add: map_upds_append [THEN sym])
+ apply (simp add: map_upds_append [symmetric])
 apply (case_tac ks)
  apply auto
 done
@@ -144,7 +144,7 @@
 apply (frule map_upds_SomeD)
 apply (rule map_upds_takeWhile)
 apply (simp (no_asm_simp))
-apply (simp add: map_upds_append [THEN sym])
+apply (simp add: map_upds_append [symmetric])
 apply (simp add: map_upds_rev)
 
   (* show length (pns @ map fst lvars) = length (pTs @ map snd lvars) *)
@@ -432,7 +432,7 @@
 \<Longrightarrow>(sttp_of (compTpInitLvars jmb lvars (ST, start_LT C pTs (length lvars))))
   = (ST, inited_LT C pTs lvars)"
 apply (simp add: start_LT_def inited_LT_def)
-apply (simp only: append_Cons [THEN sym])
+apply (simp only: append_Cons [symmetric])
 apply (rule compTpInitLvars_LT_ST_aux)
 apply (auto dest: wf_java_mdecl_length_pTs_pns wf_java_mdecl_disjoint_varnames)
 done
@@ -1288,7 +1288,7 @@
   -- {* @{text "<=s"} *}
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (simp add: wf_prog_ws_prog [THEN comp_method])
-  apply (simp add: max_spec_preserves_length [THEN sym])
+  apply (simp add: max_spec_preserves_length [symmetric])
 
   -- "@{text check_type}"
 apply (simp add: max_ssize_def ssize_sto_def)
@@ -2493,10 +2493,10 @@
 apply (rule_tac T=T and LT="inited_LT C pTs lvars" and ST=start_ST in wt_method_comp_aux)
 
   (* bc *)
-apply (simp only: append_assoc [THEN sym])
+apply (simp only: append_assoc [symmetric])
 
   (* comb *)
-apply (simp only: comb_assoc [THEN sym])
+apply (simp only: comb_assoc [symmetric])
 
   (* bc_corresp *)
 apply (rule wt_method_comp_wo_return)
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -95,7 +95,7 @@
 "(class G C = None) = (class (comp G) C = None)"
 apply (simp add: class_def comp_def compClass_def)
 apply (simp add: map_of_in_set)
-apply (simp add: image_comp [THEN sym] o_def split_beta)
+apply (simp add: image_comp [symmetric] o_def split_beta)
 done
 
 lemma comp_is_class: "is_class (comp G) C = is_class G C"
@@ -186,7 +186,7 @@
 apply (rule sym)
 apply (simp add: ws_prog_def comp_ws_cdecl comp_unique)
 apply (simp add: comp_wf_syscls)
-apply (auto simp add: comp_ws_cdecl [THEN sym] TranslComp.comp_def)
+apply (auto simp add: comp_ws_cdecl [symmetric] TranslComp.comp_def)
 done
 
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -172,10 +172,10 @@
 apply(induct_tac "vs")
  apply(clarsimp)
 apply(clarsimp)
-apply(frule list_all2_lengthD [THEN sym])
+apply(frule list_all2_lengthD [symmetric])
 apply(simp (no_asm_use) add: length_Suc_conv)
 apply(safe)
-apply(frule list_all2_lengthD [THEN sym])
+apply(frule list_all2_lengthD [symmetric])
 apply(simp (no_asm_use) add: length_Suc_conv)
 apply(clarify)
 apply(fast elim: conf_widen)
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -434,7 +434,7 @@
 apply     (simp (no_asm))
 apply     (tactic e) -- "XcptE"
 apply    (simp (no_asm))
-apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
+apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst Pair_eq, force)
 apply  (simp (no_asm))
 apply (simp (no_asm))
 apply (tactic e) -- "XcptE"
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Jan 01 11:12:15 2015 +0100
@@ -140,7 +140,7 @@
 apply(clarify)
 apply( drule (1) class_wf_struct)
 apply( unfold ws_cdecl_def)
-apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+apply(force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
 done
 
 lemma wf_cdecl_supD: 
@@ -600,7 +600,7 @@
 apply (erule disjE)
 apply (simp (no_asm_use) add: map_of_map) apply blast
 apply blast
-apply (rule trans [THEN sym], rule sym, assumption)
+apply (rule trans [symmetric], rule sym, assumption)
 apply (rule_tac x=vn in fun_cong)
 apply (rule trans, rule field_rec, assumption+)
 apply (simp (no_asm_simp) add: wf_prog_ws_prog) 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -8,15 +8,12 @@
 signature PREDICATE_COMPILE =
 sig
   val preprocess : Predicate_Compile_Aux.options -> term -> theory -> theory
-  val present_graph : bool Unsynchronized.ref
   val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
 struct
 
-val present_graph = Unsynchronized.ref false
-
 val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
 
 open Predicate_Compile_Aux;
@@ -142,7 +139,6 @@
         (fn () =>
           Predicate_Compile_Data.obtain_specification_graph options thy t
           |> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr))
-    val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
   in
     cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"
       (fn () =>
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -16,7 +16,6 @@
   val obtain_specification_graph :
     Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
 
-  val present_graph : thm list Term_Graph.T -> unit
   val normalize_equation : theory -> thm -> thm
 end;
 
@@ -298,27 +297,4 @@
     extend t Term_Graph.empty
   end;
 
-
-fun present_graph gr =
-  let
-    fun eq_cname (Const (c1, _), Const (c2, _)) = (c1 = c2)
-    fun string_of_const (Const (c, _)) = c
-      | string_of_const _ = error "string_of_const: unexpected term"
-    val constss = Term_Graph.strong_conn gr;
-    val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
-      Termtab.update (const, consts)) consts) constss;
-    fun succs consts = consts
-      |> maps (Term_Graph.immediate_succs gr)
-      |> subtract eq_cname consts
-      |> map (the o Termtab.lookup mapping)
-      |> distinct (eq_list eq_cname);
-    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-
-    fun namify consts = map string_of_const consts
-      |> commas;
-    val prgr = map (fn (consts, constss) =>
-      {name = namify consts, ID = namify consts, dir = "", unfold = true,
-       path = "", parents = map namify constss, content = [] }) conn
-  in Graph_Display.display_graph prgr end
-
 end
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -9,10 +9,12 @@
 signature LAZY =
 sig
   type 'a lazy
-  val peek: 'a lazy -> 'a Exn.result option
-  val is_finished: 'a lazy -> bool
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
+  val peek: 'a lazy -> 'a Exn.result option
+  val is_running: 'a lazy -> bool
+  val is_finished: 'a lazy -> bool
+  val finished_result: 'a lazy -> 'a Exn.result option
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
@@ -31,15 +33,36 @@
 abstype 'a lazy = Lazy of 'a expr Synchronized.var
 with
 
+fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
+fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
+
 fun peek (Lazy var) =
-  (case Synchronized.peek var of
+  (case Synchronized.value var of
     Expr _ => NONE
   | Result res => Future.peek res);
 
-fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
-fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
+
+(* status *)
+
+fun is_future pred (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => false
+  | Result res => pred res);
+
+fun is_running x = is_future (not o Future.is_finished) x;
 
-fun is_finished x = is_some (peek x);
+fun is_finished x =
+  is_future (fn res =>
+    Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
+
+fun finished_result (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => NONE
+  | Result res =>
+      if Future.is_finished res then
+        let val result = Future.join_result res
+        in if Exn.is_interrupt_exn result then NONE else SOME result end
+      else NONE);
 
 
 (* force result *)
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -17,15 +17,17 @@
 abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
 with
 
+fun lazy e = Lazy (Unsynchronized.ref (Expr e));
+fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
+
 fun peek (Lazy r) =
   (case ! r of
     Expr _ => NONE
   | Result res => SOME res);
 
-fun lazy e = Lazy (Unsynchronized.ref (Expr e));
-fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
-
+fun is_running _ = false;
 fun is_finished x = is_some (peek x);
+val finished_result = peek;
 
 
 (* force result *)
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -8,7 +8,6 @@
 sig
   type 'a var
   val var: string -> 'a -> 'a var
-  val peek: 'a var -> 'a
   val value: 'a var -> 'a
   val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
@@ -34,8 +33,6 @@
   cond = ConditionVar.conditionVar (),
   var = Unsynchronized.ref x};
 
-fun peek (Var {var, ...}) = ! var;
-
 fun value (Var {name, lock, var, ...}) =
   Multithreading.synchronized name lock (fn () => ! var);
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Concurrent/synchronized_sequential.ML
--- a/src/Pure/Concurrent/synchronized_sequential.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -11,7 +11,6 @@
 with
 
 fun var _ x = Var (Unsynchronized.ref x);
-fun peek (Var var) = ! var;
 fun value (Var var) = ! var;
 
 fun timed_access (Var var) _ f =
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -25,14 +25,19 @@
 {
   /* Swing look-and-feel */
 
+  def find_laf(name: String): Option[String] =
+    UIManager.getInstalledLookAndFeels().
+      find(c => c.getName == name || c.getClassName == name).
+      map(_.getClassName)
+
   def get_laf(): String =
-  {
-    if (Platform.is_windows || Platform.is_macos)
-      UIManager.getSystemLookAndFeelClassName()
-    else
-      UIManager.getInstalledLookAndFeels().find(_.getName == "Nimbus").map(_.getClassName)
-        .getOrElse(UIManager.getCrossPlatformLookAndFeelClassName())
-  }
+    find_laf(System.getProperty("isabelle.laf")) getOrElse {
+      if (Platform.is_windows || Platform.is_macos)
+        UIManager.getSystemLookAndFeelClassName()
+      else
+        find_laf("Nimbus") getOrElse
+          UIManager.getCrossPlatformLookAndFeelClassName()
+    }
 
   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
 
@@ -161,12 +166,6 @@
     else "<html>" + HTML.encode(text) + "</html>"
 
 
-  /* screen resolution */
-
-  def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
-  def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
-
-
   /* icon */
 
   def isabelle_icon(): ImageIcon =
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/GUI/system_dialog.scala
--- a/src/Pure/GUI/system_dialog.scala	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/GUI/system_dialog.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -78,7 +78,6 @@
     /* text */
 
     val text = new TextArea {
-      font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
       editable = false
       columns = 50
       rows = 20
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/General/graph.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -21,13 +21,15 @@
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
 
-  def make[Key, A](entries: List[((Key, A), List[Key])])(implicit ord: Ordering[Key])
-    : Graph[Key, A] =
+  def make[Key, A](entries: List[((Key, A), List[Key])], converse: Boolean = false)(
+    implicit ord: Ordering[Key]): Graph[Key, A] =
   {
     val graph1 =
       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
     val graph2 =
-      (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
+      (graph1 /: entries) { case (graph, ((x, _), ys)) =>
+        if (converse) (graph /: ys)(_.add_edge(_, x)) else (graph /: ys)(_.add_edge(x, _))
+      }
     graph2
   }
 
@@ -44,11 +46,11 @@
       list(pair(pair(key, info), list(key)))(graph.dest)
     })
 
-  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(implicit ord: Ordering[Key])
-      : XML.Decode.T[Graph[Key, A]] =
+  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A], converse: Boolean = false)(
+    implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
     ((body: XML.Body) => {
       import XML.Decode._
-      make(list(pair(pair(key, info), list(key)))(body))(ord)
+      make(list(pair(pair(key, info), list(key)))(body), converse)(ord)
     })
 }
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/General/graph_display.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -6,34 +6,66 @@
 
 signature GRAPH_DISPLAY =
 sig
-  type node =
-   {name: string, ID: string, dir: string, unfold: bool,
-    path: string, parents: string list, content: Pretty.T list}
-  type graph = node list
+  type node
+  val content_node: string -> Pretty.T list -> node
+  val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
+  type entry = (string * node) * string list
+  val eq_entry: entry * entry -> bool
+  type graph = entry list
+  val sort_graph: graph -> graph
   val write_graph_browser: Path.T -> graph -> unit
   val browserN: string
   val graphviewN: string
-  val active_graphN: string
   val display_graph: graph -> unit
 end;
 
 structure Graph_Display: GRAPH_DISPLAY =
 struct
 
-(* external graph representation *)
+(* type node *)
+
+datatype node =
+  Node of {name: string, content: Pretty.T list, unfold: bool, directory: string, path: string};
+
+fun content_node name content =
+  Node {name = name, content = content, unfold = true, directory = "", path = ""};
+
+fun session_node {name, unfold, directory, path} =
+  Node {name = name, content = [], unfold = unfold, directory = directory, path = path};
+
+
+(* type graph *)
+
+type entry = (string * node) * string list;
+val eq_entry: entry * entry -> bool = op = o apply2 (#1 o #1);
+
+type graph = entry list;
 
-type node =
- {name: string, ID: string, dir: string, unfold: bool,
-  path: string, parents: string list, content: Pretty.T list};
+structure Aux_Graph =
+  Graph(type key = string * string val ord = prod_ord string_ord string_ord);
 
-type graph = node list;
+fun sort_graph (graph: graph) =
+  let
+    val ident_names =
+      fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident)))
+        graph Symtab.empty;
+    val the_key = the o Symtab.lookup ident_names;
+    val G =
+      Aux_Graph.empty
+      |> fold (fn ((ident, node), _) => Aux_Graph.new_node (the_key ident, node)) graph
+      |> fold (fn ((ident, _), parents) =>
+          fold (fn parent => Aux_Graph.add_edge (the_key parent, the_key ident)) parents) graph
+  in
+    Aux_Graph.topological_order G |> map (fn key =>
+      let val (_, (node, (preds, _))) = Aux_Graph.get_entry G key
+      in ((#2 key, node), map #2 (Aux_Graph.Keys.dest preds)) end)
+  end;
 
 
 (* print modes *)
 
 val browserN = "browser";
 val graphviewN = "graphview";
-val active_graphN = "active_graph";
 
 fun is_browser () =
   (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
@@ -43,41 +75,35 @@
 
 (* encode graph *)
 
-fun encode_browser (graph: graph) =
-  cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
-    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
-    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
+val encode_browser =
+  map (fn ((key, Node {name, unfold, content, directory, path}), parents) =>
+    "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
+    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
+  #> cat_lines;
 
-fun write_graph_browser path graph = File.write path (encode_browser graph);
+fun write_graph_browser path graph =
+  File.write path (encode_browser graph);
 
 
-val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
+fun encode_node (Node {name, content, ...}) =
+  (name, content) |>
+    let open XML.Encode
+    in pair string (YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks) end;
 
-fun encode_graphview (graph: graph) =
-  Graph.empty
-  |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph
-  |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
-  |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
+val encode_graph =
+  let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
 
 
 (* display graph *)
 
-fun display_graph graph =
-  if print_mode_active active_graphN then
+val display_graph =
+  sort_graph #> (fn graph =>
     let
       val (markup, body) =
         if is_browser () then (Markup.browserN, encode_browser graph)
-        else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph));
+        else (Markup.graphviewN, YXML.string_of_body (encode_graph graph));
       val ((bg1, bg2), en) =
         YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
-    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
-  else
-    let
-      val _ = writeln "Displaying graph ...";
-      val path = Isabelle_System.create_tmp_path "graph" "";
-      val _ = write_graph_browser path graph;
-      val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
-    in () end;
+    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end);
 
 end;
-
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/General/output.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -9,6 +9,7 @@
   val writeln: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
+  val legacy_feature: string -> unit
 end;
 
 signature OUTPUT =
@@ -46,6 +47,7 @@
   val information_fn: (output list -> unit) Unsynchronized.ref
   val tracing_fn: (output list -> unit) Unsynchronized.ref
   val warning_fn: (output list -> unit) Unsynchronized.ref
+  val legacy_fn: (output list -> unit) Unsynchronized.ref
   val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
   val system_message_fn: (output list -> unit) Unsynchronized.ref
   val status_fn: (output list -> unit) Unsynchronized.ref
@@ -102,6 +104,8 @@
 val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
 val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
 val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
+val legacy_fn = Unsynchronized.ref (fn ss => ! warning_fn ss);
+
 val error_message_fn =
   Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
 val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
@@ -117,6 +121,7 @@
 fun information s = ! information_fn [output s];
 fun tracing s = ! tracing_fn [output s];
 fun warning s = ! warning_fn [output s];
+fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
 fun error_message s = error_message' (serial (), s);
 fun system_message s = ! system_message_fn [output s];
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/General/scan.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -328,7 +328,7 @@
     val content = dest path' lex;
   in append (if tip then rev path' :: content else content) end) tab [];
 
-val dest_lexicon = map implode o dest [];
+val dest_lexicon = sort_strings o map implode o dest [];
 
 fun merge_lexicons (lex1, lex2) =
   if pointer_eq (lex1, lex2) then lex1
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -274,26 +274,29 @@
   let
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
-
-    val gr = rev (Theory.nodes_of thy) |> map (fn node =>
-      let
-        val name = Context.theory_name node;
-        val parents = map Context.theory_name (Theory.parents_of node);
-        val session = Present.session_name node;
-        val unfold = (session = thy_session);
-      in
-       {name = name, ID = name, parents = parents, dir = session,
-        unfold = unfold, path = "", content = []}
-      end);
-  in Graph_Display.display_graph gr end);
+  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 locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
-    val gr = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
-     {name = Locale.extern thy name, ID = name, parents = parents,
-      dir = "", unfold = true, path = "", content = [body]});
-  in Graph_Display.display_graph gr end);
+  in
+    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);
 
 
 (* print theorems, terms, types etc. *)
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -36,55 +36,6 @@
 structure Command: COMMAND =
 struct
 
-(** memo results **)
-
-datatype 'a expr =
-  Expr of Document_ID.exec * (unit -> 'a) |
-  Result of 'a Exn.result;
-
-abstype 'a memo = Memo of 'a expr Synchronized.var
-with
-
-fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
-fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
-
-fun memo_result (Memo v) =
-  (case Synchronized.value v of
-    Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
-  | Result res => Exn.release res);
-
-fun memo_finished (Memo v) =
-  (case Synchronized.value v of Expr _ => false | Result _ => true);
-
-fun memo_exec execution_id (Memo v) =
-  Synchronized.timed_access v (K (SOME Time.zeroTime))
-    (fn expr =>
-      (case expr of
-        Expr (exec_id, body) =>
-          uninterruptible (fn restore_attributes => fn () =>
-            let val group = Future.worker_subgroup () in
-              if Execution.running execution_id exec_id [group] then
-                let
-                  val res =
-                    (body
-                      |> restore_attributes
-                      |> Future.task_context "Command.memo_exec" group
-                      |> Exn.interruptible_capture) ();
-                in SOME ((), Result res) end
-              else SOME ((), expr)
-            end) ()
-      | Result _ => SOME ((), expr)))
-  |> (fn NONE => error "Conflicting command execution" | _ => ());
-
-fun memo_fork params execution_id (Memo v) =
-  (case Synchronized.peek v of
-    Result _ => ()
-  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));
-
-end;
-
-
-
 (** main phases of execution **)
 
 (* read *)
@@ -184,15 +135,19 @@
 val init_eval_state =
   {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
 
-datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
+datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
 
 fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
 val eval_eq = op = o apply2 eval_exec_id;
 
 val eval_running = Execution.is_running_exec o eval_exec_id;
-fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
+fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process;
 
-fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
+fun eval_result (Eval {exec_id, eval_process}) =
+  (case Lazy.finished_result eval_process of
+    SOME result => Exn.release result
+  | NONE => error ("Unfinished execution result: " ^ Document_ID.print exec_id));
+
 val eval_result_state = #state o eval_result;
 
 local
@@ -279,7 +234,7 @@
           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
             (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
       in eval_state keywords span tr eval_state0 end;
-  in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
+  in Eval {exec_id = exec_id, eval_process = Lazy.lazy process} end;
 
 end;
 
@@ -288,7 +243,7 @@
 
 datatype print = Print of
  {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
-  exec_id: Document_ID.exec, print_process: unit memo};
+  exec_id: Document_ID.exec, print_process: unit lazy};
 
 fun print_exec_id (Print {exec_id, ...}) = exec_id;
 val print_eq = op = o apply2 print_exec_id;
@@ -310,7 +265,7 @@
       if Exn.is_interrupt exn then reraise exn
       else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
 
-fun print_finished (Print {print_process, ...}) = memo_finished print_process;
+fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
 
 fun print_persistent (Print {persistent, ...}) = persistent;
 
@@ -337,7 +292,7 @@
       in
         Print {
           name = name, args = args, delay = delay, pri = pri, persistent = persistent,
-          exec_id = exec_id, print_process = memo exec_id process}
+          exec_id = exec_id, print_process = Lazy.lazy process}
       end;
 
     fun bad_print name args exn =
@@ -408,32 +363,45 @@
 
 type exec = eval * print list;
 val no_exec: exec =
-  (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
+  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []);
 
 fun exec_ids NONE = []
   | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
 
 local
 
-fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
-  if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
+fun run_process execution_id exec_id process =
+  let val group = Future.worker_subgroup () in
+    if Execution.running execution_id exec_id [group] then
+      ignore (Future.task_context "Command.run_process" group Lazy.force_result process)
+    else ()
+  end;
+
+fun run_eval execution_id (Eval {exec_id, eval_process}) =
+  if Lazy.is_finished eval_process then ()
+  else run_process execution_id exec_id eval_process;
+
+fun run_print execution_id (Print {name, delay, pri, exec_id, print_process, ...}) =
+  if Lazy.is_running print_process orelse Lazy.is_finished print_process then ()
+  else if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
   then
     let
       val group = Future.worker_subgroup ();
       fun fork () =
-        memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
-          execution_id print_process;
+        ignore ((singleton o Future.forks)
+          {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
+          (fn () => run_process execution_id exec_id print_process));
     in
       (case delay of
         NONE => fork ()
       | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
     end
-  else memo_exec execution_id print_process;
+  else run_process execution_id exec_id print_process;
 
 in
 
-fun exec execution_id (Eval {eval_process, ...}, prints) =
-  (memo_exec execution_id eval_process; List.app (run_print execution_id) prints);
+fun exec execution_id (eval, prints) =
+  (run_eval execution_id eval; List.app (run_print execution_id) prints);
 
 end;
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -128,7 +128,7 @@
     lazy val protocol_status: Protocol.Status =
     {
       val warnings =
-        if (results.iterator.exists(p => Protocol.is_warning(p._2)))
+        if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
           List(Markup(Markup.WARNING, Nil))
         else Nil
       val errors =
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -37,9 +37,6 @@
 
 
 
-
-
-
 (** document structure **)
 
 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
@@ -166,6 +163,16 @@
     SOME eval => not (Command.eval_finished eval)
   | NONE => false);
 
+fun finished_result node =
+  (case get_result node of
+    SOME eval => Command.eval_finished eval
+  | NONE => false);
+
+fun loaded_theory name =
+  (case try (unsuffix ".thy") name of
+    SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a]
+  | NONE => NONE);
+
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
@@ -285,16 +292,17 @@
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
   execution_id: Document_ID.execution,  (*dynamic execution id*)
-  delay_request: unit future,  (*pending event timer request*)
-  frontier: Future.task Symtab.table};  (*node name -> running execution task*)
+  delay_request: unit future};  (*pending event timer request*)
 
 val no_execution: execution =
-  {version_id = Document_ID.none, execution_id = Document_ID.none,
-   delay_request = Future.value (), frontier = Symtab.empty};
+  {version_id = Document_ID.none,
+   execution_id = Document_ID.none,
+   delay_request = Future.value ()};
 
-fun new_execution version_id delay_request frontier : execution =
-  {version_id = version_id, execution_id = Execution.start (),
-   delay_request = delay_request, frontier = frontier};
+fun new_execution version_id delay_request : execution =
+  {version_id = version_id,
+   execution_id = Execution.start (),
+   delay_request = delay_request};
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
@@ -318,11 +326,11 @@
 (* document versions *)
 
 fun define_version version_id version =
-  map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
+  map_state (fn (versions, blobs, commands, {delay_request, ...}) =>
     let
       val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
-      val execution' = new_execution version_id delay_request frontier;
+      val execution' = new_execution version_id delay_request;
     in (versions', blobs, commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =
@@ -408,40 +416,40 @@
 fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   timeit "Document.start_execution" (fn () =>
     let
-      val {version_id, execution_id, delay_request, frontier} = execution;
+      val {version_id, execution_id, delay_request} = execution;
 
       val delay = seconds (Options.default_real "editor_execution_delay");
 
       val _ = Future.cancel delay_request;
       val delay_request' = Event_Timer.future (Time.+ (Time.now (), delay));
 
-      val new_tasks =
+      fun finished_import (name, (node, _)) =
+        finished_result node orelse is_some (loaded_theory name);
+      val _ =
         nodes_of (the_version state version_id) |> String_Graph.schedule
           (fn deps => fn (name, node) =>
             if visible_node node orelse pending_result node then
               let
-                val more_deps =
-                  Future.task_of delay_request' :: the_list (Symtab.lookup frontier name);
                 fun body () =
-                  iterate_entries (fn (_, opt_exec) => fn () =>
-                    (case opt_exec of
-                      SOME exec =>
-                        if Execution.is_running execution_id
-                        then SOME (Command.exec execution_id exec)
-                        else NONE
-                    | NONE => NONE)) node ()
-                  handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn;
+                  if forall finished_import deps then
+                    iterate_entries (fn (_, opt_exec) => fn () =>
+                      (case opt_exec of
+                        SOME exec =>
+                          if Execution.is_running execution_id
+                          then SOME (Command.exec execution_id exec)
+                          else NONE
+                      | NONE => NONE)) node ()
+                  else ();
                 val future =
                   (singleton o Future.forks)
-                    {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
-                      deps = more_deps @ map #2 (maps #2 deps),
-                      pri = 0, interrupts = false} body;
-              in [(name, Future.task_of future)] end
-            else []);
-      val frontier' = (fold o fold) Symtab.update new_tasks frontier;
+                   {name = "theory:" ^ name,
+                    group = SOME (Future.new_group NONE),
+                    deps = Future.task_of delay_request' :: maps (the_list o #2 o #2) deps,
+                    pri = 0, interrupts = false} body;
+              in (node, SOME (Future.task_of future)) end
+            else (node, NONE));
       val execution' =
-        {version_id = version_id, execution_id = execution_id,
-         delay_request = delay_request', frontier = frontier'};
+        {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
     in (versions, blobs, commands, execution') end));
 
 
@@ -483,11 +491,6 @@
         Symtab.update (a, ())) all_visible all_required
   end;
 
-fun loaded_theory name =
-  (case try (unsuffix ".thy") name of
-    SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a]
-  | NONE => NONE);
-
 fun init_theory deps node span =
   let
     val master_dir = master_directory node;
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -160,10 +160,10 @@
   val informationN: string
   val tracingN: string
   val warningN: string
+  val legacyN: string
   val errorN: string
   val systemN: string
   val protocolN: string
-  val legacyN: string val legacy: T
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: T
@@ -547,12 +547,11 @@
 val informationN = "information";
 val tracingN = "tracing";
 val warningN = "warning";
+val legacyN = "legacy";
 val errorN = "error";
 val systemN = "system";
 val protocolN = "protocol";
 
-val (legacyN, legacy) = markup_elem "legacy";
-
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -353,6 +353,7 @@
   val INFORMATION = "information"
   val TRACING = "tracing"
   val WARNING = "warning"
+  val LEGACY = "legacy"
   val ERROR = "error"
   val PROTOCOL = "protocol"
   val SYSTEM = "system"
@@ -365,6 +366,7 @@
   val INFORMATION_MESSAGE = "information_message"
   val TRACING_MESSAGE = "tracing_message"
   val WARNING_MESSAGE = "warning_message"
+  val LEGACY_MESSAGE = "legacy_message"
   val ERROR_MESSAGE = "error_message"
 
   val messages = Map(
@@ -373,14 +375,13 @@
     INFORMATION -> INFORMATION_MESSAGE,
     TRACING -> TRACING_MESSAGE,
     WARNING -> WARNING_MESSAGE,
+    LEGACY -> LEGACY_MESSAGE,
     ERROR -> ERROR_MESSAGE)
 
   val message: String => String = messages.withDefault((s: String) => s)
 
   val Return_Code = new Properties.Int("return_code")
 
-  val LEGACY = "legacy"
-
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -58,7 +58,7 @@
           case Markup.JOINED => forks -= 1
           case Markup.RUNNING => touched = true; runs += 1
           case Markup.FINISHED => runs -= 1
-          case Markup.WARNING => warned = true
+          case Markup.WARNING | Markup.LEGACY => warned = true
           case Markup.FAILED | Markup.ERROR => failed = true
           case _ =>
         }
@@ -105,7 +105,7 @@
       Markup.FINISHED, Markup.FAILED)
 
   val liberal_status_elements =
-    proper_status_elements + Markup.WARNING + Markup.ERROR
+    proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
 
 
   /* command timing */
@@ -241,15 +241,6 @@
       case _ => false
     }
 
-  def is_warning_markup(msg: XML.Tree, name: String): Boolean =
-    msg match {
-      case XML.Elem(Markup(Markup.WARNING, _),
-        List(XML.Elem(markup, _))) => markup.name == name
-      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
-        List(XML.Elem(markup, _))) => markup.name == name
-      case _ => false
-    }
-
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true
@@ -257,6 +248,13 @@
       case _ => false
     }
 
+  def is_legacy(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.LEGACY, _), _) => true
+      case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
+      case _ => false
+    }
+
   def is_error(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.ERROR, _), _) => true
@@ -264,8 +262,6 @@
       case _ => false
     }
 
-  def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
-
   def is_inlined(msg: XML.Tree): Boolean =
     !(is_result(msg) || is_tracing(msg) || is_state(msg))
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/ROOT.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -27,7 +27,6 @@
 use "General/properties.ML";
 use "General/output.ML";
 use "PIDE/markup.ML";
-fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
 use "General/scan.ML";
 use "General/source.ML";
 use "General/symbol.ML";
@@ -346,6 +345,7 @@
 (* ML toplevel pretty printing *)
 
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
+toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon";
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
 toplevel_pp ["Position", "T"] "Pretty.position";
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -66,6 +66,7 @@
   val is_marked: string -> bool
   val dummy_type: term
   val fun_type: term
+  val pp_lexicon: Scan.lexicon -> Pretty.T
 end;
 
 structure Lexicon: LEXICON =
@@ -451,4 +452,10 @@
 val dummy_type = Syntax.const (mark_type "dummy");
 val fun_type = Syntax.const (mark_type "fun");
 
+
+(* toplevel pretty printing *)
+
+val pp_lexicon =
+  Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon;
+
 end;
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -123,6 +123,7 @@
     Output.tracing_fn :=
       (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
     Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
+    Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
     Output.error_message_fn :=
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
     Output.system_message_fn := message Markup.systemN [];
@@ -185,8 +186,7 @@
 
 (* init *)
 
-val default_modes1 =
-  [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
+val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
 
 val init = uninterruptible (fn _ => fn rendezvous =>
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Thy/present.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -60,8 +60,8 @@
 
 (** graphs **)
 
-fun ID_of sess s = space_implode "/" (sess @ [s]);
-fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy);
+fun ident_of sess s = space_implode "/" (sess @ [s]);
+fun ident_of_thy thy = ident_of (session_chapter_name thy) (Context.theory_name thy);
 
 fun theory_link (curr_chapter, curr_session) thy =
   let
@@ -75,27 +75,20 @@
     else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
   end;
 
-(*retrieve graph data from initial collection of theories*)
-fun init_graph (curr_chapter, curr_session) = rev o map (fn thy =>
+fun init_graph_entry session thy =
   let
-    val {chapter, name = session_name} = Browser_Info.get thy;
-    val thy_name = Context.theory_name thy;
-    val path =
-      (case theory_link (curr_chapter, curr_session) thy of
-        NONE => ""
-      | SOME p => Path.implode p);
-    val entry =
-     {name = thy_name,
-      ID = ID_of [chapter, session_name] thy_name,
-      dir = session_name,
-      path = path,
-      unfold = false,
-      parents = map ID_of_thy (Theory.parents_of thy),
-      content = []};
-  in (0, entry) end);
-
-fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * Graph_Display.node) list) =
-  (i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
+    val ident = ident_of_thy thy;
+    val parents = map ident_of_thy (Theory.parents_of thy);
+    val node =
+      Graph_Display.session_node
+       {name = Context.theory_name thy,
+        unfold = false,
+        directory = session_name thy,
+        path =
+          (case theory_link session thy of
+            NONE => ""
+          | SOME p => Path.implode p)};
+  in ((ident, node), parents) end;
 
 
 
@@ -118,7 +111,7 @@
  {theories: theory_info Symtab.table,
   tex_index: (int * string) list,
   html_index: (int * string) list,
-  graph: (int * Graph_Display.node) list};
+  graph: Graph_Display.graph};
 
 fun make_browser_info (theories, tex_index, html_index, graph) : browser_info =
   {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph};
@@ -126,7 +119,7 @@
 val empty_browser_info = make_browser_info (Symtab.empty, [], [], []);
 
 fun init_browser_info session thys =
-  make_browser_info (Symtab.empty, [], [], init_graph session thys);
+  make_browser_info (Symtab.empty, [], [], map (init_graph_entry session) thys);
 
 fun map_browser_info f {theories, tex_index, html_index, graph} =
   make_browser_info (f (theories, tex_index, html_index, graph));
@@ -159,7 +152,7 @@
 
 fun add_graph_entry entry =
   change_browser_info (fn (theories, tex_index, html_index, graph) =>
-    (theories, tex_index, html_index, ins_graph_entry entry graph));
+    (theories, tex_index, html_index, update Graph_Display.eq_entry entry graph));
 
 
 
@@ -298,7 +291,7 @@
     fun finish_html (a, {html_source, ...}: theory_info) =
       File.write (Path.append session_prefix (html_path a)) html_source;
 
-    val sorted_graph = sorted_index graph;
+    val sorted_graph = Graph_Display.sort_graph graph;
     val opt_graphs =
       if doc_graph andalso not (null documents) then
         SOME (isabelle_browser sorted_graph)
@@ -382,16 +375,16 @@
       val html_source = HTML.theory name parent_specs (mk_text ());
 
       val graph_entry =
-       {name = name,
-        ID = ID_of [chapter, session_name] name,
-        dir = session_name,
-        unfold = true,
-        path = Path.implode (html_path name),
-        parents = map ID_of_thy parents,
-        content = []};
+        ((ident_of [chapter, session_name] name,
+          Graph_Display.session_node
+           {name = name,
+            directory = session_name,
+            unfold = true,
+            path = Path.implode (html_path name)}),
+          map ident_of_thy parents);
     in
       init_theory_info name (make_theory_info ("", html_source));
-      add_graph_entry (update_time, graph_entry);
+      add_graph_entry graph_entry;
       add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
       add_tex_index (update_time, Latex.theory_entry name);
       Browser_Info.put {chapter = chapter, name = session_name} thy
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -6,11 +6,11 @@
 
 signature CLASS_DEPS =
 sig
-  val visualize: Proof.context -> sort -> sort option -> unit
-  val visualize_cmd: Proof.context -> string -> string option -> unit
+  val class_deps: Proof.context -> sort -> sort option -> unit
+  val class_deps_cmd: Proof.context -> string -> string option -> unit
 end;
 
-structure Class_deps: CLASS_DEPS =
+structure Class_Deps: CLASS_DEPS =
 struct
 
 fun gen_visualize prep_sort ctxt raw_super raw_sub =
@@ -19,26 +19,28 @@
     val sub = Option.map (prep_sort ctxt) raw_sub;
     val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
     fun le_super class = Sorts.sort_le original_algebra ([class], super);
-    val sub_le = case sub of
-      NONE => K true |
-      SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]);
-    val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt)
-      (le_super andf sub_le) (K NONE) original_algebra;
-    val classes = Sorts.classes_of algebra;
-    fun entry (c, (i, (_, cs))) =
-      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
-            dir = "", unfold = true, path = "", content = []});
-    val gr =
-      Graph.fold (cons o entry) classes []
-      |> sort (int_ord o apply2 #1) |> map #2;
-  in Graph_Display.display_graph gr end;
+    val sub_le =
+      (case sub of
+        NONE => K true
+      | SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]));
+    val (_, algebra) =
+      Sorts.subalgebra (Context.pretty ctxt)
+        (le_super andf sub_le) (K NONE) original_algebra;
+  in
+    Sorts.classes_of algebra
+    |> Graph.dest
+    |> map (fn ((c, _), ds) =>
+        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) []), ds))
+    |> Graph_Display.display_graph
+  end;
 
-val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
-val visualize_cmd = gen_visualize Syntax.read_sort;
+val class_deps = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
+val class_deps_cmd = gen_visualize Syntax.read_sort;
 
 val _ =
   Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
-    ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
-      ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
+    ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (super, sub) =>
+      (Toplevel.unknown_theory o
+       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
 
 end;
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/Tools/thm_deps.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -31,18 +31,17 @@
                       | session => [session])
                   | NONE => [])
                | _ => ["global"]);
+            val directory = space_implode "/" (session @ prefix);
             val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
-            val entry =
-              {name = Long_Name.base_name name,
-               ID = name,
-               dir = space_implode "/" (session @ prefix),
-               unfold = false,
-               path = "",
-               parents = parents,
-               content = []};
-          in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
-  in Graph_Display.display_graph (sort_wrt #ID deps) end;
+          in
+            cons ((name, Graph_Display.session_node
+              {name = Long_Name.base_name name, directory = directory,
+                unfold = false, path = ""}), parents)
+          end;
+  in
+    Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []
+    |> Graph_Display.display_graph
+  end;
 
 val _ =
   Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Pure/build-jars	Thu Jan 01 11:12:15 2015 +0100
@@ -102,16 +102,16 @@
   library.scala
   term.scala
   term_xml.scala
-  "../Tools/Graphview/src/graph_panel.scala"
-  "../Tools/Graphview/src/layout_pendulum.scala"
-  "../Tools/Graphview/src/main_panel.scala"
-  "../Tools/Graphview/src/model.scala"
-  "../Tools/Graphview/src/mutator_dialog.scala"
-  "../Tools/Graphview/src/mutator_event.scala"
-  "../Tools/Graphview/src/mutator.scala"
-  "../Tools/Graphview/src/popups.scala"
-  "../Tools/Graphview/src/shapes.scala"
-  "../Tools/Graphview/src/visualizer.scala"
+  "../Tools/Graphview/graph_panel.scala"
+  "../Tools/Graphview/layout_pendulum.scala"
+  "../Tools/Graphview/main_panel.scala"
+  "../Tools/Graphview/model.scala"
+  "../Tools/Graphview/mutator_dialog.scala"
+  "../Tools/Graphview/mutator_event.scala"
+  "../Tools/Graphview/mutator.scala"
+  "../Tools/Graphview/popups.scala"
+  "../Tools/Graphview/shapes.scala"
+  "../Tools/Graphview/visualizer.scala"
 )
 
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Jan 01 11:12:15 2015 +0100
@@ -911,25 +911,30 @@
 
 fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
 
+fun join_strong_conn gr =
+  let
+    val xss = Graph.strong_conn gr;
+    val xss_zs = map (fn xs => (xs, commas xs)) xss;
+    val z_for = the o AList.lookup (op =) (maps (fn (xs, z) => map (fn x => (x, z)) xs) xss_zs);
+    val succs = map (fn (xs, z) => (z, (map z_for o maps (Graph.immediate_succs gr)) xs)) xss_zs;
+  in
+    Graph.empty
+    |> fold (fn (xs, z) => Graph.new_node (z, map (Graph.get_node gr) xs)) xss_zs
+    |> fold (fn (z, succs) => fold (fn w => Graph.add_edge (z, w)) succs) succs
+  end;
+
 fun code_deps ctxt consts =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val eqngr = code_depgr ctxt consts;
-    val constss = Graph.strong_conn eqngr;
-    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
-      Symtab.update (const, consts)) consts) constss;
-    fun succs consts = consts
-      |> maps (Graph.immediate_succs eqngr)
-      |> subtract (op =) consts
-      |> map (the o Symtab.lookup mapping)
-      |> distinct (op =);
-    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-    fun namify consts = map (Code.string_of_const thy) consts
-      |> commas;
-    val prgr = map (fn (consts, constss) =>
-      { name = namify consts, ID = namify consts, dir = "", unfold = true,
-        path = "", parents = map namify constss, content = [] }) conn;
-  in Graph_Display.display_graph prgr end;
+    val namify = commas o map (Code.string_of_const thy);
+  in
+    code_depgr ctxt consts
+    |> Graph.map (fn c => fn _ => c)
+    |> join_strong_conn
+    |> Graph.dest
+    |> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds))
+    |> Graph_Display.display_graph
+  end;
 
 local
 
@@ -950,7 +955,7 @@
     "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.unknown_context o
-      Toplevel.keep (fn state => code_deps_cmd (Toplevel.context_of state) cs)));
+      Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
 
 end;
 
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/graph_panel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,298 @@
+/*  Title:      Tools/Graphview/graph_panel.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Graphview Java2D drawing panel.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.{Dimension, Graphics2D, Point, Rectangle}
+import java.awt.geom.{AffineTransform, Point2D}
+import java.awt.image.BufferedImage
+import javax.swing.{JScrollPane, JComponent}
+
+import scala.swing.{Panel, ScrollPane}
+import scala.swing.event._
+
+
+class Graph_Panel(
+    val visualizer: Visualizer,
+    make_tooltip: (JComponent, Int, Int, XML.Body) => String)
+  extends ScrollPane
+{
+  panel =>
+
+  tooltip = ""
+
+  override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
+    override def getToolTipText(event: java.awt.event.MouseEvent): String =
+      node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+        case Some(name) =>
+          visualizer.model.complete.get_node(name).content match {
+            case Nil => null
+            case content => make_tooltip(panel.peer, event.getX, event.getY, content)
+          }
+        case None => null
+      }
+  }
+
+  peer.setWheelScrollingEnabled(false)
+  focusable = true
+  requestFocus()
+
+  horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
+  verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
+
+  def node(at: Point2D): Option[String] =
+    visualizer.model.visible_nodes_iterator
+      .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at))
+
+  def refresh()
+  {
+    if (paint_panel != null) {
+      paint_panel.set_preferred_size()
+      paint_panel.repaint()
+    }
+  }
+
+  def fit_to_window() = {
+    Transform.fit_to_window()
+    refresh()
+  }
+
+  val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
+
+  def rescale(s: Double)
+  {
+    Transform.scale = s
+    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt)
+    refresh()
+  }
+
+  def apply_layout() = visualizer.Coordinates.update_layout()
+
+  private class Paint_Panel extends Panel {
+    def set_preferred_size() {
+        val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
+        val s = Transform.scale_discrete
+        val (px, py) = Transform.padding
+
+        preferredSize = new Dimension((math.abs(maxX - minX + px) * s).toInt,
+                                      (math.abs(maxY - minY + py) * s).toInt)
+
+        revalidate()
+      }
+
+    override def paint(g: Graphics2D) {
+      super.paintComponent(g)
+      g.transform(Transform())
+
+      visualizer.Drawer.paint_all_visible(g, true)
+    }
+  }
+  private val paint_panel = new Paint_Panel
+  contents = paint_panel
+
+  listenTo(keys)
+  listenTo(mouse.moves)
+  listenTo(mouse.clicks)
+  listenTo(mouse.wheel)
+  reactions += Interaction.Mouse.react
+  reactions += Interaction.Keyboard.react
+  reactions += {
+      case KeyTyped(_, _, _, _) => {repaint(); requestFocus()}
+      case MousePressed(_, _, _, _, _) => {repaint(); requestFocus()}
+      case MouseDragged(_, _, _) => {repaint(); requestFocus()}
+      case MouseWheelMoved(_, _, _, _) => {repaint(); requestFocus()}
+      case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()}
+      case MouseMoved(_, _, _) => repaint()
+    }
+
+  visualizer.model.Colors.events += { case _ => repaint() }
+  visualizer.model.Mutators.events += { case _ => repaint() }
+
+  apply_layout()
+  rescale(1.0)
+
+  private object Transform
+  {
+    val padding = (100, 40)
+
+    private var _scale: Double = 1.0
+    def scale: Double = _scale
+    def scale_=(s: Double)
+    {
+      _scale = (s min 10) max 0.1
+    }
+    def scale_discrete: Double =
+      (_scale * visualizer.font_size).round.toDouble / visualizer.font_size
+
+    def apply() = {
+      val (minX, minY, _, _) = visualizer.Coordinates.bounds()
+
+      val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
+      at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2)
+      at
+    }
+
+    def fit_to_window() {
+      if (visualizer.model.visible_nodes_iterator.isEmpty)
+        rescale(1.0)
+      else {
+        val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
+
+        val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
+        val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy)
+        rescale(sx min sy)
+      }
+    }
+
+    def pane_to_graph_coordinates(at: Point2D): Point2D = {
+      val s = Transform.scale_discrete
+      val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null)
+
+      p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s)
+      p
+    }
+  }
+
+  object Interaction {
+    object Keyboard {
+      import scala.swing.event.Key._
+
+      val react: PartialFunction[Event, Unit] = {
+        case KeyTyped(_, c, m, _) => typed(c, m)
+      }
+
+      def typed(c: Char, m: Modifiers) =
+        (c, m) match {
+          case ('+', _) => rescale(Transform.scale * 5.0/4)
+          case ('-', _) => rescale(Transform.scale * 4.0/5)
+          case ('0', _) => Transform.fit_to_window()
+          case ('1', _) => visualizer.Coordinates.update_layout()
+          case ('2', _) => Transform.fit_to_window()
+          case _ =>
+        }
+    }
+
+    object Mouse {
+      import scala.swing.event.Key.Modifier._
+      type Modifiers = Int
+      type Dummy = ((String, String), Int)
+
+      private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
+
+      val react: PartialFunction[Event, Unit] = {
+        case MousePressed(_, p, _, _, _) => pressed(p)
+        case MouseDragged(_, to, _) => {
+            drag(draginfo, to)
+            val (_, p, d) = draginfo
+            draginfo = (to, p, d)
+          }
+        case MouseWheelMoved(_, p, _, r) => wheel(r, p)
+        case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e)
+      }
+
+      def dummy(at: Point2D): Option[Dummy] =
+        visualizer.model.visible_edges_iterator.map({
+            i => visualizer.Coordinates(i).zipWithIndex.map((i, _))
+          }).flatten.find({
+            case (_, ((x, y), _)) =>
+              visualizer.Drawer.shape(visualizer.gfx, None).contains(at.getX() - x, at.getY() - y)
+          }) match {
+            case None => None
+            case Some((name, (_, index))) => Some((name, index))
+          }
+
+      def pressed(at: Point) {
+        val c = Transform.pane_to_graph_coordinates(at)
+        val l = node(c) match {
+          case Some(l) =>
+            if (visualizer.Selection(l)) visualizer.Selection() else List(l)
+          case None => Nil
+        }
+        val d = l match {
+          case Nil => dummy(c) match {
+              case Some(d) => List(d)
+              case None => Nil
+          }
+
+          case _ => Nil
+        }
+
+        draginfo = (at, l, d)
+      }
+
+      def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) {
+        import javax.swing.SwingUtilities
+
+        val c = Transform.pane_to_graph_coordinates(at)
+        val p = node(c)
+
+        def left_click() {
+          (p, m) match {
+            case (Some(l), Control) => visualizer.Selection.add(l)
+            case (None, Control) =>
+
+            case (Some(l), Shift) => visualizer.Selection.add(l)
+            case (None, Shift) =>
+
+            case (Some(l), _) => visualizer.Selection.set(List(l))
+            case (None, _) => visualizer.Selection.clear
+          }
+        }
+
+        def right_click() {
+          val menu = Popups(panel, p, visualizer.Selection())
+          menu.show(panel.peer, at.x, at.y)
+        }
+
+        if (clicks < 2) {
+          if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
+          else left_click()
+        }
+      }
+
+      def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) {
+        val (from, p, d) = draginfo
+
+        val s = Transform.scale_discrete
+        val (dx, dy) = (to.x - from.x, to.y - from.y)
+        (p, d) match {
+          case (Nil, Nil) => {
+            val r = panel.peer.getViewport.getViewRect
+            r.translate(-dx, -dy)
+
+            paint_panel.peer.scrollRectToVisible(r)
+          }
+
+          case (Nil, ds) =>
+            ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s)))
+
+          case (ls, _) =>
+            ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s)))
+        }
+      }
+
+      def wheel(rotation: Int, at: Point) {
+        val at2 = Transform.pane_to_graph_coordinates(at)
+        // > 0 -> up
+        rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4))
+
+        // move mouseposition to center
+        Transform().transform(at2, at2)
+        val r = panel.peer.getViewport.getViewRect
+        val (width, height) = (r.getWidth, r.getHeight)
+        paint_panel.peer.scrollRectToVisible(
+          new Rectangle((at2.getX() - width / 2).toInt,
+                        (at2.getY() - height / 2).toInt,
+                        width.toInt,
+                        height.toInt)
+        )
+      }
+    }
+  }
+}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/layout_pendulum.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/layout_pendulum.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,275 @@
+/*  Title:      Tools/Graphview/layout_pendulum.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Pendulum DAG layout algorithm.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+
+object Layout_Pendulum
+{
+  type Key = String
+  type Point = (Double, Double)
+  type Coordinates = Map[Key, Point]
+  type Level = List[Key]
+  type Levels = List[Level]
+  type Dummies = (Model.Graph, List[Key], Map[Key, Int])
+
+  case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]])
+  val empty_layout = Layout(Map.empty, Map.empty)
+
+  val pendulum_iterations = 10
+  val minimize_crossings_iterations = 40
+
+  def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout =
+  {
+    if (graph.is_empty) empty_layout
+    else {
+      val initial_levels = level_map(graph)
+
+      val (dummy_graph, dummies, dummy_levels) =
+        ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) {
+          case ((graph, dummies, levels), from) =>
+            ((graph, dummies, levels) /: graph.imm_succs(from)) {
+              case ((graph, dummies, levels), to) =>
+                if (levels(to) - levels(from) <= 1) (graph, dummies, levels)
+                else {
+                  val (next, ds, ls) = add_dummies(graph, from, to, levels)
+                  (next, dummies + ((from, to) -> ds), ls)
+                }
+            }
+        }
+
+      val levels = minimize_crossings(dummy_graph, level_list(dummy_levels))
+
+      val initial_coordinates: Coordinates =
+        (((Map.empty[Key, Point], 0.0) /: levels) {
+          case ((coords1, y), level) =>
+            ((((coords1, 0.0) /: level) {
+              case ((coords2, x), key) =>
+                val s = if (graph.defined(key)) graph.get_node(key).name else "X"
+                (coords2 + (key -> (x, y)), x + box_distance)
+            })._1, y + box_height(level.length))
+        })._1
+
+      val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates)
+
+      val dummy_coords =
+        (Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
+          case (map, key) => map + (key -> dummies(key).map(coords(_)))
+        }
+
+      Layout(coords, dummy_coords)
+    }
+  }
+
+
+  def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies =
+  {
+    val ds =
+      ((levels(from) + 1) until levels(to))
+      .map("%s$%s$%d" format (from, to, _)).toList
+
+    val ls =
+      (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) {
+        case (ls, (l, d)) => ls + (d -> l)
+      }
+
+    val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info))
+    val graph2 =
+      (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
+        case (g, List(x, y)) => g.add_edge(x, y)
+      }
+    (graph2, ds, ls)
+  }
+
+  def level_map(graph: Model.Graph): Map[Key, Int] =
+    (Map.empty[Key, Int] /: graph.topological_order) {
+      (levels, key) => {
+        val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
+        levels + (key -> lev)
+      }
+    }
+
+  def level_list(map: Map[Key, Int]): Levels =
+  {
+    val max_lev = (-1 /: map) { case (m, (_, l)) => m max l }
+    val buckets = new Array[Level](max_lev + 1)
+    for (l <- 0 to max_lev) { buckets(l) = Nil }
+    for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
+    buckets.iterator.map(_.sorted).toList
+  }
+
+  def count_crossings(graph: Model.Graph, levels: Levels): Int =
+  {
+    def in_level(ls: Levels): Int = ls match {
+      case List(top, bot) =>
+        top.iterator.zipWithIndex.map {
+          case (outer_parent, outer_parent_index) =>
+            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
+            .map(outer_child =>
+              (0 until outer_parent_index)
+              .map(inner_parent =>
+                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
+                .filter(inner_child => outer_child < inner_child)
+                .size
+              ).sum
+            ).sum
+        }.sum
+
+      case _ => 0
+    }
+
+    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
+  }
+
+  def minimize_crossings(graph: Model.Graph, levels: Levels): Levels =
+  {
+    def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
+      child.map(k => {
+          val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
+          val weight =
+            (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
+          (k, weight)
+      }).sortBy(_._2).map(_._1)
+
+    def resort(levels: Levels, top_down: Boolean) = top_down match {
+      case true =>
+        (List[Level](levels.head) /: levels.tail) {
+          (tops, bot) => resort_level(tops.head, bot, top_down) :: tops
+        }.reverse
+
+      case false =>
+        (List[Level](levels.reverse.head) /: levels.reverse.tail) {
+          (bots, top) => resort_level(bots.head, top, top_down) :: bots
+        }
+      }
+
+    ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) {
+      case ((old_levels, old_crossings, top_down), _) => {
+          val new_levels = resort(old_levels, top_down)
+          val new_crossings = count_crossings(graph, new_levels)
+          if (new_crossings < old_crossings)
+            (new_levels, new_crossings, !top_down)
+          else
+            (old_levels, old_crossings, !top_down)
+      }
+    }._1
+  }
+
+  def pendulum(graph: Model.Graph, box_distance: Double,
+    levels: Levels, coords: Map[Key, Point]): Coordinates =
+  {
+    type Regions = List[List[Region]]
+
+    def iteration(regions: Regions, coords: Coordinates, top_down: Boolean)
+      : (Regions, Coordinates, Boolean) =
+    {
+      val (nextr, nextc, moved) =
+      ((List.empty[List[Region]], coords, false) /:
+       (if (top_down) regions else regions.reverse)) {
+        case ((tops, coords, prev_moved), bot) => {
+            val nextb = collapse(coords, bot, top_down)
+            val (nextc, this_moved) = deflect(coords, nextb, top_down)
+            (nextb :: tops, nextc, prev_moved || this_moved)
+        }
+      }
+
+      (nextr.reverse, nextc, moved)
+    }
+
+    def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] =
+    {
+      if (level.size <= 1) level
+      else {
+        var next = level
+        var regions_changed = true
+        while (regions_changed) {
+          regions_changed = false
+          for (i <- (next.length to 1)) {
+            val (r1, r2) = (next(i-1), next(i))
+            val d1 = r1.deflection(coords, top_down)
+            val d2 = r2.deflection(coords, top_down)
+
+            if (// Do regions touch?
+                r1.distance(coords, r2) <= box_distance &&
+                // Do they influence each other?
+                (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0))
+            {
+              regions_changed = true
+              r1.nodes = r1.nodes ::: r2.nodes
+              next = next.filter(next.indexOf(_) != i)
+            }
+          }
+        }
+        next
+      }
+    }
+
+    def deflect(coords: Coordinates, level: List[Region], top_down: Boolean)
+        : (Coordinates, Boolean) =
+    {
+      ((coords, false) /: (0 until level.length)) {
+        case ((coords, moved), i) => {
+            val r = level(i)
+            val d = r.deflection(coords, top_down)
+            val offset = {
+              if (i == 0 && d <= 0) d
+              else if (i == level.length - 1 && d >= 0) d
+              else if (d < 0) {
+                val prev = level(i-1)
+                (-(r.distance(coords, prev) - box_distance)) max d
+              }
+              else {
+                val next = level(i+1)
+                (r.distance(coords, next) - box_distance) min d
+              }
+            }
+
+            (r.move(coords, offset), moved || (d != 0))
+        }
+      }
+    }
+
+    val regions = levels.map(level => level.map(new Region(graph, _)))
+
+    ((regions, coords, true, true) /: (1 to pendulum_iterations)) {
+      case ((regions, coords, top_down, moved), _) =>
+        if (moved) {
+          val (nextr, nextc, m) = iteration(regions, coords, top_down)
+          (nextr, nextc, !top_down, m)
+        }
+        else (regions, coords, !top_down, moved)
+    }._2
+  }
+
+  private class Region(val graph: Model.Graph, node: Key)
+  {
+    var nodes: List[Key] = List(node)
+
+    def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min
+    def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max
+
+    def distance(coords: Coordinates, to: Region): Double =
+      math.abs(left(coords) - to.left(coords)) min
+      math.abs(right(coords) - to.right(coords))
+
+    def deflection(coords: Coordinates, use_preds: Boolean) =
+      nodes.map(k => (coords(k)._1,
+                      if (use_preds) graph.imm_preds(k).toList  // FIXME iterator
+                      else graph.imm_succs(k).toList))
+      .map({ case (x, as) => as.map(coords(_)._1 - x).sum / (as.length max 1) })
+      .sum / nodes.length
+
+    def move(coords: Coordinates, by: Double): Coordinates =
+      (coords /: nodes) {
+        case (cs, node) =>
+          val (x, y) = cs(node)
+          cs + (node -> (x + by, y))
+      }
+  }
+}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/main_panel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/main_panel.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,125 @@
+/*  Title:      Tools/Graphview/main_panel.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Graph Panel wrapper.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+
+import scala.collection.JavaConversions._
+import scala.swing.{BorderPanel, Button, BoxPanel,
+  Orientation, Swing, CheckBox, Action, FileChooser}
+
+import java.io.{File => JFile}
+import java.awt.{Color, Dimension, Graphics2D}
+import java.awt.geom.Rectangle2D
+import java.awt.image.BufferedImage
+import javax.imageio.ImageIO
+import javax.swing.border.EmptyBorder
+import javax.swing.JComponent
+
+
+class Main_Panel(graph: Model.Graph) extends BorderPanel
+{
+  focusable = true
+  requestFocus()
+
+  val model = new Model(graph)
+  val visualizer = new Visualizer(model)
+
+  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
+  val graph_panel = new Graph_Panel(visualizer, make_tooltip)
+
+  listenTo(keys)
+  reactions += graph_panel.reactions
+
+  val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)
+
+  val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations")
+
+  private val chooser = new FileChooser()
+  chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
+  chooser.title = "Save Image (.png or .pdf)"
+
+  val options_panel = new BoxPanel(Orientation.Horizontal) {
+    border = new EmptyBorder(0, 0, 10, 0)
+
+    contents += Swing.HGlue
+    contents += new CheckBox(){
+      selected = visualizer.arrow_heads
+      action = Action("Arrow Heads"){
+        visualizer.arrow_heads = selected
+        graph_panel.repaint()
+      }
+    }
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += new Button{
+      action = Action("Save Image"){
+        chooser.showSaveDialog(this) match {
+          case FileChooser.Result.Approve => export(chooser.selectedFile)
+          case _ =>
+        }
+      }
+    }
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += graph_panel.zoom
+
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += new Button{
+      action = Action("Apply Layout"){
+        graph_panel.apply_layout()
+      }
+    }
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += new Button{
+      action = Action("Fit to Window"){
+        graph_panel.fit_to_window()
+      }
+    }
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += new Button{
+      action = Action("Colorations"){
+        color_dialog.open
+      }
+    }
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += new Button{
+      action = Action("Filters"){
+        mutator_dialog.open
+      }
+    }
+  }
+
+  add(graph_panel, BorderPanel.Position.Center)
+  add(options_panel, BorderPanel.Position.North)
+
+  private def export(file: JFile)
+  {
+    val (x0, y0, x1, y1) = visualizer.Coordinates.bounds
+    val w = (math.abs(x1 - x0) + 400).toInt
+    val h = (math.abs(y1 - y0) + 200).toInt
+
+    def paint(gfx: Graphics2D)
+    {
+      gfx.setColor(Color.WHITE)
+      gfx.fill(new Rectangle2D.Double(0, 0, w, h))
+
+      gfx.translate(- x0 + 200, - y0 + 100)
+      visualizer.Drawer.paint_all_visible(gfx, false)
+    }
+
+    try {
+      val name = file.getName
+      if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
+      else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
+      else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
+    }
+    catch {
+      case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
+    }
+  }
+}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/model.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/model.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,106 @@
+/*  Title:      Tools/Graphview/model.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Internal graph representation.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+
+import java.awt.Color
+
+
+class Mutator_Container(val available: List[Mutator]) {
+    type Mutator_Markup = (Boolean, Color, Mutator)
+    
+    val events = new Mutator_Event.Bus
+    
+    private var _mutators : List[Mutator_Markup] = Nil
+    def apply() = _mutators
+    def apply(mutators: List[Mutator_Markup]){
+      _mutators = mutators
+      
+      events.event(Mutator_Event.NewList(mutators))
+    }    
+
+    def add(mutator: Mutator_Markup) = {
+      _mutators = _mutators ::: List(mutator)
+      
+      events.event(Mutator_Event.Add(mutator))
+    }
+}
+
+
+object Model
+{
+  /* node info */
+
+  sealed case class Info(name: String, content: XML.Body)
+
+  val empty_info: Info = Info("", Nil)
+
+  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+
+    val (name, content) = pair(string, x => x)(body)
+    Info(name, content)
+  }
+
+
+  /* graph */
+
+  type Graph = isabelle.Graph[String, Info]
+
+  val decode_graph: XML.Decode.T[Graph] =
+    isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true)
+}
+
+class Model(private val graph: Model.Graph) {  
+  val Mutators = new Mutator_Container(
+    List(
+      Node_Expression(".*", false, false, false),
+      Node_List(Nil, false, false, false),
+      Edge_Endpoints("", ""),
+      Add_Node_Expression(""),
+      Add_Transitive_Closure(true, true)
+    ))
+  
+  val Colors = new Mutator_Container(
+    List(
+      Node_Expression(".*", false, false, false),
+      Node_List(Nil, false, false, false)
+    ))  
+  
+  def visible_nodes_iterator: Iterator[String] = current.keys_iterator
+  
+  def visible_edges_iterator: Iterator[(String, String)] =
+    current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _)))
+  
+  def complete = graph
+  def current: Model.Graph =
+      (graph /: Mutators()) {
+        case (g, (enabled, _, mutator)) => {
+          if (!enabled) g
+          else mutator.mutate(graph, g)
+        }
+      }
+    
+  private var _colors = Map.empty[String, Color]
+  def colors = _colors
+  
+  private def build_colors() {
+    _colors = 
+      (Map.empty[String, Color] /: Colors()) ({
+          case (colors, (enabled, color, mutator)) => {
+              (colors /: mutator.mutate(graph, graph).keys_iterator) ({
+                  case (colors, k) => colors + (k -> color)
+                })
+            }
+      })
+  }
+  Colors.events += { case _ => build_colors() }
+}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/mutator.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/mutator.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,199 @@
+/*  Title:      Tools/Graphview/mutator.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Filters and add-operations on graphs.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.Color
+import scala.collection.immutable.SortedSet
+
+
+trait Mutator
+{
+  val name: String
+  val description: String
+  def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph
+
+  override def toString: String = name
+}
+
+trait Filter extends Mutator
+{
+  def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub)
+  def filter(sub: Model.Graph) : Model.Graph
+}
+
+object Mutators {
+  type Mutator_Markup = (Boolean, Color, Mutator)
+  
+  val Enabled = true
+  val Disabled = false
+  
+  def create(visualizer: Visualizer, m: Mutator): Mutator_Markup =
+    (Mutators.Enabled, visualizer.Colors.next, m)
+
+  class Graph_Filter(val name: String, val description: String,
+    pred: Model.Graph => Model.Graph)
+  extends Filter
+  {
+    def filter(sub: Model.Graph) : Model.Graph = pred(sub)
+  }
+
+  class Graph_Mutator(val name: String, val description: String,
+    pred: (Model.Graph, Model.Graph) => Model.Graph)
+  extends Mutator
+  {
+    def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph =
+          pred(complete, sub)
+  }
+
+  class Node_Filter(name: String, description: String,
+    pred: (Model.Graph, String) => Boolean)
+    extends Graph_Filter (
+
+    name,
+    description,
+    g => g.restrict(pred(g, _))
+  )
+
+  class Edge_Filter(name: String, description: String,
+    pred: (Model.Graph, String, String) => Boolean)
+    extends Graph_Filter (
+
+    name,
+    description,
+    g => (g /: g.dest) {
+      case (graph, ((from, _), tos)) => {
+        (graph /: tos) {
+          (gr, to) => if (pred(gr, from, to)) gr
+                      else gr.del_edge(from, to)
+        }
+      }
+    }
+  )
+
+  class Node_Family_Filter(name: String, description: String,
+      reverse: Boolean, parents: Boolean, children: Boolean,
+      pred: (Model.Graph, String) => Boolean)
+    extends Node_Filter(
+
+    name,
+    description,
+    (g, k) => reverse != (
+      pred(g, k) ||
+      (parents && g.all_preds(List(k)).exists(pred(g, _))) ||
+      (children && g.all_succs(List(k)).exists(pred(g, _)))
+    )
+  )  
+  
+  case class Identity()
+    extends Graph_Filter(
+
+    "Identity",
+    "Does not change the graph.",
+    g => g
+  )
+
+  case class Node_Expression(regex: String,
+    reverse: Boolean, parents: Boolean, children: Boolean)
+    extends Node_Family_Filter(
+
+    "Filter by Name",
+    "Only shows or hides all nodes with any family member's name matching " +
+    "a regex.",
+    reverse,
+    parents,
+    children,
+    (g, k) => (regex.r findFirstIn k).isDefined
+  )
+
+  case class Node_List(list: List[String],
+    reverse: Boolean, parents: Boolean, children: Boolean)
+    extends Node_Family_Filter(
+
+    "Filter by Name List",
+    "Only shows or hides all nodes with any family member's name matching " +
+    "any string in a comma separated list.",
+    reverse,
+    parents,
+    children,
+    (g, k) => list.exists(_ == k)
+  )
+
+  case class Edge_Endpoints(source: String, dest: String)
+    extends Edge_Filter(
+
+    "Hide edge",
+    "Hides the edge whose endpoints match strings.",
+    (g, s, d) => !(s == source && d == dest)
+  )
+
+  private def add_node_group(from: Model.Graph, to: Model.Graph,
+    keys: List[String]) = {
+    
+    // Add Nodes
+    val with_nodes = 
+      (to /: keys) {
+        (graph, key) => graph.default_node(key, from.get_node(key))
+      }
+    
+    // Add Edges
+    (with_nodes /: keys) {
+      (gv, key) => {
+        def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
+          (g /: keys) {
+            (graph, end) => {
+              if (!graph.keys_iterator.contains(end)) graph
+              else {
+                if (succs) graph.add_edge(key, end)
+                else graph.add_edge(end, key)
+              }
+            }
+          }
+
+        
+        add_edges(
+          add_edges(gv, from.imm_preds(key), false),
+          from.imm_succs(key), true
+        )
+      }
+    }
+  }  
+  
+  case class Add_Node_Expression(regex: String)
+    extends Graph_Mutator(
+
+    "Add by name",
+    "Adds every node whose name matches the regex. " +
+    "Adds all relevant edges.",
+    (complete, sub) => {
+      add_node_group(complete, sub, complete.keys.filter(
+          k => (regex.r findFirstIn k).isDefined
+        ).toList)
+    }
+  )
+  
+  case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
+    extends Graph_Mutator(
+
+    "Add transitive closure",
+    "Adds all family members of all current nodes.",
+    (complete, sub) => {     
+      val withparents = 
+        if (parents)
+          add_node_group(complete, sub, complete.all_preds(sub.keys))
+        else
+          sub
+      
+      if (children)
+        add_node_group(complete, withparents, complete.all_succs(sub.keys))
+      else 
+        withparents
+    }
+  )
+}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/mutator_dialog.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/mutator_dialog.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,427 @@
+/*  Title:      Tools/Graphview/mutator_dialog.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Mutator selection and configuration dialog.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.Color
+import java.awt.FocusTraversalPolicy
+import javax.swing.JColorChooser
+import javax.swing.border.EmptyBorder
+import scala.collection.JavaConversions._
+import scala.swing._
+import isabelle.graphview.Mutators._
+import scala.swing.event.ValueChanged
+
+
+class Mutator_Dialog(
+    visualizer: Visualizer,
+    container: Mutator_Container,
+    caption: String,
+    reverse_caption: String = "Inverse",
+    show_color_chooser: Boolean = true)
+  extends Dialog
+{
+  type Mutator_Markup = (Boolean, Color, Mutator)
+  
+  title = caption
+  
+  private var _panels: List[Mutator_Panel] = Nil
+  private def panels = _panels
+  private def panels_= (panels: List[Mutator_Panel]) {
+    _panels = panels
+    paintPanels
+  }
+
+  container.events += {
+    case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
+    case Mutator_Event.NewList(ms) => panels = getPanels(ms)
+  }
+
+  override def open() {
+    if (!visible)
+      panels = getPanels(container())
+
+    super.open
+  }
+
+  minimumSize = new Dimension(700, 200)
+  preferredSize = new Dimension(1000, 300)
+  peer.setFocusTraversalPolicy(focusTraversal)
+
+  private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] =
+    m.filter(_ match {case (_, _, Identity()) => false; case _ => true})
+    .map(m => new Mutator_Panel(m))
+
+  private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = 
+    panels.map(panel => panel.get_Mutator_Markup)
+
+  private def movePanelUp(m: Mutator_Panel) = {
+    def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
+      case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs)
+      case _ => l
+    }
+
+    panels = moveUp(panels)
+  }
+
+  private def movePanelDown(m: Mutator_Panel) = {
+    def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
+      case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs)
+      case _ => l
+    }
+
+    panels = moveDown(panels)
+  }
+
+  private def removePanel(m: Mutator_Panel) = {
+    panels = panels.filter(_ != m).toList
+  }
+
+  private def addPanel(m: Mutator_Panel) = {
+    panels = panels ::: List(m)
+  }
+
+  def paintPanels = {
+    focusTraversal.clear
+    filterPanel.contents.clear
+    panels.map(x => {
+        filterPanel.contents += x
+        focusTraversal.addAll(x.focusList)
+      })
+    filterPanel.contents += Swing.VGlue
+
+    focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component])
+    focusTraversal.add(addButton.peer)
+    focusTraversal.add(applyButton.peer)
+    focusTraversal.add(cancelButton.peer)
+    filterPanel.revalidate
+    filterPanel.repaint
+  }
+
+  val filterPanel = new BoxPanel(Orientation.Vertical) {}
+
+  private val mutatorBox = new ComboBox[Mutator](container.available)
+
+  private val addButton: Button = new Button{
+    action = Action("Add") {
+      addPanel(
+        new Mutator_Panel((true, visualizer.Colors.next,
+                           mutatorBox.selection.item))
+      )
+    }
+  }
+
+  private val applyButton = new Button{
+    action = Action("Apply") {
+      container(getMutators(panels))
+    }
+  }
+
+  private val resetButton = new Button {
+    action = Action("Reset") {
+      panels = getPanels(container())
+    }
+  }
+
+  private val cancelButton = new Button{
+      action = Action("Close") {
+        close
+      }
+    }
+  defaultButton = cancelButton
+
+  private val botPanel = new BoxPanel(Orientation.Horizontal) {
+    border = new EmptyBorder(10, 0, 0, 0)
+
+    contents += mutatorBox
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += addButton
+
+    contents += Swing.HGlue
+    contents += Swing.RigidBox(new Dimension(30, 0))
+    contents += applyButton
+
+    contents += Swing.RigidBox(new Dimension(5, 0))
+    contents += resetButton
+
+    contents += Swing.RigidBox(new Dimension(5, 0))
+    contents += cancelButton
+  }
+  
+  contents = new BorderPanel {
+    border = new EmptyBorder(5, 5, 5, 5)
+
+    add(new ScrollPane(filterPanel), BorderPanel.Position.Center)
+    add(botPanel, BorderPanel.Position.South)
+  }
+
+  private class Mutator_Panel(initials: Mutator_Markup)
+    extends BoxPanel(Orientation.Horizontal)
+  {
+    private val (_enabled, _color, _mutator) = initials
+    
+    private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs()
+    var focusList = List.empty[java.awt.Component]
+    private val enabledBox = new iCheckBox("Enabled", _enabled)
+
+    border = new EmptyBorder(5, 5, 5, 5)
+    maximumSize = new Dimension(Integer.MAX_VALUE, 30)
+    background = _color
+
+    contents += new Label(_mutator.name) {
+      preferredSize = new Dimension(175, 20)
+      horizontalAlignment = Alignment.Left
+      if (_mutator.description != "") tooltip = _mutator.description
+    }
+    contents += Swing.RigidBox(new Dimension(10, 0))
+    contents += enabledBox
+    contents += Swing.RigidBox(new Dimension(5, 0))
+    focusList = enabledBox.peer :: focusList
+    inputs.map( _ match {
+      case (n, c) => {
+          contents += Swing.RigidBox(new Dimension(10, 0))
+        if (n != "") {
+          contents += new Label(n)
+          contents += Swing.RigidBox(new Dimension(5, 0))
+        }
+        contents += c.asInstanceOf[Component]
+        
+        focusList = c.asInstanceOf[Component].peer :: focusList
+      }
+      case _ =>
+    })
+
+    {
+      val t = this
+      contents += Swing.HGlue
+      contents += Swing.RigidBox(new Dimension(10, 0))
+
+      if (show_color_chooser) {
+        contents += new Button {
+          maximumSize = new Dimension(20, 20)
+
+          action = Action("Color") {
+            t.background =
+              JColorChooser.showDialog(t.peer, "Choose new Color", t.background)
+          }
+
+          focusList = this.peer :: focusList
+        }
+        contents += Swing.RigidBox(new Dimension(2, 0))
+      }
+
+      contents += new Button {
+        maximumSize = new Dimension(20, 20)
+
+        action = Action("Up") {
+          movePanelUp(t)
+        }
+
+        focusList = this.peer :: focusList
+      }
+      contents += Swing.RigidBox(new Dimension(2, 0))
+      contents += new Button {
+        maximumSize = new Dimension(20, 20)
+
+        action = Action("Down") {
+          movePanelDown(t)
+        }
+
+        focusList = this.peer :: focusList
+      }
+      contents += Swing.RigidBox(new Dimension(2, 0))
+      contents += new Button {
+        maximumSize = new Dimension(20, 20)
+
+        action = Action("Del") {
+          removePanel(t)
+        }
+
+        focusList = this.peer :: focusList
+      }
+    }
+
+    focusList = focusList.reverse
+
+    private def isRegex(regex: String): Boolean = {
+      try {
+        regex.r
+
+        true
+      } catch {
+        case _: java.util.regex.PatternSyntaxException =>  false
+      }
+    }
+   
+    def get_Mutator_Markup: Mutator_Markup = {
+      def regexOrElse(regex: String, orElse: String): String = {
+        if (isRegex(regex)) regex
+        else orElse
+      }
+      
+      val m = _mutator match {
+        case Identity() =>
+          Identity()
+        case Node_Expression(r, _, _, _) =>
+          Node_Expression(
+            regexOrElse(inputs(2)._2.getString, r),
+            inputs(3)._2.getBool,
+            // "Parents" means "Show parents" or "Matching Children"
+            inputs(1)._2.getBool,
+            inputs(0)._2.getBool
+          )
+        case Node_List(_, _, _, _) =>
+          Node_List(
+            inputs(2)._2.getString.split(',').filter(_ != "").toList,
+            inputs(3)._2.getBool,
+            // "Parents" means "Show parents" or "Matching Children"
+            inputs(1)._2.getBool,
+            inputs(0)._2.getBool
+          )
+        case Edge_Endpoints(_, _) =>
+          Edge_Endpoints(
+            inputs(0)._2.getString,
+            inputs(1)._2.getString
+          )
+        case Add_Node_Expression(r) =>
+          Add_Node_Expression(
+            regexOrElse(inputs(0)._2.getString, r)
+          )
+        case Add_Transitive_Closure(_, _) =>
+          Add_Transitive_Closure(
+            inputs(0)._2.getBool,
+            inputs(1)._2.getBool
+          )
+        case _ =>
+          Identity()
+      }
+      
+      (enabledBox.selected, background, m)
+    }
+    
+    private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match {
+      case Node_Expression(regex, reverse, check_parents, check_children) =>
+        List(
+          ("", new iCheckBox("Parents", check_children)),
+          ("", new iCheckBox("Children", check_parents)),
+          ("Regex", new iTextField(regex, x => !isRegex(x))),
+          ("", new iCheckBox(reverse_caption, reverse))
+        )
+      case Node_List(list, reverse, check_parents, check_children) =>
+        List(
+          ("", new iCheckBox("Parents", check_children)),
+          ("", new iCheckBox("Children", check_parents)),
+          ("Names", new iTextField(list.mkString(","))),
+          ("", new iCheckBox(reverse_caption, reverse))
+        )
+      case Edge_Endpoints(source, dest) =>
+        List(
+          ("Source", new iTextField(source)),
+          ("Destination", new iTextField(dest))
+        )
+      case Add_Node_Expression(regex) =>
+        List(
+          ("Regex", new iTextField(regex, x => !isRegex(x)))
+        )
+      case Add_Transitive_Closure(parents, children) =>
+        List(
+          ("", new iCheckBox("Parents", parents)),
+          ("", new iCheckBox("Children", children))
+        )
+      case _ => Nil
+    }
+  }
+
+  private trait Mutator_Input_Value
+  {
+    def getString: String
+    def getBool: Boolean
+  }
+
+  private class iTextField(t: String, colorator: String => Boolean)
+  extends TextField(t) with Mutator_Input_Value
+  {
+    def this(t: String) = this(t, x => false)
+
+    preferredSize = new Dimension(125, 18)
+
+    reactions += {
+      case ValueChanged(_) =>
+          if (colorator(text))
+            background = Color.RED
+          else
+            background = Color.WHITE
+    }
+
+    def getString = text
+    def getBool = true
+  }
+
+  private class iCheckBox(t: String, s: Boolean)
+  extends CheckBox(t) with Mutator_Input_Value
+  {
+    selected = s
+
+    def getString = ""
+    def getBool = selected
+  }
+
+  private object focusTraversal
+    extends FocusTraversalPolicy
+  {
+    private var items = Vector[java.awt.Component]()
+
+    def add(c: java.awt.Component) {
+      items = items :+ c
+    }
+    def addAll(cs: TraversableOnce[java.awt.Component]) {
+      items = items ++ cs
+    }
+    def clear() {
+      items = Vector[java.awt.Component]()
+    }
+
+    def getComponentAfter(root: java.awt.Container,
+                          c: java.awt.Component): java.awt.Component = {
+      val i = items.indexOf(c)
+      if (i < 0) {
+        getDefaultComponent(root)
+      } else {
+        items((i + 1) % items.length)
+      }
+    }
+
+    def getComponentBefore(root: java.awt.Container,
+                           c: java.awt.Component): java.awt.Component = {
+      val i = items.indexOf(c)
+      if (i < 0) {
+        getDefaultComponent(root)
+      } else {
+        items((i - 1) % items.length)
+      }
+    }
+
+    def getFirstComponent(root: java.awt.Container): java.awt.Component = {
+      if (items.length > 0)
+        items(0)
+      else
+        null
+    }
+
+    def getDefaultComponent(root: java.awt.Container)
+      : java.awt.Component = getFirstComponent(root)
+
+    def getLastComponent(root: java.awt.Container): java.awt.Component = {
+      if (items.length > 0)
+        items.last
+      else
+        null
+    }
+  }
+}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/mutator_event.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/mutator_event.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,35 @@
+/*  Title:      Tools/Graphview/mutator_event.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Events for dialog synchronization.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import scala.collection.mutable
+
+import java.awt.Color
+
+
+object Mutator_Event
+{
+  type Mutator_Markup = (Boolean, Color, Mutator)
+
+  sealed abstract class Message
+  case class Add(m: Mutator_Markup) extends Message
+  case class NewList(m: List[Mutator_Markup]) extends Message
+
+  type Receiver = PartialFunction[Message, Unit]
+
+  class Bus
+  {
+    private val receivers = new mutable.ListBuffer[Receiver]
+
+    def += (r: Receiver) { GUI_Thread.require {}; receivers += r }
+    def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r }
+    def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) }
+  }
+}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/popups.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/popups.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,176 @@
+/*  Title:      Tools/Graphview/popups.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+PopupMenu generation for graph components.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+
+import javax.swing.JPopupMenu
+import scala.swing.{Action, Menu, MenuItem, Separator}
+
+
+object Popups
+{
+  def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String])
+    : JPopupMenu =
+  {
+    val visualizer = panel.visualizer
+
+    val add_mutator = visualizer.model.Mutators.add _
+    val curr = visualizer.model.current
+
+    def filter_context(ls: List[String], reverse: Boolean,
+                       caption: String, edges: Boolean) =
+      new Menu(caption) {
+        contents += new MenuItem(new Action("This") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, false, false)
+                )
+              )
+          })
+
+        contents += new MenuItem(new Action("Family") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, true, true)
+                )
+              )
+          })
+
+        contents += new MenuItem(new Action("Parents") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, false, true)
+                )
+              )
+          })
+
+        contents += new MenuItem(new Action("Children") {
+            def apply =
+              add_mutator(
+                Mutators.create(visualizer,
+                  Node_List(ls, reverse, true, false)
+                )
+              )
+          })
+
+
+        if (edges) {
+          val outs = ls.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
+                      .filter(_._2.size > 0).sortBy(_._1)
+          val ins = ls.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
+                      .filter(_._2.size > 0).sortBy(_._1)
+
+          if (outs.nonEmpty || ins.nonEmpty) {
+            contents += new Separator()
+
+            contents += new Menu("Edge") {
+              if (outs.nonEmpty) {
+                contents += new MenuItem("From...") {
+                  enabled = false
+                }
+
+                outs.map( e => {
+                  val (from, tos) = e
+                  contents += new Menu(from) {
+                    contents += new MenuItem("To..."){
+                      enabled = false
+                    }
+
+                    tos.toList.sorted.distinct.map( to => {
+                      contents += new MenuItem(new Action(to) {
+                        def apply =
+                          add_mutator(
+                            Mutators.create(visualizer, Edge_Endpoints(from, to))
+                          )
+                      })
+                    })
+                  }
+                })
+              }
+              if (outs.nonEmpty && ins.nonEmpty) {
+                contents += new Separator()
+              }
+              if (ins.nonEmpty) {
+                contents += new MenuItem("To...") {
+                  enabled = false
+                }
+
+                ins.map( e => {
+                  val (to, froms) = e
+                  contents += new Menu(to) {
+                    contents += new MenuItem("From..."){
+                      enabled = false
+                    }
+
+                    froms.toList.sorted.distinct.map( from => {
+                      contents += new MenuItem(new Action(from) {
+                        def apply =
+                          add_mutator(
+                            Mutators.create(visualizer, Edge_Endpoints(from, to))
+                          )
+                      })
+                    })
+                  }
+                })
+              }
+            }
+          }
+        }
+    }
+
+    val popup = new JPopupMenu()
+
+    popup.add(new MenuItem(new Action("Remove all filters") {
+          def apply = visualizer.model.Mutators(Nil)
+        }).peer
+    )
+    popup.add(new JPopupMenu.Separator)
+
+    if (under_mouse.isDefined) {
+      val v = under_mouse.get
+      popup.add(new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) {
+        enabled = false
+      }.peer)
+
+      popup.add(filter_context(List(v), true, "Hide", true).peer)
+      popup.add(filter_context(List(v), false, "Show only", false).peer)
+
+      popup.add(new JPopupMenu.Separator)
+    }
+    if (!selected.isEmpty) {
+      val text = {
+        if (selected.length > 1) {
+          "Multiple"
+        } else {
+          visualizer.Caption(selected.head)
+        }
+      }
+
+      popup.add(new MenuItem("Selected: %s".format(text)) {
+        enabled = false
+      }.peer)
+
+      popup.add(filter_context(selected, true, "Hide", true).peer)
+      popup.add(filter_context(selected, false, "Show only", false).peer)
+      popup.add(new JPopupMenu.Separator)
+    }
+
+
+    popup.add(new MenuItem(new Action("Fit to Window") {
+        def apply = panel.fit_to_window()
+      }).peer
+    )
+
+    popup
+  }
+}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/shapes.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/shapes.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,255 @@
+/*  Title:      Tools/Graphview/shapes.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Drawable shapes.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.{BasicStroke, Graphics2D, Shape}
+import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator}
+
+
+object Shapes
+{
+  trait Node
+  {
+    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape
+    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit
+  }
+
+  object Growing_Node extends Node
+  {
+    private val stroke =
+      new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+
+    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double =
+    {
+      val (x, y) = visualizer.Coordinates(peer.get)
+      val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g)
+      val w = bounds.getWidth + visualizer.pad_x
+      val h = bounds.getHeight + visualizer.pad_y
+      new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
+    }
+
+    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
+    {
+      val caption = visualizer.Caption(peer.get)
+      val bounds = g.getFontMetrics.getStringBounds(caption, g)
+      val s = shape(g, visualizer, peer)
+
+      val (border, background, foreground) = visualizer.Color(peer)
+      g.setStroke(stroke)
+      g.setColor(border)
+      g.draw(s)
+      g.setColor(background)
+      g.fill(s)
+      g.setColor(foreground)
+      g.drawString(caption,
+        (s.getCenterX + (- bounds.getWidth / 2)).toFloat,
+        (s.getCenterY + 5).toFloat)
+    }
+  }
+
+  object Dummy extends Node
+  {
+    private val stroke =
+      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+    private val shape = new Rectangle2D.Double(-5, -5, 10, 10)
+    private val identity = new AffineTransform()
+
+    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape
+
+    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
+      paint_transformed(g, visualizer, peer, identity)
+
+    def paint_transformed(g: Graphics2D, visualizer: Visualizer,
+      peer: Option[String], at: AffineTransform)
+    {
+      val (border, background, foreground) = visualizer.Color(peer)
+      g.setStroke(stroke)
+      g.setColor(border)
+      g.draw(at.createTransformedShape(shape))
+    }
+  }
+
+  trait Edge
+  {
+    def paint(g: Graphics2D, visualizer: Visualizer,
+      peer: (String, String), head: Boolean, dummies: Boolean)
+  }
+
+  object Straight_Edge extends Edge
+  {
+    private val stroke =
+      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+
+    def paint(g: Graphics2D, visualizer: Visualizer,
+      peer: (String, String), head: Boolean, dummies: Boolean)
+    {
+      val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
+      val ds =
+      {
+        val min = fy min ty
+        val max = fy max ty
+        visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max })
+      }
+      val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
+
+      path.moveTo(fx, fy)
+      ds.foreach({case (x, y) => path.lineTo(x, y)})
+      path.lineTo(tx, ty)
+
+      if (dummies) {
+        ds.foreach({
+            case (x, y) => {
+              val at = AffineTransform.getTranslateInstance(x, y)
+              Dummy.paint_transformed(g, visualizer, None, at)
+            }
+          })
+      }
+
+      g.setStroke(stroke)
+      g.setColor(visualizer.Color(peer))
+      g.draw(path)
+
+      if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
+    }
+  }
+
+  object Cardinal_Spline_Edge extends Edge
+  {
+    private val stroke =
+      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+    private val slack = 0.1
+
+    def paint(g: Graphics2D, visualizer: Visualizer,
+      peer: (String, String), head: Boolean, dummies: Boolean)
+    {
+      val ((fx, fy), (tx, ty)) =
+        (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
+      val ds =
+      {
+        val min = fy min ty
+        val max = fy max ty
+        visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+      }
+
+      if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies)
+      else {
+        val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
+        path.moveTo(fx, fy)
+
+        val coords = ((fx, fy) :: ds ::: List((tx, ty)))
+        val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
+
+        val (dx2, dy2) =
+          ((dx, dy) /: coords.sliding(3))({
+            case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => {
+              val (dx2, dy2) = (rx - lx, ry - ly)
+
+              path.curveTo(lx + slack * dx , ly + slack * dy,
+                           mx - slack * dx2, my - slack * dy2,
+                           mx              , my)
+              (dx2, dy2)
+            }
+          })
+
+        val (lx, ly) = ds.last
+        path.curveTo(lx + slack * dx2, ly + slack * dy2,
+                     tx - slack * dx2, ty - slack * dy2,
+                     tx              , ty)
+
+        if (dummies) {
+          ds.foreach({
+              case (x, y) => {
+                val at = AffineTransform.getTranslateInstance(x, y)
+                Dummy.paint_transformed(g, visualizer, None, at)
+              }
+            })
+        }
+
+        g.setStroke(stroke)
+        g.setColor(visualizer.Color(peer))
+        g.draw(path)
+
+        if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
+      }
+    }
+  }
+
+  object Arrow_Head
+  {
+    type Point = (Double, Double)
+
+    private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] =
+    {
+      def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
+      {
+        val i = path.getPathIterator(null, 1.0)
+        val seg = Array[Double](0,0,0,0,0,0)
+        var p1 = (0.0, 0.0)
+        var p2 = (0.0, 0.0)
+        while (!i.isDone()) {
+          i.currentSegment(seg) match {
+            case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
+            case PathIterator.SEG_LINETO =>
+              p1 = p2
+              p2 = (seg(0), seg(1))
+
+              if(shape.contains(seg(0), seg(1)))
+                return Some((p1, p2))
+            case _ =>
+          }
+          i.next()
+        }
+        None
+      }
+
+      def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] =
+      {
+        val ((fx, fy), (tx, ty)) = line
+        if (shape.contains(fx, fy) == shape.contains(tx, ty))
+          None
+        else {
+          val (dx, dy) = (fx - tx, fy - ty)
+          if ((dx * dx + dy * dy) < 1.0) {
+            val at = AffineTransform.getTranslateInstance(fx, fy)
+            at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
+            Some(at)
+          }
+          else {
+            val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0)
+            if (shape.contains(fx, fy) == shape.contains(mx, my))
+              binary_search(((mx, my), (tx, ty)), shape)
+            else
+              binary_search(((fx, fy), (mx, my)), shape)
+          }
+        }
+      }
+
+      intersecting_line(path, shape) match {
+        case None => None
+        case Some(line) => binary_search(line, shape)
+      }
+    }
+
+    def paint(g: Graphics2D, path: GeneralPath, shape: Shape)
+    {
+      position(path, shape) match {
+        case None =>
+        case Some(at) =>
+          val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3)
+          arrow.moveTo(0, 0)
+          arrow.lineTo(-10, 4)
+          arrow.lineTo(-6, 0)
+          arrow.lineTo(-10, -4)
+          arrow.lineTo(0, 0)
+          arrow.transform(at)
+
+          g.fill(arrow)
+      }
+    }
+  }
+}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,298 +0,0 @@
-/*  Title:      Tools/Graphview/src/graph_panel.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Graphview Java2D drawing panel.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import java.awt.{Dimension, Graphics2D, Point, Rectangle}
-import java.awt.geom.{AffineTransform, Point2D}
-import java.awt.image.BufferedImage
-import javax.swing.{JScrollPane, JComponent}
-
-import scala.swing.{Panel, ScrollPane}
-import scala.swing.event._
-
-
-class Graph_Panel(
-    val visualizer: Visualizer,
-    make_tooltip: (JComponent, Int, Int, XML.Body) => String)
-  extends ScrollPane
-{
-  panel =>
-
-  tooltip = ""
-
-  override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
-    override def getToolTipText(event: java.awt.event.MouseEvent): String =
-      node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
-        case Some(name) =>
-          visualizer.model.complete.get_node(name).content match {
-            case Nil => null
-            case content => make_tooltip(panel.peer, event.getX, event.getY, content)
-          }
-        case None => null
-      }
-  }
-
-  peer.setWheelScrollingEnabled(false)
-  focusable = true
-  requestFocus()
-
-  horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
-  verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
-
-  def node(at: Point2D): Option[String] =
-    visualizer.model.visible_nodes_iterator
-      .find(name => visualizer.Drawer.shape(visualizer.gfx, Some(name)).contains(at))
-
-  def refresh()
-  {
-    if (paint_panel != null) {
-      paint_panel.set_preferred_size()
-      paint_panel.repaint()
-    }
-  }
-
-  def fit_to_window() = {
-    Transform.fit_to_window()
-    refresh()
-  }
-
-  val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
-
-  def rescale(s: Double)
-  {
-    Transform.scale = s
-    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt)
-    refresh()
-  }
-
-  def apply_layout() = visualizer.Coordinates.update_layout()
-
-  private class Paint_Panel extends Panel {
-    def set_preferred_size() {
-        val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
-        val s = Transform.scale_discrete
-        val (px, py) = Transform.padding
-
-        preferredSize = new Dimension((math.abs(maxX - minX + px) * s).toInt,
-                                      (math.abs(maxY - minY + py) * s).toInt)
-
-        revalidate()
-      }
-
-    override def paint(g: Graphics2D) {
-      super.paintComponent(g)
-      g.transform(Transform())
-
-      visualizer.Drawer.paint_all_visible(g, true)
-    }
-  }
-  private val paint_panel = new Paint_Panel
-  contents = paint_panel
-
-  listenTo(keys)
-  listenTo(mouse.moves)
-  listenTo(mouse.clicks)
-  listenTo(mouse.wheel)
-  reactions += Interaction.Mouse.react
-  reactions += Interaction.Keyboard.react
-  reactions += {
-      case KeyTyped(_, _, _, _) => {repaint(); requestFocus()}
-      case MousePressed(_, _, _, _, _) => {repaint(); requestFocus()}
-      case MouseDragged(_, _, _) => {repaint(); requestFocus()}
-      case MouseWheelMoved(_, _, _, _) => {repaint(); requestFocus()}
-      case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()}
-      case MouseMoved(_, _, _) => repaint()
-    }
-
-  visualizer.model.Colors.events += { case _ => repaint() }
-  visualizer.model.Mutators.events += { case _ => repaint() }
-
-  apply_layout()
-  rescale(1.0)
-
-  private object Transform
-  {
-    val padding = (100, 40)
-
-    private var _scale: Double = 1.0
-    def scale: Double = _scale
-    def scale_=(s: Double)
-    {
-      _scale = (s min 10) max 0.1
-    }
-    def scale_discrete: Double =
-      (_scale * visualizer.font_size).round.toDouble / visualizer.font_size
-
-    def apply() = {
-      val (minX, minY, _, _) = visualizer.Coordinates.bounds()
-
-      val at = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
-      at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2)
-      at
-    }
-
-    def fit_to_window() {
-      if (visualizer.model.visible_nodes_iterator.isEmpty)
-        rescale(1.0)
-      else {
-        val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
-
-        val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
-        val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy)
-        rescale(sx min sy)
-      }
-    }
-
-    def pane_to_graph_coordinates(at: Point2D): Point2D = {
-      val s = Transform.scale_discrete
-      val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null)
-
-      p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s)
-      p
-    }
-  }
-
-  object Interaction {
-    object Keyboard {
-      import scala.swing.event.Key._
-
-      val react: PartialFunction[Event, Unit] = {
-        case KeyTyped(_, c, m, _) => typed(c, m)
-      }
-
-      def typed(c: Char, m: Modifiers) =
-        (c, m) match {
-          case ('+', _) => rescale(Transform.scale * 5.0/4)
-          case ('-', _) => rescale(Transform.scale * 4.0/5)
-          case ('0', _) => Transform.fit_to_window()
-          case ('1', _) => visualizer.Coordinates.update_layout()
-          case ('2', _) => Transform.fit_to_window()
-          case _ =>
-        }
-    }
-
-    object Mouse {
-      import scala.swing.event.Key.Modifier._
-      type Modifiers = Int
-      type Dummy = ((String, String), Int)
-
-      private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
-
-      val react: PartialFunction[Event, Unit] = {
-        case MousePressed(_, p, _, _, _) => pressed(p)
-        case MouseDragged(_, to, _) => {
-            drag(draginfo, to)
-            val (_, p, d) = draginfo
-            draginfo = (to, p, d)
-          }
-        case MouseWheelMoved(_, p, _, r) => wheel(r, p)
-        case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e)
-      }
-
-      def dummy(at: Point2D): Option[Dummy] =
-        visualizer.model.visible_edges_iterator.map({
-            i => visualizer.Coordinates(i).zipWithIndex.map((i, _))
-          }).flatten.find({
-            case (_, ((x, y), _)) =>
-              visualizer.Drawer.shape(visualizer.gfx, None).contains(at.getX() - x, at.getY() - y)
-          }) match {
-            case None => None
-            case Some((name, (_, index))) => Some((name, index))
-          }
-
-      def pressed(at: Point) {
-        val c = Transform.pane_to_graph_coordinates(at)
-        val l = node(c) match {
-          case Some(l) =>
-            if (visualizer.Selection(l)) visualizer.Selection() else List(l)
-          case None => Nil
-        }
-        val d = l match {
-          case Nil => dummy(c) match {
-              case Some(d) => List(d)
-              case None => Nil
-          }
-
-          case _ => Nil
-        }
-
-        draginfo = (at, l, d)
-      }
-
-      def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) {
-        import javax.swing.SwingUtilities
-
-        val c = Transform.pane_to_graph_coordinates(at)
-        val p = node(c)
-
-        def left_click() {
-          (p, m) match {
-            case (Some(l), Control) => visualizer.Selection.add(l)
-            case (None, Control) =>
-
-            case (Some(l), Shift) => visualizer.Selection.add(l)
-            case (None, Shift) =>
-
-            case (Some(l), _) => visualizer.Selection.set(List(l))
-            case (None, _) => visualizer.Selection.clear
-          }
-        }
-
-        def right_click() {
-          val menu = Popups(panel, p, visualizer.Selection())
-          menu.show(panel.peer, at.x, at.y)
-        }
-
-        if (clicks < 2) {
-          if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
-          else left_click()
-        }
-      }
-
-      def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) {
-        val (from, p, d) = draginfo
-
-        val s = Transform.scale_discrete
-        val (dx, dy) = (to.x - from.x, to.y - from.y)
-        (p, d) match {
-          case (Nil, Nil) => {
-            val r = panel.peer.getViewport.getViewRect
-            r.translate(-dx, -dy)
-
-            paint_panel.peer.scrollRectToVisible(r)
-          }
-
-          case (Nil, ds) =>
-            ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s)))
-
-          case (ls, _) =>
-            ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s)))
-        }
-      }
-
-      def wheel(rotation: Int, at: Point) {
-        val at2 = Transform.pane_to_graph_coordinates(at)
-        // > 0 -> up
-        rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4))
-
-        // move mouseposition to center
-        Transform().transform(at2, at2)
-        val r = panel.peer.getViewport.getViewRect
-        val (width, height) = (r.getWidth, r.getHeight)
-        paint_panel.peer.scrollRectToVisible(
-          new Rectangle((at2.getX() - width / 2).toInt,
-                        (at2.getY() - height / 2).toInt,
-                        width.toInt,
-                        height.toInt)
-        )
-      }
-    }
-  }
-}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/layout_pendulum.scala
--- a/src/Tools/Graphview/src/layout_pendulum.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,275 +0,0 @@
-/*  Title:      Tools/Graphview/src/layout_pendulum.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Pendulum DAG layout algorithm.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-
-object Layout_Pendulum
-{
-  type Key = String
-  type Point = (Double, Double)
-  type Coordinates = Map[Key, Point]
-  type Level = List[Key]
-  type Levels = List[Level]
-  type Dummies = (Model.Graph, List[Key], Map[Key, Int])
-
-  case class Layout(nodes: Coordinates, dummies: Map[(Key, Key), List[Point]])
-  val empty_layout = Layout(Map.empty, Map.empty)
-
-  val pendulum_iterations = 10
-  val minimize_crossings_iterations = 40
-
-  def apply(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout =
-  {
-    if (graph.is_empty) empty_layout
-    else {
-      val initial_levels = level_map(graph)
-
-      val (dummy_graph, dummies, dummy_levels) =
-        ((graph, Map.empty[(Key, Key), List[Key]], initial_levels) /: graph.keys_iterator) {
-          case ((graph, dummies, levels), from) =>
-            ((graph, dummies, levels) /: graph.imm_succs(from)) {
-              case ((graph, dummies, levels), to) =>
-                if (levels(to) - levels(from) <= 1) (graph, dummies, levels)
-                else {
-                  val (next, ds, ls) = add_dummies(graph, from, to, levels)
-                  (next, dummies + ((from, to) -> ds), ls)
-                }
-            }
-        }
-
-      val levels = minimize_crossings(dummy_graph, level_list(dummy_levels))
-
-      val initial_coordinates: Coordinates =
-        (((Map.empty[Key, Point], 0.0) /: levels) {
-          case ((coords1, y), level) =>
-            ((((coords1, 0.0) /: level) {
-              case ((coords2, x), key) =>
-                val s = if (graph.defined(key)) graph.get_node(key).name else "X"
-                (coords2 + (key -> (x, y)), x + box_distance)
-            })._1, y + box_height(level.length))
-        })._1
-
-      val coords = pendulum(dummy_graph, box_distance, levels, initial_coordinates)
-
-      val dummy_coords =
-        (Map.empty[(Key, Key), List[Point]] /: dummies.keys) {
-          case (map, key) => map + (key -> dummies(key).map(coords(_)))
-        }
-
-      Layout(coords, dummy_coords)
-    }
-  }
-
-
-  def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies =
-  {
-    val ds =
-      ((levels(from) + 1) until levels(to))
-      .map("%s$%s$%d" format (from, to, _)).toList
-
-    val ls =
-      (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) {
-        case (ls, (l, d)) => ls + (d -> l)
-      }
-
-    val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info))
-    val graph2 =
-      (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
-        case (g, List(x, y)) => g.add_edge(x, y)
-      }
-    (graph2, ds, ls)
-  }
-
-  def level_map(graph: Model.Graph): Map[Key, Int] =
-    (Map.empty[Key, Int] /: graph.topological_order) {
-      (levels, key) => {
-        val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
-        levels + (key -> lev)
-      }
-    }
-
-  def level_list(map: Map[Key, Int]): Levels =
-  {
-    val max_lev = (-1 /: map) { case (m, (_, l)) => m max l }
-    val buckets = new Array[Level](max_lev + 1)
-    for (l <- 0 to max_lev) { buckets(l) = Nil }
-    for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
-    buckets.iterator.map(_.sorted).toList
-  }
-
-  def count_crossings(graph: Model.Graph, levels: Levels): Int =
-  {
-    def in_level(ls: Levels): Int = ls match {
-      case List(top, bot) =>
-        top.iterator.zipWithIndex.map {
-          case (outer_parent, outer_parent_index) =>
-            graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_))
-            .map(outer_child =>
-              (0 until outer_parent_index)
-              .map(inner_parent =>
-                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
-                .filter(inner_child => outer_child < inner_child)
-                .size
-              ).sum
-            ).sum
-        }.sum
-
-      case _ => 0
-    }
-
-    levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
-  }
-
-  def minimize_crossings(graph: Model.Graph, levels: Levels): Levels =
-  {
-    def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
-      child.map(k => {
-          val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
-          val weight =
-            (0.0 /: ps) { (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1)
-          (k, weight)
-      }).sortBy(_._2).map(_._1)
-
-    def resort(levels: Levels, top_down: Boolean) = top_down match {
-      case true =>
-        (List[Level](levels.head) /: levels.tail) {
-          (tops, bot) => resort_level(tops.head, bot, top_down) :: tops
-        }.reverse
-
-      case false =>
-        (List[Level](levels.reverse.head) /: levels.reverse.tail) {
-          (bots, top) => resort_level(bots.head, top, top_down) :: bots
-        }
-      }
-
-    ((levels, count_crossings(graph, levels), true) /: (1 to minimize_crossings_iterations)) {
-      case ((old_levels, old_crossings, top_down), _) => {
-          val new_levels = resort(old_levels, top_down)
-          val new_crossings = count_crossings(graph, new_levels)
-          if (new_crossings < old_crossings)
-            (new_levels, new_crossings, !top_down)
-          else
-            (old_levels, old_crossings, !top_down)
-      }
-    }._1
-  }
-
-  def pendulum(graph: Model.Graph, box_distance: Double,
-    levels: Levels, coords: Map[Key, Point]): Coordinates =
-  {
-    type Regions = List[List[Region]]
-
-    def iteration(regions: Regions, coords: Coordinates, top_down: Boolean)
-      : (Regions, Coordinates, Boolean) =
-    {
-      val (nextr, nextc, moved) =
-      ((List.empty[List[Region]], coords, false) /:
-       (if (top_down) regions else regions.reverse)) {
-        case ((tops, coords, prev_moved), bot) => {
-            val nextb = collapse(coords, bot, top_down)
-            val (nextc, this_moved) = deflect(coords, nextb, top_down)
-            (nextb :: tops, nextc, prev_moved || this_moved)
-        }
-      }
-
-      (nextr.reverse, nextc, moved)
-    }
-
-    def collapse(coords: Coordinates, level: List[Region], top_down: Boolean): List[Region] =
-    {
-      if (level.size <= 1) level
-      else {
-        var next = level
-        var regions_changed = true
-        while (regions_changed) {
-          regions_changed = false
-          for (i <- (next.length to 1)) {
-            val (r1, r2) = (next(i-1), next(i))
-            val d1 = r1.deflection(coords, top_down)
-            val d2 = r2.deflection(coords, top_down)
-
-            if (// Do regions touch?
-                r1.distance(coords, r2) <= box_distance &&
-                // Do they influence each other?
-                (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0))
-            {
-              regions_changed = true
-              r1.nodes = r1.nodes ::: r2.nodes
-              next = next.filter(next.indexOf(_) != i)
-            }
-          }
-        }
-        next
-      }
-    }
-
-    def deflect(coords: Coordinates, level: List[Region], top_down: Boolean)
-        : (Coordinates, Boolean) =
-    {
-      ((coords, false) /: (0 until level.length)) {
-        case ((coords, moved), i) => {
-            val r = level(i)
-            val d = r.deflection(coords, top_down)
-            val offset = {
-              if (i == 0 && d <= 0) d
-              else if (i == level.length - 1 && d >= 0) d
-              else if (d < 0) {
-                val prev = level(i-1)
-                (-(r.distance(coords, prev) - box_distance)) max d
-              }
-              else {
-                val next = level(i+1)
-                (r.distance(coords, next) - box_distance) min d
-              }
-            }
-
-            (r.move(coords, offset), moved || (d != 0))
-        }
-      }
-    }
-
-    val regions = levels.map(level => level.map(new Region(graph, _)))
-
-    ((regions, coords, true, true) /: (1 to pendulum_iterations)) {
-      case ((regions, coords, top_down, moved), _) =>
-        if (moved) {
-          val (nextr, nextc, m) = iteration(regions, coords, top_down)
-          (nextr, nextc, !top_down, m)
-        }
-        else (regions, coords, !top_down, moved)
-    }._2
-  }
-
-  private class Region(val graph: Model.Graph, node: Key)
-  {
-    var nodes: List[Key] = List(node)
-
-    def left(coords: Coordinates): Double = nodes.map(coords(_)._1).min
-    def right(coords: Coordinates): Double = nodes.map(coords(_)._1).max
-
-    def distance(coords: Coordinates, to: Region): Double =
-      math.abs(left(coords) - to.left(coords)) min
-      math.abs(right(coords) - to.right(coords))
-
-    def deflection(coords: Coordinates, use_preds: Boolean) =
-      nodes.map(k => (coords(k)._1,
-                      if (use_preds) graph.imm_preds(k).toList  // FIXME iterator
-                      else graph.imm_succs(k).toList))
-      .map({ case (x, as) => as.map(coords(_)._1 - x).sum / (as.length max 1) })
-      .sum / nodes.length
-
-    def move(coords: Coordinates, by: Double): Coordinates =
-      (coords /: nodes) {
-        case (cs, node) =>
-          val (x, y) = cs(node)
-          cs + (node -> (x + by, y))
-      }
-  }
-}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,125 +0,0 @@
-/*  Title:      Tools/Graphview/src/main_panel.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Graph Panel wrapper.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-import isabelle.graphview.Mutators._
-
-import scala.collection.JavaConversions._
-import scala.swing.{BorderPanel, Button, BoxPanel,
-  Orientation, Swing, CheckBox, Action, FileChooser}
-
-import java.io.{File => JFile}
-import java.awt.{Color, Dimension, Graphics2D}
-import java.awt.geom.Rectangle2D
-import java.awt.image.BufferedImage
-import javax.imageio.ImageIO
-import javax.swing.border.EmptyBorder
-import javax.swing.JComponent
-
-
-class Main_Panel(graph: Model.Graph) extends BorderPanel
-{
-  focusable = true
-  requestFocus()
-
-  val model = new Model(graph)
-  val visualizer = new Visualizer(model)
-
-  def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String = null
-  val graph_panel = new Graph_Panel(visualizer, make_tooltip)
-
-  listenTo(keys)
-  reactions += graph_panel.reactions
-
-  val mutator_dialog = new Mutator_Dialog(visualizer, model.Mutators, "Filters", "Hide", false)
-
-  val color_dialog = new Mutator_Dialog(visualizer, model.Colors, "Colorations")
-
-  private val chooser = new FileChooser()
-  chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
-  chooser.title = "Save Image (.png or .pdf)"
-
-  val options_panel = new BoxPanel(Orientation.Horizontal) {
-    border = new EmptyBorder(0, 0, 10, 0)
-
-    contents += Swing.HGlue
-    contents += new CheckBox(){
-      selected = visualizer.arrow_heads
-      action = Action("Arrow Heads"){
-        visualizer.arrow_heads = selected
-        graph_panel.repaint()
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Save Image"){
-        chooser.showSaveDialog(this) match {
-          case FileChooser.Result.Approve => export(chooser.selectedFile)
-          case _ =>
-        }
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += graph_panel.zoom
-
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Apply Layout"){
-        graph_panel.apply_layout()
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Fit to Window"){
-        graph_panel.fit_to_window()
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Colorations"){
-        color_dialog.open
-      }
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += new Button{
-      action = Action("Filters"){
-        mutator_dialog.open
-      }
-    }
-  }
-
-  add(graph_panel, BorderPanel.Position.Center)
-  add(options_panel, BorderPanel.Position.North)
-
-  private def export(file: JFile)
-  {
-    val (x0, y0, x1, y1) = visualizer.Coordinates.bounds
-    val w = (math.abs(x1 - x0) + 400).toInt
-    val h = (math.abs(y1 - y0) + 200).toInt
-
-    def paint(gfx: Graphics2D)
-    {
-      gfx.setColor(Color.WHITE)
-      gfx.fill(new Rectangle2D.Double(0, 0, w, h))
-
-      gfx.translate(- x0 + 200, - y0 + 100)
-      visualizer.Drawer.paint_all_visible(gfx, false)
-    }
-
-    try {
-      val name = file.getName
-      if (name.endsWith(".png")) Graphics_File.write_png(file, paint _, w, h)
-      else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint _, w, h)
-      else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
-    }
-    catch {
-      case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
-    }
-  }
-}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/model.scala
--- a/src/Tools/Graphview/src/model.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-/*  Title:      Tools/Graphview/src/model.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Internal graph representation.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-import isabelle.graphview.Mutators._
-
-import java.awt.Color
-
-
-class Mutator_Container(val available: List[Mutator]) {
-    type Mutator_Markup = (Boolean, Color, Mutator)
-    
-    val events = new Mutator_Event.Bus
-    
-    private var _mutators : List[Mutator_Markup] = Nil
-    def apply() = _mutators
-    def apply(mutators: List[Mutator_Markup]){
-      _mutators = mutators
-      
-      events.event(Mutator_Event.NewList(mutators))
-    }    
-
-    def add(mutator: Mutator_Markup) = {
-      _mutators = _mutators ::: List(mutator)
-      
-      events.event(Mutator_Event.Add(mutator))
-    }
-}
-
-
-object Model
-{
-  /* node info */
-
-  sealed case class Info(name: String, content: XML.Body)
-
-  val empty_info: Info = Info("", Nil)
-
-  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
-  {
-    import XML.Decode._
-
-    val (name, content) = pair(string, x => x)(body)
-    Info(name, content)
-  }
-
-
-  /* graph */
-
-  type Graph = isabelle.Graph[String, Info]
-
-  val decode_graph: XML.Decode.T[Graph] =
-    isabelle.Graph.decode(XML.Decode.string, decode_info)
-}
-
-class Model(private val graph: Model.Graph) {  
-  val Mutators = new Mutator_Container(
-    List(
-      Node_Expression(".*", false, false, false),
-      Node_List(Nil, false, false, false),
-      Edge_Endpoints("", ""),
-      Add_Node_Expression(""),
-      Add_Transitive_Closure(true, true)
-    ))
-  
-  val Colors = new Mutator_Container(
-    List(
-      Node_Expression(".*", false, false, false),
-      Node_List(Nil, false, false, false)
-    ))  
-  
-  def visible_nodes_iterator: Iterator[String] = current.keys_iterator
-  
-  def visible_edges_iterator: Iterator[(String, String)] =
-    current.keys_iterator.flatMap(k => current.imm_succs(k).iterator.map((k, _)))
-  
-  def complete = graph
-  def current: Model.Graph =
-      (graph /: Mutators()) {
-        case (g, (enabled, _, mutator)) => {
-          if (!enabled) g
-          else mutator.mutate(graph, g)
-        }
-      }
-    
-  private var _colors = Map.empty[String, Color]
-  def colors = _colors
-  
-  private def build_colors() {
-    _colors = 
-      (Map.empty[String, Color] /: Colors()) ({
-          case (colors, (enabled, color, mutator)) => {
-              (colors /: mutator.mutate(graph, graph).keys_iterator) ({
-                  case (colors, k) => colors + (k -> color)
-                })
-            }
-      })
-  }
-  Colors.events += { case _ => build_colors() }
-}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/mutator.scala
--- a/src/Tools/Graphview/src/mutator.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,199 +0,0 @@
-/*  Title:      Tools/Graphview/src/mutator.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Filters and add-operations on graphs.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import java.awt.Color
-import scala.collection.immutable.SortedSet
-
-
-trait Mutator
-{
-  val name: String
-  val description: String
-  def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph
-
-  override def toString: String = name
-}
-
-trait Filter extends Mutator
-{
-  def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub)
-  def filter(sub: Model.Graph) : Model.Graph
-}
-
-object Mutators {
-  type Mutator_Markup = (Boolean, Color, Mutator)
-  
-  val Enabled = true
-  val Disabled = false
-  
-  def create(visualizer: Visualizer, m: Mutator): Mutator_Markup =
-    (Mutators.Enabled, visualizer.Colors.next, m)
-
-  class Graph_Filter(val name: String, val description: String,
-    pred: Model.Graph => Model.Graph)
-  extends Filter
-  {
-    def filter(sub: Model.Graph) : Model.Graph = pred(sub)
-  }
-
-  class Graph_Mutator(val name: String, val description: String,
-    pred: (Model.Graph, Model.Graph) => Model.Graph)
-  extends Mutator
-  {
-    def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph =
-          pred(complete, sub)
-  }
-
-  class Node_Filter(name: String, description: String,
-    pred: (Model.Graph, String) => Boolean)
-    extends Graph_Filter (
-
-    name,
-    description,
-    g => g.restrict(pred(g, _))
-  )
-
-  class Edge_Filter(name: String, description: String,
-    pred: (Model.Graph, String, String) => Boolean)
-    extends Graph_Filter (
-
-    name,
-    description,
-    g => (g /: g.dest) {
-      case (graph, ((from, _), tos)) => {
-        (graph /: tos) {
-          (gr, to) => if (pred(gr, from, to)) gr
-                      else gr.del_edge(from, to)
-        }
-      }
-    }
-  )
-
-  class Node_Family_Filter(name: String, description: String,
-      reverse: Boolean, parents: Boolean, children: Boolean,
-      pred: (Model.Graph, String) => Boolean)
-    extends Node_Filter(
-
-    name,
-    description,
-    (g, k) => reverse != (
-      pred(g, k) ||
-      (parents && g.all_preds(List(k)).exists(pred(g, _))) ||
-      (children && g.all_succs(List(k)).exists(pred(g, _)))
-    )
-  )  
-  
-  case class Identity()
-    extends Graph_Filter(
-
-    "Identity",
-    "Does not change the graph.",
-    g => g
-  )
-
-  case class Node_Expression(regex: String,
-    reverse: Boolean, parents: Boolean, children: Boolean)
-    extends Node_Family_Filter(
-
-    "Filter by Name",
-    "Only shows or hides all nodes with any family member's name matching " +
-    "a regex.",
-    reverse,
-    parents,
-    children,
-    (g, k) => (regex.r findFirstIn k).isDefined
-  )
-
-  case class Node_List(list: List[String],
-    reverse: Boolean, parents: Boolean, children: Boolean)
-    extends Node_Family_Filter(
-
-    "Filter by Name List",
-    "Only shows or hides all nodes with any family member's name matching " +
-    "any string in a comma separated list.",
-    reverse,
-    parents,
-    children,
-    (g, k) => list.exists(_ == k)
-  )
-
-  case class Edge_Endpoints(source: String, dest: String)
-    extends Edge_Filter(
-
-    "Hide edge",
-    "Hides the edge whose endpoints match strings.",
-    (g, s, d) => !(s == source && d == dest)
-  )
-
-  private def add_node_group(from: Model.Graph, to: Model.Graph,
-    keys: List[String]) = {
-    
-    // Add Nodes
-    val with_nodes = 
-      (to /: keys) {
-        (graph, key) => graph.default_node(key, from.get_node(key))
-      }
-    
-    // Add Edges
-    (with_nodes /: keys) {
-      (gv, key) => {
-        def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
-          (g /: keys) {
-            (graph, end) => {
-              if (!graph.keys_iterator.contains(end)) graph
-              else {
-                if (succs) graph.add_edge(key, end)
-                else graph.add_edge(end, key)
-              }
-            }
-          }
-
-        
-        add_edges(
-          add_edges(gv, from.imm_preds(key), false),
-          from.imm_succs(key), true
-        )
-      }
-    }
-  }  
-  
-  case class Add_Node_Expression(regex: String)
-    extends Graph_Mutator(
-
-    "Add by name",
-    "Adds every node whose name matches the regex. " +
-    "Adds all relevant edges.",
-    (complete, sub) => {
-      add_node_group(complete, sub, complete.keys.filter(
-          k => (regex.r findFirstIn k).isDefined
-        ).toList)
-    }
-  )
-  
-  case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
-    extends Graph_Mutator(
-
-    "Add transitive closure",
-    "Adds all family members of all current nodes.",
-    (complete, sub) => {     
-      val withparents = 
-        if (parents)
-          add_node_group(complete, sub, complete.all_preds(sub.keys))
-        else
-          sub
-      
-      if (children)
-        add_node_group(complete, withparents, complete.all_succs(sub.keys))
-      else 
-        withparents
-    }
-  )
-}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/mutator_dialog.scala
--- a/src/Tools/Graphview/src/mutator_dialog.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,427 +0,0 @@
-/*  Title:      Tools/Graphview/src/mutator_dialog.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Mutator selection and configuration dialog.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import java.awt.Color
-import java.awt.FocusTraversalPolicy
-import javax.swing.JColorChooser
-import javax.swing.border.EmptyBorder
-import scala.collection.JavaConversions._
-import scala.swing._
-import isabelle.graphview.Mutators._
-import scala.swing.event.ValueChanged
-
-
-class Mutator_Dialog(
-    visualizer: Visualizer,
-    container: Mutator_Container,
-    caption: String,
-    reverse_caption: String = "Inverse",
-    show_color_chooser: Boolean = true)
-  extends Dialog
-{
-  type Mutator_Markup = (Boolean, Color, Mutator)
-  
-  title = caption
-  
-  private var _panels: List[Mutator_Panel] = Nil
-  private def panels = _panels
-  private def panels_= (panels: List[Mutator_Panel]) {
-    _panels = panels
-    paintPanels
-  }
-
-  container.events += {
-    case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
-    case Mutator_Event.NewList(ms) => panels = getPanels(ms)
-  }
-
-  override def open() {
-    if (!visible)
-      panels = getPanels(container())
-
-    super.open
-  }
-
-  minimumSize = new Dimension(700, 200)
-  preferredSize = new Dimension(1000, 300)
-  peer.setFocusTraversalPolicy(focusTraversal)
-
-  private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] =
-    m.filter(_ match {case (_, _, Identity()) => false; case _ => true})
-    .map(m => new Mutator_Panel(m))
-
-  private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] = 
-    panels.map(panel => panel.get_Mutator_Markup)
-
-  private def movePanelUp(m: Mutator_Panel) = {
-    def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
-      case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs)
-      case _ => l
-    }
-
-    panels = moveUp(panels)
-  }
-
-  private def movePanelDown(m: Mutator_Panel) = {
-    def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
-      case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs)
-      case _ => l
-    }
-
-    panels = moveDown(panels)
-  }
-
-  private def removePanel(m: Mutator_Panel) = {
-    panels = panels.filter(_ != m).toList
-  }
-
-  private def addPanel(m: Mutator_Panel) = {
-    panels = panels ::: List(m)
-  }
-
-  def paintPanels = {
-    focusTraversal.clear
-    filterPanel.contents.clear
-    panels.map(x => {
-        filterPanel.contents += x
-        focusTraversal.addAll(x.focusList)
-      })
-    filterPanel.contents += Swing.VGlue
-
-    focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component])
-    focusTraversal.add(addButton.peer)
-    focusTraversal.add(applyButton.peer)
-    focusTraversal.add(cancelButton.peer)
-    filterPanel.revalidate
-    filterPanel.repaint
-  }
-
-  val filterPanel = new BoxPanel(Orientation.Vertical) {}
-
-  private val mutatorBox = new ComboBox[Mutator](container.available)
-
-  private val addButton: Button = new Button{
-    action = Action("Add") {
-      addPanel(
-        new Mutator_Panel((true, visualizer.Colors.next,
-                           mutatorBox.selection.item))
-      )
-    }
-  }
-
-  private val applyButton = new Button{
-    action = Action("Apply") {
-      container(getMutators(panels))
-    }
-  }
-
-  private val resetButton = new Button {
-    action = Action("Reset") {
-      panels = getPanels(container())
-    }
-  }
-
-  private val cancelButton = new Button{
-      action = Action("Close") {
-        close
-      }
-    }
-  defaultButton = cancelButton
-
-  private val botPanel = new BoxPanel(Orientation.Horizontal) {
-    border = new EmptyBorder(10, 0, 0, 0)
-
-    contents += mutatorBox
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += addButton
-
-    contents += Swing.HGlue
-    contents += Swing.RigidBox(new Dimension(30, 0))
-    contents += applyButton
-
-    contents += Swing.RigidBox(new Dimension(5, 0))
-    contents += resetButton
-
-    contents += Swing.RigidBox(new Dimension(5, 0))
-    contents += cancelButton
-  }
-  
-  contents = new BorderPanel {
-    border = new EmptyBorder(5, 5, 5, 5)
-
-    add(new ScrollPane(filterPanel), BorderPanel.Position.Center)
-    add(botPanel, BorderPanel.Position.South)
-  }
-
-  private class Mutator_Panel(initials: Mutator_Markup)
-    extends BoxPanel(Orientation.Horizontal)
-  {
-    private val (_enabled, _color, _mutator) = initials
-    
-    private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs()
-    var focusList = List.empty[java.awt.Component]
-    private val enabledBox = new iCheckBox("Enabled", _enabled)
-
-    border = new EmptyBorder(5, 5, 5, 5)
-    maximumSize = new Dimension(Integer.MAX_VALUE, 30)
-    background = _color
-
-    contents += new Label(_mutator.name) {
-      preferredSize = new Dimension(175, 20)
-      horizontalAlignment = Alignment.Left
-      if (_mutator.description != "") tooltip = _mutator.description
-    }
-    contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += enabledBox
-    contents += Swing.RigidBox(new Dimension(5, 0))
-    focusList = enabledBox.peer :: focusList
-    inputs.map( _ match {
-      case (n, c) => {
-          contents += Swing.RigidBox(new Dimension(10, 0))
-        if (n != "") {
-          contents += new Label(n)
-          contents += Swing.RigidBox(new Dimension(5, 0))
-        }
-        contents += c.asInstanceOf[Component]
-        
-        focusList = c.asInstanceOf[Component].peer :: focusList
-      }
-      case _ =>
-    })
-
-    {
-      val t = this
-      contents += Swing.HGlue
-      contents += Swing.RigidBox(new Dimension(10, 0))
-
-      if (show_color_chooser) {
-        contents += new Button {
-          maximumSize = new Dimension(20, 20)
-
-          action = Action("Color") {
-            t.background =
-              JColorChooser.showDialog(t.peer, "Choose new Color", t.background)
-          }
-
-          focusList = this.peer :: focusList
-        }
-        contents += Swing.RigidBox(new Dimension(2, 0))
-      }
-
-      contents += new Button {
-        maximumSize = new Dimension(20, 20)
-
-        action = Action("Up") {
-          movePanelUp(t)
-        }
-
-        focusList = this.peer :: focusList
-      }
-      contents += Swing.RigidBox(new Dimension(2, 0))
-      contents += new Button {
-        maximumSize = new Dimension(20, 20)
-
-        action = Action("Down") {
-          movePanelDown(t)
-        }
-
-        focusList = this.peer :: focusList
-      }
-      contents += Swing.RigidBox(new Dimension(2, 0))
-      contents += new Button {
-        maximumSize = new Dimension(20, 20)
-
-        action = Action("Del") {
-          removePanel(t)
-        }
-
-        focusList = this.peer :: focusList
-      }
-    }
-
-    focusList = focusList.reverse
-
-    private def isRegex(regex: String): Boolean = {
-      try {
-        regex.r
-
-        true
-      } catch {
-        case _: java.util.regex.PatternSyntaxException =>  false
-      }
-    }
-   
-    def get_Mutator_Markup: Mutator_Markup = {
-      def regexOrElse(regex: String, orElse: String): String = {
-        if (isRegex(regex)) regex
-        else orElse
-      }
-      
-      val m = _mutator match {
-        case Identity() =>
-          Identity()
-        case Node_Expression(r, _, _, _) =>
-          Node_Expression(
-            regexOrElse(inputs(2)._2.getString, r),
-            inputs(3)._2.getBool,
-            // "Parents" means "Show parents" or "Matching Children"
-            inputs(1)._2.getBool,
-            inputs(0)._2.getBool
-          )
-        case Node_List(_, _, _, _) =>
-          Node_List(
-            inputs(2)._2.getString.split(',').filter(_ != "").toList,
-            inputs(3)._2.getBool,
-            // "Parents" means "Show parents" or "Matching Children"
-            inputs(1)._2.getBool,
-            inputs(0)._2.getBool
-          )
-        case Edge_Endpoints(_, _) =>
-          Edge_Endpoints(
-            inputs(0)._2.getString,
-            inputs(1)._2.getString
-          )
-        case Add_Node_Expression(r) =>
-          Add_Node_Expression(
-            regexOrElse(inputs(0)._2.getString, r)
-          )
-        case Add_Transitive_Closure(_, _) =>
-          Add_Transitive_Closure(
-            inputs(0)._2.getBool,
-            inputs(1)._2.getBool
-          )
-        case _ =>
-          Identity()
-      }
-      
-      (enabledBox.selected, background, m)
-    }
-    
-    private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match {
-      case Node_Expression(regex, reverse, check_parents, check_children) =>
-        List(
-          ("", new iCheckBox("Parents", check_children)),
-          ("", new iCheckBox("Children", check_parents)),
-          ("Regex", new iTextField(regex, x => !isRegex(x))),
-          ("", new iCheckBox(reverse_caption, reverse))
-        )
-      case Node_List(list, reverse, check_parents, check_children) =>
-        List(
-          ("", new iCheckBox("Parents", check_children)),
-          ("", new iCheckBox("Children", check_parents)),
-          ("Names", new iTextField(list.mkString(","))),
-          ("", new iCheckBox(reverse_caption, reverse))
-        )
-      case Edge_Endpoints(source, dest) =>
-        List(
-          ("Source", new iTextField(source)),
-          ("Destination", new iTextField(dest))
-        )
-      case Add_Node_Expression(regex) =>
-        List(
-          ("Regex", new iTextField(regex, x => !isRegex(x)))
-        )
-      case Add_Transitive_Closure(parents, children) =>
-        List(
-          ("", new iCheckBox("Parents", parents)),
-          ("", new iCheckBox("Children", children))
-        )
-      case _ => Nil
-    }
-  }
-
-  private trait Mutator_Input_Value
-  {
-    def getString: String
-    def getBool: Boolean
-  }
-
-  private class iTextField(t: String, colorator: String => Boolean)
-  extends TextField(t) with Mutator_Input_Value
-  {
-    def this(t: String) = this(t, x => false)
-
-    preferredSize = new Dimension(125, 18)
-
-    reactions += {
-      case ValueChanged(_) =>
-          if (colorator(text))
-            background = Color.RED
-          else
-            background = Color.WHITE
-    }
-
-    def getString = text
-    def getBool = true
-  }
-
-  private class iCheckBox(t: String, s: Boolean)
-  extends CheckBox(t) with Mutator_Input_Value
-  {
-    selected = s
-
-    def getString = ""
-    def getBool = selected
-  }
-
-  private object focusTraversal
-    extends FocusTraversalPolicy
-  {
-    private var items = Vector[java.awt.Component]()
-
-    def add(c: java.awt.Component) {
-      items = items :+ c
-    }
-    def addAll(cs: TraversableOnce[java.awt.Component]) {
-      items = items ++ cs
-    }
-    def clear() {
-      items = Vector[java.awt.Component]()
-    }
-
-    def getComponentAfter(root: java.awt.Container,
-                          c: java.awt.Component): java.awt.Component = {
-      val i = items.indexOf(c)
-      if (i < 0) {
-        getDefaultComponent(root)
-      } else {
-        items((i + 1) % items.length)
-      }
-    }
-
-    def getComponentBefore(root: java.awt.Container,
-                           c: java.awt.Component): java.awt.Component = {
-      val i = items.indexOf(c)
-      if (i < 0) {
-        getDefaultComponent(root)
-      } else {
-        items((i - 1) % items.length)
-      }
-    }
-
-    def getFirstComponent(root: java.awt.Container): java.awt.Component = {
-      if (items.length > 0)
-        items(0)
-      else
-        null
-    }
-
-    def getDefaultComponent(root: java.awt.Container)
-      : java.awt.Component = getFirstComponent(root)
-
-    def getLastComponent(root: java.awt.Container): java.awt.Component = {
-      if (items.length > 0)
-        items.last
-      else
-        null
-    }
-  }
-}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/mutator_event.scala
--- a/src/Tools/Graphview/src/mutator_event.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-/*  Title:      Tools/Graphview/src/mutator_event.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Events for dialog synchronization.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import scala.collection.mutable
-
-import java.awt.Color
-
-
-object Mutator_Event
-{
-  type Mutator_Markup = (Boolean, Color, Mutator)
-
-  sealed abstract class Message
-  case class Add(m: Mutator_Markup) extends Message
-  case class NewList(m: List[Mutator_Markup]) extends Message
-
-  type Receiver = PartialFunction[Message, Unit]
-
-  class Bus
-  {
-    private val receivers = new mutable.ListBuffer[Receiver]
-
-    def += (r: Receiver) { GUI_Thread.require {}; receivers += r }
-    def -= (r: Receiver) { GUI_Thread.require {}; receivers -= r }
-    def event(x: Message) { GUI_Thread.require {}; receivers.foreach(r => r(x)) }
-  }
-}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/popups.scala
--- a/src/Tools/Graphview/src/popups.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-/*  Title:      Tools/Graphview/src/popups.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-PopupMenu generation for graph components.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-import isabelle.graphview.Mutators._
-
-import javax.swing.JPopupMenu
-import scala.swing.{Action, Menu, MenuItem, Separator}
-
-
-object Popups
-{
-  def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String])
-    : JPopupMenu =
-  {
-    val visualizer = panel.visualizer
-
-    val add_mutator = visualizer.model.Mutators.add _
-    val curr = visualizer.model.current
-
-    def filter_context(ls: List[String], reverse: Boolean,
-                       caption: String, edges: Boolean) =
-      new Menu(caption) {
-        contents += new MenuItem(new Action("This") {
-            def apply =
-              add_mutator(
-                Mutators.create(visualizer,
-                  Node_List(ls, reverse, false, false)
-                )
-              )
-          })
-
-        contents += new MenuItem(new Action("Family") {
-            def apply =
-              add_mutator(
-                Mutators.create(visualizer,
-                  Node_List(ls, reverse, true, true)
-                )
-              )
-          })
-
-        contents += new MenuItem(new Action("Parents") {
-            def apply =
-              add_mutator(
-                Mutators.create(visualizer,
-                  Node_List(ls, reverse, false, true)
-                )
-              )
-          })
-
-        contents += new MenuItem(new Action("Children") {
-            def apply =
-              add_mutator(
-                Mutators.create(visualizer,
-                  Node_List(ls, reverse, true, false)
-                )
-              )
-          })
-
-
-        if (edges) {
-          val outs = ls.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
-                      .filter(_._2.size > 0).sortBy(_._1)
-          val ins = ls.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
-                      .filter(_._2.size > 0).sortBy(_._1)
-
-          if (outs.nonEmpty || ins.nonEmpty) {
-            contents += new Separator()
-
-            contents += new Menu("Edge") {
-              if (outs.nonEmpty) {
-                contents += new MenuItem("From...") {
-                  enabled = false
-                }
-
-                outs.map( e => {
-                  val (from, tos) = e
-                  contents += new Menu(from) {
-                    contents += new MenuItem("To..."){
-                      enabled = false
-                    }
-
-                    tos.toList.sorted.distinct.map( to => {
-                      contents += new MenuItem(new Action(to) {
-                        def apply =
-                          add_mutator(
-                            Mutators.create(visualizer, Edge_Endpoints(from, to))
-                          )
-                      })
-                    })
-                  }
-                })
-              }
-              if (outs.nonEmpty && ins.nonEmpty) {
-                contents += new Separator()
-              }
-              if (ins.nonEmpty) {
-                contents += new MenuItem("To...") {
-                  enabled = false
-                }
-
-                ins.map( e => {
-                  val (to, froms) = e
-                  contents += new Menu(to) {
-                    contents += new MenuItem("From..."){
-                      enabled = false
-                    }
-
-                    froms.toList.sorted.distinct.map( from => {
-                      contents += new MenuItem(new Action(from) {
-                        def apply =
-                          add_mutator(
-                            Mutators.create(visualizer, Edge_Endpoints(from, to))
-                          )
-                      })
-                    })
-                  }
-                })
-              }
-            }
-          }
-        }
-    }
-
-    val popup = new JPopupMenu()
-
-    popup.add(new MenuItem(new Action("Remove all filters") {
-          def apply = visualizer.model.Mutators(Nil)
-        }).peer
-    )
-    popup.add(new JPopupMenu.Separator)
-
-    if (under_mouse.isDefined) {
-      val v = under_mouse.get
-      popup.add(new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) {
-        enabled = false
-      }.peer)
-
-      popup.add(filter_context(List(v), true, "Hide", true).peer)
-      popup.add(filter_context(List(v), false, "Show only", false).peer)
-
-      popup.add(new JPopupMenu.Separator)
-    }
-    if (!selected.isEmpty) {
-      val text = {
-        if (selected.length > 1) {
-          "Multiple"
-        } else {
-          visualizer.Caption(selected.head)
-        }
-      }
-
-      popup.add(new MenuItem("Selected: %s".format(text)) {
-        enabled = false
-      }.peer)
-
-      popup.add(filter_context(selected, true, "Hide", true).peer)
-      popup.add(filter_context(selected, false, "Show only", false).peer)
-      popup.add(new JPopupMenu.Separator)
-    }
-
-
-    popup.add(new MenuItem(new Action("Fit to Window") {
-        def apply = panel.fit_to_window()
-      }).peer
-    )
-
-    popup
-  }
-}
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/shapes.scala
--- a/src/Tools/Graphview/src/shapes.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,255 +0,0 @@
-/*  Title:      Tools/Graphview/src/shapes.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Drawable shapes.
-*/
-
-package isabelle.graphview
-
-
-import java.awt.{BasicStroke, Graphics2D, Shape}
-import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator}
-
-
-object Shapes
-{
-  trait Node
-  {
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit
-  }
-
-  object Growing_Node extends Node
-  {
-    private val stroke =
-      new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Rectangle2D.Double =
-    {
-      val (x, y) = visualizer.Coordinates(peer.get)
-      val bounds = g.getFontMetrics.getStringBounds(visualizer.Caption(peer.get), g)
-      val w = bounds.getWidth + visualizer.pad_x
-      val h = bounds.getHeight + visualizer.pad_y
-      new Rectangle2D.Double(x - (w / 2), y - (h / 2), w, h)
-    }
-
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
-    {
-      val caption = visualizer.Caption(peer.get)
-      val bounds = g.getFontMetrics.getStringBounds(caption, g)
-      val s = shape(g, visualizer, peer)
-
-      val (border, background, foreground) = visualizer.Color(peer)
-      g.setStroke(stroke)
-      g.setColor(border)
-      g.draw(s)
-      g.setColor(background)
-      g.fill(s)
-      g.setColor(foreground)
-      g.drawString(caption,
-        (s.getCenterX + (- bounds.getWidth / 2)).toFloat,
-        (s.getCenterY + 5).toFloat)
-    }
-  }
-
-  object Dummy extends Node
-  {
-    private val stroke =
-      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-    private val shape = new Rectangle2D.Double(-5, -5, 10, 10)
-    private val identity = new AffineTransform()
-
-    def shape(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Shape = shape
-
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
-      paint_transformed(g, visualizer, peer, identity)
-
-    def paint_transformed(g: Graphics2D, visualizer: Visualizer,
-      peer: Option[String], at: AffineTransform)
-    {
-      val (border, background, foreground) = visualizer.Color(peer)
-      g.setStroke(stroke)
-      g.setColor(border)
-      g.draw(at.createTransformedShape(shape))
-    }
-  }
-
-  trait Edge
-  {
-    def paint(g: Graphics2D, visualizer: Visualizer,
-      peer: (String, String), head: Boolean, dummies: Boolean)
-  }
-
-  object Straight_Edge extends Edge
-  {
-    private val stroke =
-      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-
-    def paint(g: Graphics2D, visualizer: Visualizer,
-      peer: (String, String), head: Boolean, dummies: Boolean)
-    {
-      val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
-      val ds =
-      {
-        val min = fy min ty
-        val max = fy max ty
-        visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max })
-      }
-      val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
-
-      path.moveTo(fx, fy)
-      ds.foreach({case (x, y) => path.lineTo(x, y)})
-      path.lineTo(tx, ty)
-
-      if (dummies) {
-        ds.foreach({
-            case (x, y) => {
-              val at = AffineTransform.getTranslateInstance(x, y)
-              Dummy.paint_transformed(g, visualizer, None, at)
-            }
-          })
-      }
-
-      g.setStroke(stroke)
-      g.setColor(visualizer.Color(peer))
-      g.draw(path)
-
-      if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
-    }
-  }
-
-  object Cardinal_Spline_Edge extends Edge
-  {
-    private val stroke =
-      new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
-    private val slack = 0.1
-
-    def paint(g: Graphics2D, visualizer: Visualizer,
-      peer: (String, String), head: Boolean, dummies: Boolean)
-    {
-      val ((fx, fy), (tx, ty)) =
-        (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
-      val ds =
-      {
-        val min = fy min ty
-        val max = fy max ty
-        visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max})
-      }
-
-      if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies)
-      else {
-        val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
-        path.moveTo(fx, fy)
-
-        val coords = ((fx, fy) :: ds ::: List((tx, ty)))
-        val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
-
-        val (dx2, dy2) =
-          ((dx, dy) /: coords.sliding(3))({
-            case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => {
-              val (dx2, dy2) = (rx - lx, ry - ly)
-
-              path.curveTo(lx + slack * dx , ly + slack * dy,
-                           mx - slack * dx2, my - slack * dy2,
-                           mx              , my)
-              (dx2, dy2)
-            }
-          })
-
-        val (lx, ly) = ds.last
-        path.curveTo(lx + slack * dx2, ly + slack * dy2,
-                     tx - slack * dx2, ty - slack * dy2,
-                     tx              , ty)
-
-        if (dummies) {
-          ds.foreach({
-              case (x, y) => {
-                val at = AffineTransform.getTranslateInstance(x, y)
-                Dummy.paint_transformed(g, visualizer, None, at)
-              }
-            })
-        }
-
-        g.setStroke(stroke)
-        g.setColor(visualizer.Color(peer))
-        g.draw(path)
-
-        if (head) Arrow_Head.paint(g, path, visualizer.Drawer.shape(g, Some(peer._2)))
-      }
-    }
-  }
-
-  object Arrow_Head
-  {
-    type Point = (Double, Double)
-
-    private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] =
-    {
-      def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
-      {
-        val i = path.getPathIterator(null, 1.0)
-        val seg = Array[Double](0,0,0,0,0,0)
-        var p1 = (0.0, 0.0)
-        var p2 = (0.0, 0.0)
-        while (!i.isDone()) {
-          i.currentSegment(seg) match {
-            case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
-            case PathIterator.SEG_LINETO =>
-              p1 = p2
-              p2 = (seg(0), seg(1))
-
-              if(shape.contains(seg(0), seg(1)))
-                return Some((p1, p2))
-            case _ =>
-          }
-          i.next()
-        }
-        None
-      }
-
-      def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] =
-      {
-        val ((fx, fy), (tx, ty)) = line
-        if (shape.contains(fx, fy) == shape.contains(tx, ty))
-          None
-        else {
-          val (dx, dy) = (fx - tx, fy - ty)
-          if ((dx * dx + dy * dy) < 1.0) {
-            val at = AffineTransform.getTranslateInstance(fx, fy)
-            at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
-            Some(at)
-          }
-          else {
-            val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0)
-            if (shape.contains(fx, fy) == shape.contains(mx, my))
-              binary_search(((mx, my), (tx, ty)), shape)
-            else
-              binary_search(((fx, fy), (mx, my)), shape)
-          }
-        }
-      }
-
-      intersecting_line(path, shape) match {
-        case None => None
-        case Some(line) => binary_search(line, shape)
-      }
-    }
-
-    def paint(g: Graphics2D, path: GeneralPath, shape: Shape)
-    {
-      position(path, shape) match {
-        case None =>
-        case Some(at) =>
-          val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3)
-          arrow.moveTo(0, 0)
-          arrow.lineTo(-10, 4)
-          arrow.lineTo(-6, 0)
-          arrow.lineTo(-10, -4)
-          arrow.lineTo(0, 0)
-          arrow.transform(at)
-
-          g.fill(arrow)
-      }
-    }
-  }
-}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/src/visualizer.scala
--- a/src/Tools/Graphview/src/visualizer.scala	Thu Jan 01 11:08:47 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,215 +0,0 @@
-/*  Title:      Tools/Graphview/src/visualizer.scala
-    Author:     Markus Kaiser, TU Muenchen
-
-Graph visualization parameters and interface state.
-*/
-
-package isabelle.graphview
-
-
-import isabelle._
-
-import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D}
-import java.awt.image.BufferedImage
-import javax.swing.JComponent
-
-
-class Visualizer(val model: Model)
-{
-  visualizer =>
-
-
-  /* font rendering information */
-
-  val font_family: String = "IsabelleText"
-  val font_size: Int = 14
-  val font = new Font(font_family, Font.BOLD, font_size)
-
-  val rendering_hints =
-    new RenderingHints(
-      RenderingHints.KEY_ANTIALIASING,
-      RenderingHints.VALUE_ANTIALIAS_ON)
-
-  val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics
-  gfx.setFont(font)
-  gfx.setRenderingHints(rendering_hints)
-
-  val font_metrics: FontMetrics = gfx.getFontMetrics(font)
-
-  val tooltip_font_size: Int = 10
-
-
-  /* rendering parameters */
-
-  val gap_x = 20
-  val pad_x = 8
-  val pad_y = 5
-
-  var arrow_heads = false
-
-  object Colors
-  {
-    private val filter_colors = List(
-      new JColor(0xD9, 0xF2, 0xE2), // blue
-      new JColor(0xFF, 0xE7, 0xD8), // orange
-      new JColor(0xFF, 0xFF, 0xE5), // yellow
-      new JColor(0xDE, 0xCE, 0xFF), // lilac
-      new JColor(0xCC, 0xEB, 0xFF), // turquoise
-      new JColor(0xFF, 0xE5, 0xE5), // red
-      new JColor(0xE5, 0xE5, 0xD9)  // green
-    )
-
-    private var curr : Int = -1
-    def next(): JColor =
-    {
-      curr = (curr + 1) % filter_colors.length
-      filter_colors(curr)
-    }
-  }
-
-
-  object Coordinates
-  {
-    private var layout = Layout_Pendulum.empty_layout
-
-    def apply(k: String): (Double, Double) =
-      layout.nodes.get(k) match {
-        case Some(c) => c
-        case None => (0, 0)
-      }
-
-    def apply(e: (String, String)): List[(Double, Double)] =
-      layout.dummies.get(e) match {
-        case Some(ds) => ds
-        case None => Nil
-      }
-
-    def reposition(k: String, to: (Double, Double))
-    {
-      layout = layout.copy(nodes = layout.nodes + (k -> to))
-    }
-
-    def reposition(d: ((String, String), Int), to: (Double, Double))
-    {
-      val (e, index) = d
-      layout.dummies.get(e) match {
-        case None =>
-        case Some(ds) =>
-          layout = layout.copy(dummies =
-            layout.dummies + (e ->
-              (ds.zipWithIndex :\ List.empty[(Double, Double)]) {
-                case ((t, i), n) => if (index == i) to :: n else t :: n
-              }))
-      }
-    }
-
-    def translate(k: String, by: (Double, Double))
-    {
-      val ((x, y), (dx, dy)) = (Coordinates(k), by)
-      reposition(k, (x + dx, y + dy))
-    }
-
-    def translate(d: ((String, String), Int), by: (Double, Double))
-    {
-      val ((e, i),(dx, dy)) = (d, by)
-      val (x, y) = apply(e)(i)
-      reposition(d, (x + dx, y + dy))
-    }
-
-    def update_layout()
-    {
-      layout =
-        if (model.current.is_empty) Layout_Pendulum.empty_layout
-        else {
-          val max_width =
-            model.current.iterator.map({ case (_, (info, _)) =>
-              font_metrics.stringWidth(info.name).toDouble }).max
-          val box_distance = max_width + pad_x + gap_x
-          def box_height(n: Int): Double =
-            ((font_metrics.getAscent + font_metrics.getDescent + pad_y) * (5 max n)).toDouble
-          Layout_Pendulum(model.current, box_distance, box_height)
-        }
-    }
-
-    def bounds(): (Double, Double, Double, Double) =
-      model.visible_nodes_iterator.toList match {
-        case Nil => (0, 0, 0, 0)
-        case nodes =>
-          val X: (String => Double) = (n => apply(n)._1)
-          val Y: (String => Double) = (n => apply(n)._2)
-
-          (X(nodes.minBy(X)), Y(nodes.minBy(Y)),
-           X(nodes.maxBy(X)), Y(nodes.maxBy(Y)))
-      }
-  }
-
-  object Drawer
-  {
-    def apply(g: Graphics2D, n: Option[String])
-    {
-      n match {
-        case None =>
-        case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n)
-      }
-    }
-
-    def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean)
-    {
-      Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
-    }
-
-    def paint_all_visible(g: Graphics2D, dummies: Boolean)
-    {
-      g.setFont(font)
-
-      g.setRenderingHints(rendering_hints)
-
-      model.visible_edges_iterator.foreach(e => {
-          apply(g, e, arrow_heads, dummies)
-        })
-
-      model.visible_nodes_iterator.foreach(l => {
-          apply(g, Some(l))
-        })
-    }
-
-    def shape(g: Graphics2D, n: Option[String]): Shape =
-      n match {
-        case None => Shapes.Dummy.shape(g, visualizer, None)
-        case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n)
-      }
-  }
-
-  object Selection
-  {
-    private var selected: List[String] = Nil
-
-    def apply() = selected
-    def apply(s: String) = selected.contains(s)
-
-    def add(s: String) { selected = s :: selected }
-    def set(ss: List[String]) { selected = ss }
-    def clear() { selected = Nil }
-  }
-
-  object Color
-  {
-    def apply(l: Option[String]): (JColor, JColor, JColor) =
-      l match {
-        case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK)
-        case Some(c) => {
-            if (Selection(c))
-              (JColor.BLUE, JColor.GREEN, JColor.BLACK)
-            else
-              (JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK)
-        }
-      }
-
-    def apply(e: (String, String)): JColor = JColor.BLACK
-  }
-
-  object Caption
-  {
-    def apply(key: String) = model.complete.get_node(key).name
-  }
-}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/Graphview/visualizer.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/visualizer.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -0,0 +1,215 @@
+/*  Title:      Tools/Graphview/visualizer.scala
+    Author:     Markus Kaiser, TU Muenchen
+
+Graph visualization parameters and interface state.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D}
+import java.awt.image.BufferedImage
+import javax.swing.JComponent
+
+
+class Visualizer(val model: Model)
+{
+  visualizer =>
+
+
+  /* font rendering information */
+
+  val font_family: String = "IsabelleText"
+  val font_size: Int = 14
+  val font = new Font(font_family, Font.BOLD, font_size)
+
+  val rendering_hints =
+    new RenderingHints(
+      RenderingHints.KEY_ANTIALIASING,
+      RenderingHints.VALUE_ANTIALIAS_ON)
+
+  val gfx = new BufferedImage(1, 1, BufferedImage.TYPE_INT_ARGB).createGraphics
+  gfx.setFont(font)
+  gfx.setRenderingHints(rendering_hints)
+
+  val font_metrics: FontMetrics = gfx.getFontMetrics(font)
+
+  val tooltip_font_size: Int = 10
+
+
+  /* rendering parameters */
+
+  val gap_x = 20
+  val pad_x = 8
+  val pad_y = 5
+
+  var arrow_heads = false
+
+  object Colors
+  {
+    private val filter_colors = List(
+      new JColor(0xD9, 0xF2, 0xE2), // blue
+      new JColor(0xFF, 0xE7, 0xD8), // orange
+      new JColor(0xFF, 0xFF, 0xE5), // yellow
+      new JColor(0xDE, 0xCE, 0xFF), // lilac
+      new JColor(0xCC, 0xEB, 0xFF), // turquoise
+      new JColor(0xFF, 0xE5, 0xE5), // red
+      new JColor(0xE5, 0xE5, 0xD9)  // green
+    )
+
+    private var curr : Int = -1
+    def next(): JColor =
+    {
+      curr = (curr + 1) % filter_colors.length
+      filter_colors(curr)
+    }
+  }
+
+
+  object Coordinates
+  {
+    private var layout = Layout_Pendulum.empty_layout
+
+    def apply(k: String): (Double, Double) =
+      layout.nodes.get(k) match {
+        case Some(c) => c
+        case None => (0, 0)
+      }
+
+    def apply(e: (String, String)): List[(Double, Double)] =
+      layout.dummies.get(e) match {
+        case Some(ds) => ds
+        case None => Nil
+      }
+
+    def reposition(k: String, to: (Double, Double))
+    {
+      layout = layout.copy(nodes = layout.nodes + (k -> to))
+    }
+
+    def reposition(d: ((String, String), Int), to: (Double, Double))
+    {
+      val (e, index) = d
+      layout.dummies.get(e) match {
+        case None =>
+        case Some(ds) =>
+          layout = layout.copy(dummies =
+            layout.dummies + (e ->
+              (ds.zipWithIndex :\ List.empty[(Double, Double)]) {
+                case ((t, i), n) => if (index == i) to :: n else t :: n
+              }))
+      }
+    }
+
+    def translate(k: String, by: (Double, Double))
+    {
+      val ((x, y), (dx, dy)) = (Coordinates(k), by)
+      reposition(k, (x + dx, y + dy))
+    }
+
+    def translate(d: ((String, String), Int), by: (Double, Double))
+    {
+      val ((e, i),(dx, dy)) = (d, by)
+      val (x, y) = apply(e)(i)
+      reposition(d, (x + dx, y + dy))
+    }
+
+    def update_layout()
+    {
+      layout =
+        if (model.current.is_empty) Layout_Pendulum.empty_layout
+        else {
+          val max_width =
+            model.current.iterator.map({ case (_, (info, _)) =>
+              font_metrics.stringWidth(info.name).toDouble }).max
+          val box_distance = max_width + pad_x + gap_x
+          def box_height(n: Int): Double =
+            ((font_metrics.getAscent + font_metrics.getDescent + pad_y) * (5 max n)).toDouble
+          Layout_Pendulum(model.current, box_distance, box_height)
+        }
+    }
+
+    def bounds(): (Double, Double, Double, Double) =
+      model.visible_nodes_iterator.toList match {
+        case Nil => (0, 0, 0, 0)
+        case nodes =>
+          val X: (String => Double) = (n => apply(n)._1)
+          val Y: (String => Double) = (n => apply(n)._2)
+
+          (X(nodes.minBy(X)), Y(nodes.minBy(Y)),
+           X(nodes.maxBy(X)), Y(nodes.maxBy(Y)))
+      }
+  }
+
+  object Drawer
+  {
+    def apply(g: Graphics2D, n: Option[String])
+    {
+      n match {
+        case None =>
+        case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n)
+      }
+    }
+
+    def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean)
+    {
+      Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
+    }
+
+    def paint_all_visible(g: Graphics2D, dummies: Boolean)
+    {
+      g.setFont(font)
+
+      g.setRenderingHints(rendering_hints)
+
+      model.visible_edges_iterator.foreach(e => {
+          apply(g, e, arrow_heads, dummies)
+        })
+
+      model.visible_nodes_iterator.foreach(l => {
+          apply(g, Some(l))
+        })
+    }
+
+    def shape(g: Graphics2D, n: Option[String]): Shape =
+      n match {
+        case None => Shapes.Dummy.shape(g, visualizer, None)
+        case Some(_) => Shapes.Growing_Node.shape(g, visualizer, n)
+      }
+  }
+
+  object Selection
+  {
+    private var selected: List[String] = Nil
+
+    def apply() = selected
+    def apply(s: String) = selected.contains(s)
+
+    def add(s: String) { selected = s :: selected }
+    def set(ss: List[String]) { selected = ss }
+    def clear() { selected = Nil }
+  }
+
+  object Color
+  {
+    def apply(l: Option[String]): (JColor, JColor, JColor) =
+      l match {
+        case None => (JColor.GRAY, JColor.WHITE, JColor.BLACK)
+        case Some(c) => {
+            if (Selection(c))
+              (JColor.BLUE, JColor.GREEN, JColor.BLACK)
+            else
+              (JColor.BLACK, model.colors.getOrElse(c, JColor.WHITE), JColor.BLACK)
+        }
+      }
+
+    def apply(e: (String, String)): JColor = JColor.BLACK
+  }
+
+  object Caption
+  {
+    def apply(key: String) = model.complete.get_node(key).name
+  }
+}
\ No newline at end of file
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Tools/jEdit/etc/options	Thu Jan 01 11:12:15 2015 +0100
@@ -88,12 +88,14 @@
 option writeln_color : string = "C0C0C0FF"
 option information_color : string = "C1DFEEFF"
 option warning_color : string = "FF8C00FF"
+option legacy_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option writeln_message_color : string = "F0F0F0FF"
 option state_message_color : string = "F0E4E4FF"
 option information_message_color : string = "DCEAF3FF"
 option tracing_message_color : string = "F0F8FFFF"
 option warning_message_color : string = "EEE8AAFF"
+option legacy_message_color : string = "EEE8AAFF"
 option error_message_color : string = "FFC1C1FF"
 option spell_checker_color : string = "0000FFFF"
 option bad_color : string = "FF6A6A64"
diff -r 436b7b0c94f6 -r 839f4d1a7467 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Jan 01 11:08:47 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Jan 01 11:12:15 2015 +0100
@@ -46,6 +46,8 @@
     Markup.TRACING_MESSAGE -> tracing_pri,
     Markup.WARNING -> warning_pri,
     Markup.WARNING_MESSAGE -> warning_pri,
+    Markup.LEGACY -> legacy_pri,
+    Markup.LEGACY_MESSAGE -> legacy_pri,
     Markup.ERROR -> error_pri,
     Markup.ERROR_MESSAGE -> error_pri)
 
@@ -161,8 +163,8 @@
       Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
 
   private val tooltip_message_elements =
-    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING,
-      Markup.ERROR, Markup.BAD)
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
+      Markup.BAD)
 
   private val tooltip_descriptions =
     Map(
@@ -182,14 +184,15 @@
     Markup.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
-    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
 
   private val squiggly_elements =
-    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
+    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
 
   private val line_background_elements =
     Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
-      Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
+      Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE,
+      Markup.ERROR_MESSAGE)
 
   private val separator_elements =
     Markup.Elements(Markup.SEPARATOR)
@@ -198,8 +201,8 @@
     Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
-      Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
-      active_elements
+      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
+      Markup.BAD + Markup.INTENSIFY ++ active_elements
 
   private val foreground_elements =
     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
@@ -232,12 +235,14 @@
   val writeln_color = color_value("writeln_color")
   val information_color = color_value("information_color")
   val warning_color = color_value("warning_color")
+  val legacy_color = color_value("legacy_color")
   val error_color = color_value("error_color")
   val writeln_message_color = color_value("writeln_message_color")
   val state_message_color = color_value("state_message_color")
   val information_message_color = color_value("information_message_color")
   val tracing_message_color = color_value("tracing_message_color")
   val warning_message_color = color_value("warning_message_color")
+  val legacy_message_color = color_value("legacy_message_color")
   val error_message_color = color_value("error_message_color")
   val spell_checker_color = color_value("spell_checker_color")
   val bad_color = color_value("bad_color")
@@ -591,6 +596,7 @@
     Rendering.writeln_pri -> writeln_color,
     Rendering.information_pri -> information_color,
     Rendering.warning_pri -> warning_color,
+    Rendering.legacy_pri -> legacy_color,
     Rendering.error_pri -> error_color)
 
   def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
@@ -615,6 +621,7 @@
     Rendering.information_pri -> information_message_color,
     Rendering.tracing_pri -> tracing_message_color,
     Rendering.warning_pri -> warning_message_color,
+    Rendering.legacy_pri -> legacy_message_color,
     Rendering.error_pri -> error_message_color)
 
   def line_background(range: Text.Range): Option[(Color, Boolean)] =