equal
deleted
inserted
replaced
9 package isabelle.jedit |
9 package isabelle.jedit |
10 |
10 |
11 |
11 |
12 import isabelle.proofdocument.Text |
12 import isabelle.proofdocument.Text |
13 import isabelle.prover.{Prover, Command} |
13 import isabelle.prover.{Prover, Command} |
14 import isabelle.prover.Command.Phase |
|
15 |
14 |
16 import java.awt.Graphics2D |
15 import java.awt.Graphics2D |
17 import java.awt.event.{ActionEvent, ActionListener} |
16 import java.awt.event.{ActionEvent, ActionListener} |
18 import java.awt.Color |
17 import java.awt.Color |
19 import javax.swing.Timer |
18 import javax.swing.Timer |
27 object TheoryView { |
26 object TheoryView { |
28 |
27 |
29 def choose_color(state: Command): Color = { |
28 def choose_color(state: Command): Color = { |
30 if (state == null) Color.red |
29 if (state == null) Color.red |
31 else |
30 else |
32 state.phase match { |
31 state.status match { |
33 case Phase.UNPROCESSED => new Color(255, 228, 225) |
32 case Command.Status.UNPROCESSED => new Color(255, 228, 225) |
34 case Phase.FINISHED => new Color(234, 248, 255) |
33 case Command.Status.FINISHED => new Color(234, 248, 255) |
35 case Phase.FAILED => new Color(255, 192, 192) |
34 case Command.Status.FAILED => new Color(255, 192, 192) |
36 case _ => Color.red |
35 case _ => Color.red |
37 } |
36 } |
38 } |
37 } |
39 |
38 |
40 def choose_color(markup: String): Color = { |
39 def choose_color(markup: String): Color = { |
146 else pos + col.added - col.removed |
145 else pos + col.added - col.removed |
147 else pos |
146 else pos |
148 |
147 |
149 def repaint(cmd: Command) = |
148 def repaint(cmd: Command) = |
150 { |
149 { |
151 val phase = cmd.phase |
150 val status = cmd.status |
152 if (text_area != null && phase != Phase.REMOVE && phase != Phase.REMOVED) { |
151 if (text_area != null && status != Command.Status.REMOVE && status != Command.Status.REMOVED) { |
153 val start = text_area.getLineOfOffset(to_current(cmd.start)) |
152 val start = text_area.getLineOfOffset(to_current(cmd.start)) |
154 val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1) |
153 val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1) |
155 text_area.invalidateLineRange(start, stop) |
154 text_area.invalidateLineRange(start, stop) |
156 |
155 |
157 if (Isabelle.prover_setup(buffer).selected_state == cmd) |
156 if (Isabelle.prover_setup(buffer).selected_state == cmd) |