--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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:
--- 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)
--- 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)
--- 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
--- 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)
--- 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"
--- 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)
--- 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 () =>
--- 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
--- 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 *)
--- 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 *)
--- 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);
--- 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 =
--- 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 =
--- 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
--- 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)
})
}
--- 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;
-
--- 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];
--- 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
--- 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. *)
--- 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;
--- 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 =
--- 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;
--- 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";
--- 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"
--- 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))
--- 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";
--- 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;
--- 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 =>
--- 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
--- 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;
--- 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"
--- 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"
)
--- 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;
--- /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)
+ )
+ }
+ }
+ }
+}
--- /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))
+ }
+ }
+}
--- /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))
+ }
+ }
+}
--- /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() }
+}
--- /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
--- /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
--- /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
--- /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
+ }
+}
--- /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
--- 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)
- )
- }
- }
- }
-}
--- 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))
- }
- }
-}
--- 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))
- }
- }
-}
--- 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() }
-}
--- 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
--- 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
--- 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
--- 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
- }
-}
--- 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
--- 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
--- /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
--- 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"
--- 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)] =