isabelle: src/Tools/Graphview/etc/options@0426b53a5d54 (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
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	14	public option graphview_iterations_minimize_crossings : int = 40
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
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	17	public option graphview_iterations_pendulum : int = 10
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	18	-- "number of iterations for pendulum method"
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	19
d7f4f46e9a59 configurable options; wenzelm parents: 59286 diff changeset	20	public option graphview_iterations_rubberband : int = 10
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
	Mon, 19 Jan 2015 21:15:30 +0100
changeset 59412	0426b53a5d54
parent 59393	9f518fa77c1c
child 59419	2fb2194853cc
permissions	-rw-r--r--