src/Tools/Graphview/graph_panel.scala
24 months ago wenzelm 2017-06-27 clarified defaults;
24 months ago wenzelm 2017-06-27 tuned signature;
2015-09-14 wenzelm 2015-09-14 avoid hardwired colors; more explicit switch of editor style vs. default style, which is more appropriate for printing (via PDF);
2015-01-28 wenzelm 2015-01-28 tuned comment;
2015-01-28 wenzelm 2015-01-28 tuned signature;
2015-01-28 wenzelm 2015-01-28 clarified module name;
2015-01-25 wenzelm 2015-01-25 support for off-line graph output, without GUI thread;
2015-01-25 wenzelm 2015-01-25 separate module Graph_File;
2015-01-19 wenzelm 2015-01-19 suppress inactive controls (again);
2015-01-19 wenzelm 2015-01-19 tuned;
2015-01-19 wenzelm 2015-01-19 more symmetric layout of main panel; misc tuning;
2015-01-18 wenzelm 2015-01-18 suppress some controls that don't work yet;
2015-01-18 wenzelm 2015-01-18 tuned;
2015-01-18 wenzelm 2015-01-18 misc tuning;
2015-01-18 wenzelm 2015-01-18 proper scrolling wrt. transform; tuned signature;
2015-01-18 wenzelm 2015-01-18 support for tree view on graph nodes; misc tuning;
2015-01-17 wenzelm 2015-01-17 proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;
2015-01-06 wenzelm 2015-01-06 tuned signature;
2015-01-06 wenzelm 2015-01-06 tuned signature;
2015-01-06 wenzelm 2015-01-06 explict layout graph structure, with dummies and coordinates; explicit metrics for dummy box; tuned signature; misc tuning;
2015-01-05 wenzelm 2015-01-05 clarified visualizer parameters; do not show dummies by default;
2015-01-05 wenzelm 2015-01-05 more direct coordinates for dummy;
2015-01-05 wenzelm 2015-01-05 separate module Metrics; maintain static metrics (with font) and visible_graph via layout;
2015-01-05 wenzelm 2015-01-05 avoid fractional font size;
2015-01-05 wenzelm 2015-01-05 GUI.imitate_font: more explicit result size, e.g. relevant for caching; some graphview font options: Helvetica family is important for self-contained PDF; tuned;
2015-01-04 wenzelm 2015-01-04 explicit Layout.Point; tuned signature; tuned;
2015-01-04 wenzelm 2015-01-04 clarified static full_graph vs. dynamic visible_graph; tuned;
2015-01-03 wenzelm 2015-01-03 clarified fit_to_window: floor scale within window bounds;
2015-01-03 wenzelm 2015-01-03 apply_layout: proper repaint; discontinued dysfunctional keyboard interaction: avoid delicate questions about focus and "standard" key bindings in Isabelle/jEdit;
2015-01-03 wenzelm 2015-01-03 tuned;
2015-01-03 wenzelm 2015-01-03 more formal Graph_Display.Node (with ordering) and Graph_Display.Edge; misc tuning; tuned signature;
2015-01-03 wenzelm 2015-01-03 recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;
2015-01-03 wenzelm 2015-01-03 clarified bounding box, similar to old graph browser; default font like old browser; clarified metrics; tuned signature;
2015-01-02 wenzelm 2015-01-02 tuned headers;
2015-01-02 wenzelm 2015-01-02 less excessive event handling;
2015-01-02 wenzelm 2015-01-02 tuned;
2015-01-02 wenzelm 2015-01-02 clarified mouse wheel: conventional scrolling, not scaling;
2015-01-01 wenzelm 2015-01-01 tuned color;
2015-01-01 wenzelm 2015-01-01 tuned signature;
2015-01-01 wenzelm 2015-01-01 more dynamic visualizer -- re-use jEdit font info;
2015-01-01 wenzelm 2015-01-01 more dynamic visualizer -- re-use Isabelle/jEdit options; clarified iTextField error: like Isabelle/jEdit search field; tuned signature;
2015-01-01 wenzelm 2015-01-01 tuned;
2015-01-01 wenzelm 2015-01-01 tuned imports;
2015-01-01 wenzelm 2015-01-01 tuned;
2015-01-01 wenzelm 2015-01-01 tuned whitespace;
2014-12-30 wenzelm 2014-12-30 clarified source location;