isabelle: src/Tools/Graphview/etc/options@6e042537555d (annotated)

59286 ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	1	(* :mode=isabelle-options: *)
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	2
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	3	section "Graphview"
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	4
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	5	option graphview_font_family : string = "Helvetica"
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	6	-- "base font family (notably for PDF)"
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	7
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	8	option graphview_font_size : int = 12
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	9	-- "base font size (notably for PDF)"
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	10
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	11	public option graphview_font_scale : real = 0.85
ac74eedb910a GUI.imitate_font: more explicit result size, e.g. relevant for caching; wenzelm parents: diff changeset	12	-- "scale factor of graph view wrt. main text font"
59313 d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	13
59419 2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout; wenzelm parents: 59412 diff changeset	14	public option graphview_iterations_minimize_crossings : int = 20
59313 d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	15	-- "number of iterations to minimize edge crossings"
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	16
59419 2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout; wenzelm parents: 59412 diff changeset	17	public option graphview_iterations_pendulum : int = 5
59313 d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	18	-- "number of iterations for pendulum method"
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	19
59419 2fb2194853cc clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout; wenzelm parents: 59412 diff changeset	20	public option graphview_iterations_rubberband : int = 5
59313 d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	21	-- "number of iterations for rubberband method"
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	22
59384 c75327a34960 more explicit Layout.Info: size and content; wenzelm parents: 59313 diff changeset	23	public option graphview_content_margin : int = 60
c75327a34960 more explicit Layout.Info: size and content; wenzelm parents: 59313 diff changeset	24	-- "margin for node content pretty-printing"
c75327a34960 more explicit Layout.Info: size and content; wenzelm parents: 59313 diff changeset	25

author	wenzelm
	Thu, 09 Mar 2017 15:19:24 +0100
changeset 65160	6e042537555d
parent 59419	2fb2194853cc
child 69369	6ecc85955e04
permissions	-rw-r--r--