--- a/src/Tools/Graphview/main_panel.scala Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Sun Jan 18 19:21:10 2015 +0100
@@ -34,7 +34,7 @@
}
val split_pane =
- if (visualizer.get_options.bool("graphview_swap_panels"))
+ if (visualizer.options.bool("graphview_swap_panels"))
new SplitPane(Orientation.Vertical, tree_panel, graph_panel)
else
new SplitPane(Orientation.Vertical, graph_panel, tree_panel)
--- a/src/Tools/Graphview/tree_panel.scala Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Sun Jan 18 19:21:10 2015 +0100
@@ -84,7 +84,7 @@
private val selection_field_foreground = selection_field.foreground
private val selection_delay =
- GUI_Thread.delay_last(visualizer.get_options.seconds("editor_input_delay")) {
+ GUI_Thread.delay_last(visualizer.options.seconds("editor_input_delay")) {
val (pattern, ok) =
selection_field.text match {
case null | "" => (None, true)
--- a/src/Tools/Graphview/visualizer.scala Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala Sun Jan 18 19:21:10 2015 +0100
@@ -2,7 +2,7 @@
Author: Markus Kaiser, TU Muenchen
Author: Makarius
-Graph visualization parameters and interface state.
+Graph visualization parameters and GUI state.
*/
package isabelle.graphview
@@ -15,12 +15,12 @@
import javax.swing.JComponent
-class Visualizer(options: => Options, val model: Model)
+abstract class Visualizer(val model: Model)
{
visualizer =>
- def get_options: Options = options
+ def options: Options
/* layout state */
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sun Jan 18 19:09:41 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sun Jan 18 19:21:10 2015 +0100
@@ -62,26 +62,29 @@
graph_result match {
case Exn.Res(graph) =>
val model = new isabelle.graphview.Model(graph)
- val visualizer = new isabelle.graphview.Visualizer(PIDE.options.value, model) {
+ val visualizer = new isabelle.graphview.Visualizer(model) {
+ def options: Options = PIDE.options.value
+
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
Pretty_Tooltip.invoke(() =>
{
- val rendering = Rendering(snapshot, PIDE.options.value)
+ val rendering = Rendering(snapshot, options)
val info = Text.Info(Text.Range(~1), body)
Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
})
null
}
+
+ override def make_font(): Font =
+ GUI.imitate_font(Font_Info.main().font,
+ options.string("graphview_font_family"),
+ options.real("graphview_font_scale"))
+
override def foreground_color = view.getTextArea.getPainter.getForeground
override def selection_color = view.getTextArea.getPainter.getSelectionColor
override def current_color = view.getTextArea.getPainter.getLineHighlightColor
override def error_color = PIDE.options.color_value("error_color")
-
- override def make_font(): Font =
- GUI.imitate_font(Font_Info.main().font,
- PIDE.options.string("graphview_font_family"),
- PIDE.options.real("graphview_font_scale"))
}
new isabelle.graphview.Main_Panel(model, visualizer)
case Exn.Exn(exn) => new TextArea(Exn.message(exn))