| #
c3febf30 |
|
02-Apr-2016 |
wenzelm <none@none> |
more robust display of bidirectional Unicode text: enforce left-to-right;
|
| #
25b91132 |
|
28-Jan-2015 |
wenzelm <none@none> |
clarified module name;
--HG--
rename : src/Tools/Graphview/visualizer.scala => src/Tools/Graphview/graphview.scala
|
| #
d8f3ad9d |
|
19-Jan-2015 |
wenzelm <none@none> |
tuned colors;
|
| #
f0f70d79 |
|
19-Jan-2015 |
wenzelm <none@none> |
clarified edge_color;
|
| #
3681e0bf |
|
17-Jan-2015 |
wenzelm <none@none> |
more explicit Layout.Info: size and content;
allow multi-line vertex label, based on content;
misc tuning;
|
| #
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;
|
| #
01c29dd2 |
|
05-Jan-2015 |
wenzelm <none@none> |
tuned metrics;
|
| #
76dba21f |
|
05-Jan-2015 |
wenzelm <none@none> |
proper bounding box including dummies;
|
| #
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;
|
| #
a947cf97 |
|
04-Jan-2015 |
wenzelm <none@none> |
explicit Layout.Point;
tuned signature;
tuned;
|
| #
26fabcb5 |
|
04-Jan-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
a972f9c2 |
|
03-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
3ca4d5de |
|
03-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
e0787b82 |
|
03-Jan-2015 |
wenzelm <none@none> |
tuned;
|
| #
ca7d3a1b |
|
03-Jan-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
331be8f5 |
|
03-Jan-2015 |
wenzelm <none@none> |
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
misc tuning;
tuned signature;
|
| #
73433f4a |
|
03-Jan-2015 |
wenzelm <none@none> |
prefer integer coordinates;
tuned painting;
|
| #
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;
|
| #
2ed0c628 |
|
02-Jan-2015 |
wenzelm <none@none> |
clarified metrics, similar to old graph browser;
|
| #
0e616366 |
|
01-Jan-2015 |
wenzelm <none@none> |
more dynamic visualizer -- re-use jEdit font info;
|
| #
e07ca76d |
|
31-Dec-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
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
|
| #
e0e8cf48 |
|
02-May-2015 |
wenzelm <none@none> |
misc tuning, based on warnings by IntelliJ IDEA;
|