| #
3891c3e0 |
|
27-Jun-2017 |
wenzelm <none@none> |
clarified defaults;
|
| #
3d4309c0 |
|
27-Jun-2017 |
wenzelm <none@none> |
tuned signature;
|
| #
5b7b1f2f |
|
14-Sep-2015 |
wenzelm <none@none> |
avoid hardwired colors;
more explicit switch of editor style vs. default style, which is more appropriate for printing (via PDF);
|
| #
605bf1dd |
|
28-Jan-2015 |
wenzelm <none@none> |
tuned comment;
|
| #
0b760ac9 |
|
28-Jan-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
25b91132 |
|
28-Jan-2015 |
wenzelm <none@none> |
clarified module name;
--HG--
rename : src/Tools/Graphview/visualizer.scala => src/Tools/Graphview/graphview.scala
|
| #
e2e241ba |
|
25-Jan-2015 |
wenzelm <none@none> |
support for off-line graph output, without GUI thread;
|
| #
5db2daa7 |
|
25-Jan-2015 |
wenzelm <none@none> |
separate module Graph_File;
|
| #
d95dde8d |
|
19-Jan-2015 |
wenzelm <none@none> |
suppress inactive controls (again);
|
| #
6d760ae0 |
|
19-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
62632c06 |
|
19-Jan-2015 |
wenzelm <none@none> |
more symmetric layout of main panel;
misc tuning;
|
| #
730988c8 |
|
18-Jan-2015 |
wenzelm <none@none> |
suppress some controls that don't work yet;
|
| #
9640a669 |
|
18-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
0515044c |
|
18-Jan-2015 |
wenzelm <none@none> |
misc tuning;
|
| #
e31c6e88 |
|
18-Jan-2015 |
wenzelm <none@none> |
proper scrolling wrt. transform;
tuned signature;
|
| #
f653497f |
|
18-Jan-2015 |
wenzelm <none@none> |
support for tree view on graph nodes;
misc tuning;
|
| #
bbd13c69 |
|
17-Jan-2015 |
wenzelm <none@none> |
proper refresh after apply_layout, in order to update preferred size, which is required for scroll pane;
|
| #
9a83d20b |
|
06-Jan-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
420fa195 |
|
06-Jan-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
71ea3d5c |
|
06-Jan-2015 |
wenzelm <none@none> |
explict layout graph structure, with dummies and coordinates;
explicit metrics for dummy box;
tuned signature;
misc tuning;
|
| #
85d69581 |
|
05-Jan-2015 |
wenzelm <none@none> |
clarified visualizer parameters;
do not show dummies by default;
|
| #
ca94b554 |
|
05-Jan-2015 |
wenzelm <none@none> |
more direct coordinates for dummy;
|
| #
e1df35e0 |
|
05-Jan-2015 |
wenzelm <none@none> |
separate module Metrics;
maintain static metrics (with font) and visible_graph via layout;
|
| #
f11f6693 |
|
05-Jan-2015 |
wenzelm <none@none> |
avoid fractional font size;
|
| #
37b03ce6 |
|
05-Jan-2015 |
wenzelm <none@none> |
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;
|
| #
a947cf97 |
|
04-Jan-2015 |
wenzelm <none@none> |
explicit Layout.Point;
tuned signature;
tuned;
|
| #
a838e0a4 |
|
04-Jan-2015 |
wenzelm <none@none> |
clarified static full_graph vs. dynamic visible_graph;
tuned;
|
| #
4129f46a |
|
03-Jan-2015 |
wenzelm <none@none> |
clarified fit_to_window: floor scale within window bounds;
|
| #
237642da |
|
03-Jan-2015 |
wenzelm <none@none> |
apply_layout: proper repaint;
discontinued dysfunctional keyboard interaction: avoid delicate questions about focus and "standard" key bindings in Isabelle/jEdit;
|
| #
3ca4d5de |
|
03-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
331be8f5 |
|
03-Jan-2015 |
wenzelm <none@none> |
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
misc tuning;
tuned signature;
|
| #
f7a1e8a6 |
|
03-Jan-2015 |
wenzelm <none@none> |
recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;
|
| #
46126c11 |
|
03-Jan-2015 |
wenzelm <none@none> |
clarified bounding box, similar to old graph browser;
default font like old browser;
clarified metrics;
tuned signature;
|
| #
a9c5fc80 |
|
02-Jan-2015 |
wenzelm <none@none> |
tuned headers;
|
| #
671c4159 |
|
02-Jan-2015 |
wenzelm <none@none> |
less excessive event handling;
|
| #
2a8ab89a |
|
02-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
d01e0134 |
|
02-Jan-2015 |
wenzelm <none@none> |
clarified mouse wheel: conventional scrolling, not scaling;
|
| #
631bf49d |
|
01-Jan-2015 |
wenzelm <none@none> |
tuned color;
|
| #
219f8a6b |
|
01-Jan-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
0e616366 |
|
01-Jan-2015 |
wenzelm <none@none> |
more dynamic visualizer -- re-use jEdit font info;
|
| #
282ee19a |
|
01-Jan-2015 |
wenzelm <none@none> |
more dynamic visualizer -- re-use Isabelle/jEdit options;
clarified iTextField error: like Isabelle/jEdit search field;
tuned signature;
|
| #
9a951ccc |
|
01-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
af879b32 |
|
01-Jan-2015 |
wenzelm <none@none> |
tuned imports;
|
| #
b93ca508 |
|
31-Dec-2014 |
wenzelm <none@none> |
tuned;
|
| #
0d3566c6 |
|
01-Jan-2015 |
wenzelm <none@none> |
tuned whitespace;
|
| #
bbe9df58 |
|
30-Dec-2014 |
wenzelm <none@none> |
clarified source location;
--HG--
rename : src/Tools/Graphview/src/graph_panel.scala => src/Tools/Graphview/graph_panel.scala
rename : src/Tools/Graphview/src/layout_pendulum.scala => src/Tools/Graphview/layout_pendulum.scala
rename : src/Tools/Graphview/src/main_panel.scala => src/Tools/Graphview/main_panel.scala
rename : src/Tools/Graphview/src/model.scala => src/Tools/Graphview/model.scala
rename : src/Tools/Graphview/src/mutator.scala => src/Tools/Graphview/mutator.scala
rename : src/Tools/Graphview/src/mutator_dialog.scala => src/Tools/Graphview/mutator_dialog.scala
rename : src/Tools/Graphview/src/mutator_event.scala => src/Tools/Graphview/mutator_event.scala
rename : src/Tools/Graphview/src/popups.scala => src/Tools/Graphview/popups.scala
rename : src/Tools/Graphview/src/shapes.scala => src/Tools/Graphview/shapes.scala
rename : src/Tools/Graphview/src/visualizer.scala => src/Tools/Graphview/visualizer.scala
|