author | wenzelm |
Sun, 21 Dec 2008 21:43:41 +0100 | |
changeset 34434 | ba08fc74f98a |
parent 34408 | ad7b6c4813c8 |
child 34440 | 561a6d19bd95 |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
34408 | 2 |
* jEdit text area as document text source |
34407 | 3 |
* |
4 |
* @author Fabian Immler, TU Munich |
|
5 |
* @author Johannes Hölzl, TU Munich |
|
6 |
*/ |
|
7 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle.utils.EventSource |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
12 |
import isabelle.proofdocument.Text |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
import isabelle.prover.{ Prover, Command, CommandChangeInfo } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
import isabelle.prover.Command.Phase |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
16 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
import javax.swing.Timer |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
18 |
import javax.swing.event.{ CaretListener, CaretEvent } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
import java.awt.Graphics2D |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
import java.awt.event.{ ActionEvent, ActionListener } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
21 |
import java.awt.Color; |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
22 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
import org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer } |
34402
bd8d70cd9baf
information on command-phase left of scrollbar
immler@in.tum.de
parents:
34401
diff
changeset
|
24 |
import org.gjt.sp.jedit.textarea.{ JEditTextArea, TextAreaExtension, TextAreaPainter } |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
25 |
import org.gjt.sp.jedit.syntax.SyntaxStyle |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
26 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
27 |
object TheoryView { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
28 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
29 |
def chooseColor(state : Command) : Color = { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
30 |
if (state == null) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
31 |
Color.red |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
32 |
else |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
33 |
state.phase match { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
34 |
case Phase.UNPROCESSED => new Color(255, 255, 192) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
35 |
case Phase.FINISHED => new Color(192, 255, 192) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
36 |
case Phase.FAILED => new Color(255, 192, 192) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
37 |
case _ => Color.red |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
38 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
39 |
} |
34391 | 40 |
|
41 |
def chooseColor(status : String) : Color = { |
|
42 |
//TODO: as properties! |
|
43 |
status match { |
|
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
44 |
//outer |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
45 |
case "ident" | "command" | "keyword" => Color.blue |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
46 |
case "verbatim"=> Color.green |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
47 |
case "comment" => Color.gray |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
48 |
case "control" => Color.white |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
49 |
case "malformed" => Color.red |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
50 |
case "string" | "altstring" => Color.orange |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
51 |
//logical |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
52 |
case "tclass" | "tycon" | "fixed_decl" | "fixed" |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
53 |
| "const_decl" | "const" | "fact_decl" | "fact" |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
54 |
|"dynamic_fact" |"local_fact_decl" | "local_fact" |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
55 |
=> new Color(255, 0, 255) |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
56 |
//inner syntax |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
57 |
case "tfree" | "free" => Color.blue |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
58 |
case "tvar" | "skolem" | "bound" | "var" => Color.green |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
59 |
case "num" | "xnum" | "xstr" | "literal" | "inner_comment" => new Color(255, 128, 128) |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
60 |
case "sort" | "typ" | "term" | "prop" | "attribute" | "method" => Color.yellow |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
61 |
// embedded source |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
62 |
case "doc_source" | "ML_source" | "ML_antic" | "doc_antiq" | "antiq" |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
63 |
=> new Color(0, 192, 0) |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
64 |
case _ => Color.white |
34391 | 65 |
} |
66 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
67 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
68 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
69 |
class TheoryView (text_area : JEditTextArea) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
70 |
extends TextAreaExtension with Text with BufferListener { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
71 |
import TheoryView._ |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
72 |
import Text.Changed |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
73 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
74 |
var col : Changed = null |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
75 |
|
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
76 |
val buffer = text_area.getBuffer |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
77 |
buffer.addBufferListener(this) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
78 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
79 |
val colTimer = new Timer(300, new ActionListener() { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
80 |
override def actionPerformed(e : ActionEvent) { commit() } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
81 |
}) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
82 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
83 |
val changesSource = new EventSource[Changed] |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
84 |
val phase_overview = new PhaseOverviewPanel(Plugin.prover(buffer)) |
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34402
diff
changeset
|
85 |
|
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34402
diff
changeset
|
86 |
val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll()) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
87 |
Plugin.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore()) |
34434 | 88 |
Plugin.self.font_changed.add(font => updateFont()) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
89 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
90 |
colTimer.stop |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
91 |
colTimer.setRepeats(true) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
92 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
93 |
def activate() { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
94 |
text_area.addCaretListener(selectedStateController) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
95 |
phase_overview.textarea = text_area |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
96 |
text_area.addLeftOfScrollBar(phase_overview) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
97 |
val painter = text_area.getPainter() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
98 |
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
99 |
updateFont() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
100 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
101 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
102 |
private def updateFont() { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
103 |
if (text_area != null) { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
104 |
val painter = text_area.getPainter() |
34434 | 105 |
if (Plugin.self.font != null) { |
106 |
painter.setStyles(painter.getStyles.map(style => |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
107 |
new SyntaxStyle(style.getForegroundColor, |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
108 |
style.getBackgroundColor, |
34434 | 109 |
Plugin.self.font) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
110 |
)) |
34434 | 111 |
painter.setFont(Plugin.self.font) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
112 |
repaintAll() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
113 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
114 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
115 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
116 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
117 |
def deactivate() { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
118 |
text_area.getPainter().removeExtension(this) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
119 |
text_area.removeCaretListener(selectedStateController) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
120 |
text_area.removeLeftOfScrollBar(phase_overview) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
121 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
122 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
123 |
val selectedStateController = new CaretListener() { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
124 |
override def caretUpdate(e : CaretEvent) { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
125 |
val cmd = Plugin.prover(buffer).document.getNextCommandContaining(e.getDot()) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
126 |
if (cmd != null && cmd.start <= e.getDot() && |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
127 |
Plugin.prover_setup(buffer).selectedState != cmd) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
128 |
Plugin.prover_setup(buffer).selectedState = cmd |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
129 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
130 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
131 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
132 |
private def fromCurrent(pos : Int) = |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
133 |
if (col != null && col.start <= pos) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
134 |
if (pos < col.start + col.added) col.start |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
135 |
else pos - col.added + col.removed |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
136 |
else pos |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
137 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
138 |
private def toCurrent(pos : Int) = |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
139 |
if (col != null && col.start <= pos) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
140 |
if (pos < col.start + col.removed) col.start |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
141 |
else pos + col.added - col.removed |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
142 |
else pos |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
143 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
144 |
def repaint(cmd : Command) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
145 |
{ |
34404
98155c35d252
delayed repainting new phase in buffer and overview;
immler@in.tum.de
parents:
34402
diff
changeset
|
146 |
val ph = cmd.phase |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
147 |
if (text_area != null && ph != Phase.REMOVE && ph != Phase.REMOVED) { |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
148 |
var start = text_area.getLineOfOffset(toCurrent(cmd.start)) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
149 |
var stop = text_area.getLineOfOffset(toCurrent(cmd.stop) - 1) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
150 |
text_area.invalidateLineRange(start, stop) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
151 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
152 |
if (Plugin.prover_setup(buffer).selectedState == cmd) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
153 |
Plugin.prover_setup(buffer).selectedState = cmd // update State view |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
154 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
155 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
156 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
157 |
def repaintAll() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
158 |
{ |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
159 |
if (text_area != null) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
160 |
text_area.invalidateLineRange(text_area.getFirstPhysicalLine, |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
161 |
text_area.getLastPhysicalLine) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
162 |
} |
34391 | 163 |
|
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
164 |
def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color, fill : Boolean){ |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
165 |
val fm = text_area.getPainter.getFontMetrics |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
166 |
val startP = text_area.offsetToXY(begin) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
167 |
val stopP = if (finish < buffer.getLength()) text_area.offsetToXY(finish) |
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
168 |
else { var p = text_area.offsetToXY(finish - 1) |
34391 | 169 |
p.x = p.x + fm.charWidth(' ') |
170 |
p } |
|
171 |
||
172 |
if (startP != null && stopP != null) { |
|
173 |
gfx.setColor(color) |
|
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
174 |
if(fill){gfx.fillRect(startP.x, y, stopP.x - startP.x, height)} |
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
175 |
else {gfx.drawRect(startP.x, y, stopP.x - startP.x, height)} |
34391 | 176 |
} |
177 |
} |
|
178 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
179 |
override def paintValidLine(gfx : Graphics2D, screenLine : Int, |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
180 |
pl : Int, start : Int, end : Int, y : Int) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
181 |
{ |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
182 |
val fm = text_area.getPainter.getFontMetrics |
34391 | 183 |
var savedColor = gfx.getColor |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
184 |
var e = Plugin.prover(buffer).document.getNextCommandContaining(fromCurrent(start)) |
34391 | 185 |
|
186 |
//Encolor Phase |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
187 |
while (e != null && toCurrent(e.start) < end) { |
34392
a02d46bca7e4
encoloring only details in the current line!
immler@in.tum.de
parents:
34391
diff
changeset
|
188 |
val begin = start max toCurrent(e.start) |
a02d46bca7e4
encoloring only details in the current line!
immler@in.tum.de
parents:
34391
diff
changeset
|
189 |
val finish = end - 1 min toCurrent(e.stop) |
34399
5b8b89b7e597
interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents:
34393
diff
changeset
|
190 |
encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e), true) |
34391 | 191 |
// paint details of command |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
192 |
for(node <- e.root_node.dfs){ |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
193 |
val begin = toCurrent(node.start + e.start) |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
194 |
val finish = toCurrent(node.end + e.start) |
34392
a02d46bca7e4
encoloring only details in the current line!
immler@in.tum.de
parents:
34391
diff
changeset
|
195 |
if(finish > start && begin < end) |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34399
diff
changeset
|
196 |
encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node.short), true) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
197 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
198 |
e = e.next |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
199 |
} |
34391 | 200 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
201 |
gfx.setColor(savedColor) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
202 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
203 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
204 |
def content(start : Int, stop : Int) = buffer.getText(start, stop - start) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34405
diff
changeset
|
205 |
override def length = buffer.getLength |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
206 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
207 |
def changes = changesSource |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
208 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
209 |
private def commit() { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
210 |
if (col != null) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
211 |
changes.fire(col) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
212 |
col = null |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
213 |
if (colTimer.isRunning()) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
214 |
colTimer.stop() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
215 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
216 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
217 |
private def delayCommit() { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
218 |
if (colTimer.isRunning()) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
219 |
colTimer.restart() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
220 |
else |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
221 |
colTimer.start() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
222 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
223 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
224 |
override def contentInserted(buffer : JEditBuffer, startLine : Int, |
34387
d67fe0cb1106
removed xsymbol converting -> sidekick should do that
immler@in.tum.de
parents:
34375
diff
changeset
|
225 |
offset : Int, numLines : Int, length : Int) { } |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
226 |
override def contentRemoved(buffer : JEditBuffer, startLine : Int, |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
227 |
offset : Int, numLines : Int, length : Int) { } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
228 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
229 |
override def preContentInserted(buffer : JEditBuffer, startLine : Int, |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
230 |
offset : Int, numLines : Int, length : Int) { |
34364 | 231 |
if (col == null) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
232 |
col = new Changed(offset, length, 0) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
233 |
else if (col.start <= offset && offset <= col.start + col.added) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
234 |
col = new Changed(col.start, col.added + length, col.removed) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
235 |
else { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
236 |
commit() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
237 |
col = new Changed(offset, length, 0) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
238 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
239 |
delayCommit() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
240 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
241 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
242 |
override def preContentRemoved(buffer : JEditBuffer, startLine : Int, |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
243 |
start : Int, numLines : Int, removed : Int) { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
244 |
if (col == null) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
245 |
col = new Changed(start, 0, removed) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
246 |
else if (col.start > start + removed || start > col.start + col.added) { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
247 |
commit() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
248 |
col = new Changed(start, 0, removed) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
249 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
250 |
else { |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
251 |
val offset = start - col.start |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
252 |
val diff = col.added - removed |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
253 |
val (added, addRemoved) = |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
254 |
if (diff < offset) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
255 |
(offset max 0, diff - (offset max 0)) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
256 |
else |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
257 |
(diff - (offset min 0), offset min 0) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
258 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
259 |
col = new Changed(start min col.start, added, col.removed - addRemoved) |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
260 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
261 |
delayCommit() |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
262 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
263 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
264 |
override def bufferLoaded(buffer : JEditBuffer) { } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
265 |
override def foldHandlerChanged(buffer : JEditBuffer) { } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
266 |
override def foldLevelChanged(buffer : JEditBuffer, startLine : Int, |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
267 |
endLine : Int) = { } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
268 |
override def transactionComplete(buffer : JEditBuffer) = { } |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
269 |
} |