33 } |
33 } |
34 |
34 |
35 def chooseColor(status : String) : Color = { |
35 def chooseColor(status : String) : Color = { |
36 //TODO: as properties! |
36 //TODO: as properties! |
37 status match { |
37 status match { |
38 case "ident" => new Color(192, 192, 255) |
38 //outer |
39 case "literal" => new Color(192, 255, 255) |
39 case "ident" | "command" | "keyword" => Color.blue |
40 case "fixed_decl" => new Color(192, 192, 192) |
40 case "verbatim"=> Color.green |
41 case "prop" => new Color(255, 192 ,255) |
41 case "comment" => Color.gray |
42 case "typ" => new Color(192, 192, 128) |
42 case "control" => Color.white |
43 case "term" => new Color(192, 128, 192) |
43 case "malformed" => Color.red |
44 case "method" => new Color(128, 192, 192) |
44 case "string" | "altstring" => Color.orange |
45 case "doc_source" => new Color(128, 128, 192) |
45 //logical |
46 case "ML_source" => new Color(128, 192, 128) |
46 case "tclass" | "tycon" | "fixed_decl" | "fixed" |
47 case "local_fact_decl" => new Color(192, 128, 128) |
47 | "const_decl" | "const" | "fact_decl" | "fact" |
48 case _ => Color.red |
48 |"dynamic_fact" |"local_fact_decl" | "local_fact" |
|
49 => new Color(255, 0, 255) |
|
50 //inner syntax |
|
51 case "tfree" | "free" => Color.blue |
|
52 case "tvar" | "skolem" | "bound" | "var" => Color.green |
|
53 case "num" | "xnum" | "xstr" | "literal" | "inner_comment" => new Color(255, 128, 128) |
|
54 case "sort" | "typ" | "term" | "prop" | "attribute" | "method" => Color.yellow |
|
55 // embedded source |
|
56 case "doc_source" | "ML_source" | "ML_antic" | "doc_antiq" | "antiq" |
|
57 => new Color(0, 192, 0) |
|
58 case _ => Color.white |
49 } |
59 } |
50 } |
60 } |
51 def withView(view : TextArea, f : (TheoryView) => Unit) { |
61 def withView(view : TextArea, f : (TheoryView) => Unit) { |
52 if (view != null && view.getBuffer() != null) |
62 if (view != null && view.getBuffer() != null) |
53 view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match { |
63 view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match { |
162 if (textArea != null) |
172 if (textArea != null) |
163 textArea.invalidateLineRange(textArea.getFirstPhysicalLine, |
173 textArea.invalidateLineRange(textArea.getFirstPhysicalLine, |
164 textArea.getLastPhysicalLine) |
174 textArea.getLastPhysicalLine) |
165 } |
175 } |
166 |
176 |
167 def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color){ |
177 def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color, fill : Boolean){ |
168 val fm = textArea.getPainter.getFontMetrics |
178 val fm = textArea.getPainter.getFontMetrics |
169 val startP = textArea.offsetToXY(begin) |
179 val startP = textArea.offsetToXY(begin) |
170 val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish) |
180 val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish) |
171 else { var p = textArea.offsetToXY(finish - 1) |
181 else { var p = textArea.offsetToXY(finish - 1) |
172 p.x = p.x + fm.charWidth(' ') |
182 p.x = p.x + fm.charWidth(' ') |
173 p } |
183 p } |
174 |
184 |
175 if (startP != null && stopP != null) { |
185 if (startP != null && stopP != null) { |
176 gfx.setColor(color) |
186 gfx.setColor(color) |
177 gfx.fillRect(startP.x, y, stopP.x - startP.x, height) |
187 if(fill){gfx.fillRect(startP.x, y, stopP.x - startP.x, height)} |
|
188 else {gfx.drawRect(startP.x, y, stopP.x - startP.x, height)} |
178 } |
189 } |
179 } |
190 } |
180 |
191 |
181 override def paintValidLine(gfx : Graphics2D, screenLine : Int, |
192 override def paintValidLine(gfx : Graphics2D, screenLine : Int, |
182 pl : Int, start : Int, end : Int, y : Int) |
193 pl : Int, start : Int, end : Int, y : Int) |
187 |
198 |
188 //Encolor Phase |
199 //Encolor Phase |
189 while (e != null && toCurrent(e.start) < end) { |
200 while (e != null && toCurrent(e.start) < end) { |
190 val begin = start max toCurrent(e.start) |
201 val begin = start max toCurrent(e.start) |
191 val finish = end - 1 min toCurrent(e.stop) |
202 val finish = end - 1 min toCurrent(e.stop) |
192 encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e)) |
203 encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e), true) |
193 // paint details of command |
204 // paint details of command |
194 var dy = 0 |
205 var nodes = e.root_node.breadthFirstEnumeration |
195 for(status <- e.statuses){ |
206 while(nodes.hasMoreElements){ |
196 dy += 1 |
207 val node = nodes.nextElement.asInstanceOf[javax.swing.tree.DefaultMutableTreeNode] |
197 val begin = toCurrent(status.start + e.start) |
208 val node_asset = node.getUserObject.asInstanceOf[isabelle.prover.RelativeAsset] |
198 val finish = toCurrent(status.stop + e.start) |
209 val begin = toCurrent(node_asset.rel_start + e.start) |
|
210 val finish = toCurrent(node_asset.rel_end + e.start) |
199 if(finish > start && begin < end) |
211 if(finish > start && begin < end) |
200 encolor(gfx, y + dy, fm.getHeight - dy, begin max start, finish min end, chooseColor(status.kind)) |
212 encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node_asset.getShortDescription), true) |
201 } |
213 } |
202 e = e.next |
214 e = e.next |
203 } |
215 } |
204 |
216 |
205 gfx.setColor(savedColor) |
217 gfx.setColor(savedColor) |