author  wenzelm 
Tue, 24 Nov 2015 23:17:03 +0100  
changeset 61747  a870098fc27e 
parent 61723  7feee72b5897 
child 61904  30f70d1b97c9 
permissions  rwrr 
46572  1 
/* Title: Tools/jEdit/src/text_overview.scala 
2 
Author: Makarius 

3 

57613  4 
GUI component for text status overview. 
46572  5 
*/ 
6 

7 
package isabelle.jedit 

8 

9 

10 
import isabelle._ 

11 

12 
import scala.annotation.tailrec 

13 

49346  14 
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color} 
46572  15 
import java.awt.event.{MouseAdapter, MouseEvent} 
16 
import javax.swing.{JPanel, ToolTipManager} 

17 

18 

19 
class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout) 

20 
{ 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

21 
/* GUI components */ 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

22 

46572  23 
private val text_area = doc_view.text_area 
24 
private val buffer = doc_view.model.buffer 

25 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

26 
private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

27 

61747  28 
private val WIDTH = text_area.getPainter.getFontMetrics.stringWidth("A") max 10 
50895  29 
private val HEIGHT = 4 
46572  30 

31 
setPreferredSize(new Dimension(WIDTH, 0)) 

32 

33 
setRequestFocusEnabled(false) 

34 

35 
addMouseListener(new MouseAdapter { 

36 
override def mousePressed(event: MouseEvent) { 

37 
val line = (event.getY * lines()) / getHeight 

38 
if (line >= 0 && line < text_area.getLineCount) 

39 
text_area.setCaretPosition(text_area.getLineStartOffset(line)) 

40 
} 

41 
}) 

42 

43 
override def addNotify() { 

44 
super.addNotify() 

45 
ToolTipManager.sharedInstance.registerComponent(this) 

46 
} 

47 

48 
override def removeNotify() { 

49 
ToolTipManager.sharedInstance.unregisterComponent(this) 

50 
super.removeNotify 

51 
} 

52 

49346  53 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

54 
/* overview */ 
49346  55 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

56 
private case class Overview( 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

57 
line_count: Int = 0, 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

58 
char_count: Int = 0, 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

59 
L: Int = 0, 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

60 
H: Int = 0) 
49346  61 

61196  62 
private def get_overview(): Overview = 
61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

63 
Overview( 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

64 
line_count = buffer.getLineCount, 
61196  65 
char_count = buffer.getLength, 
61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

66 
L = lines(), 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

67 
H = getHeight()) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

68 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

69 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

70 
/* synchronous painting */ 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

71 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

72 
private var current_overview = Overview() 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

73 
private var current_colors: List[(Color, Int, Int)] = Nil 
49346  74 

46572  75 
override def paintComponent(gfx: Graphics) 
76 
{ 

77 
super.paintComponent(gfx) 

57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56662
diff
changeset

78 
GUI_Thread.assert {} 
46572  79 

49411  80 
doc_view.rich_text_area.robust_body(()) { 
49406  81 
JEdit_Lib.buffer_lock(buffer) { 
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset

82 
val rendering = doc_view.get_rendering() 
61196  83 
val overview = get_overview() 
46572  84 

61197
b9d69001824e
straightforward refresh, without special preconditions;
wenzelm
parents:
61196
diff
changeset

85 
if (!rendering.snapshot.is_outdated && overview == current_overview) { 
49346  86 
gfx.setColor(getBackground) 
87 
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

88 
for ((color, h, h1) < current_colors) { 
49346  89 
gfx.setColor(color) 
90 
gfx.fillRect(0, h, getWidth, h1  h) 

46572  91 
} 
92 
} 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

93 
else { 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

94 
gfx.setColor(rendering.outdated_color) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

95 
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

96 
} 
46572  97 
} 
98 
} 

99 
} 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

100 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

101 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

102 
/* asynchronous refresh */ 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

103 

61561  104 
private var future_refresh: Option[Future[Unit]] = None 
105 
private def cancel(): Unit = future_refresh.map(_.cancel) 

61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

106 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

107 
def invoke(): Unit = delay_refresh.invoke() 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

108 
def revoke(): Unit = delay_refresh.revoke() 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

109 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

110 
private val delay_refresh = 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

111 
GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"), cancel _) { 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

112 
doc_view.rich_text_area.robust_body(()) { 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

113 
JEdit_Lib.buffer_lock(buffer) { 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

114 
val rendering = doc_view.get_rendering() 
61196  115 
val overview = get_overview() 
61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

116 

61197
b9d69001824e
straightforward refresh, without special preconditions;
wenzelm
parents:
61196
diff
changeset

117 
if (!rendering.snapshot.is_outdated) { 
61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

118 
cancel() 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

119 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

120 
val line_offsets = 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

121 
{ 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

122 
val line_manager = JEdit_Lib.buffer_line_manager(buffer) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

123 
val a = new Array[Int](line_manager.getLineCount) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

124 
for (i < 1 until a.length) a(i) = line_manager.getLineEndOffset(i  1) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

125 
a 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

126 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

127 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

128 
future_refresh = 
61561  129 
Some(Future.fork { 
61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

130 
val line_count = overview.line_count 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

131 
val char_count = overview.char_count 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

132 
val L = overview.L 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

133 
val H = overview.H 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

134 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

135 
@tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)]) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

136 
: List[(Color, Int, Int)] = 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

137 
{ 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

138 
Exn.Interrupt.expose() 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

139 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

140 
if (l < line_count && h < H) { 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

141 
val p1 = p + H 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

142 
val q1 = q + HEIGHT * L 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

143 
val (l1, h1) = 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

144 
if (p1 >= q1) (l + 1, h + (p1  q) / L) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

145 
else (l + (q1  p) / H, h + HEIGHT) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

146 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

147 
val start = line_offsets(l) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

148 
val end = 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

149 
if (l1 < line_count) line_offsets(l1) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

150 
else char_count 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

151 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

152 
val colors1 = 
61196  153 
(rendering.overview_color(Text.Range(start, end)), colors) match { 
61195
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

154 
case (Some(color), (old_color, old_h, old_h1) :: rest) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

155 
if color == old_color && old_h1 == h => (color, old_h, h1) :: rest 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

156 
case (Some(color), _) => (color, h, h1) :: colors 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

157 
case (None, _) => colors 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

158 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

159 
loop(l1, h1, p + (l1  l) * H, q + (h1  h) * L, colors1) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

160 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

161 
else colors.reverse 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

162 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

163 
val new_colors = loop(0, 0, 0, 0, Nil) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

164 

42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

165 
GUI_Thread.later { 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

166 
current_overview = overview 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

167 
current_colors = new_colors 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

168 
repaint() 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

169 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

170 
}) 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

171 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

172 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

173 
} 
42419fe6f660
fast synchronous painting and asynchronous refresh of text overview, reduces GUI thread latency from 100ms to 1ms for big files like src/HOL/Multivariate_Analsyis/Integration.thy;
wenzelm
parents:
57613
diff
changeset

174 
} 
46572  175 
} 