src/Tools/jEdit/src/jedit/TheoryView.scala
author wenzelm
Sun, 28 Dec 2008 18:40:38 +0100
changeset 34446 5c79f97ec1d1
parent 34445 61ffe9a35f1d
child 34447 dc8b486fde9f
permissions -rw-r--r--
superficial tuning; improved comments and sectioning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     1
/*
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34407
diff changeset
     2
 * jEdit text area as document text source
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     3
 *
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     4
 * @author Fabian Immler, TU Munich
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     5
 * @author Johannes Hölzl, TU Munich
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     6
 */
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     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
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    10
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    11
import isabelle.utils.EventSource
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    12
import isabelle.proofdocument.Text
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    13
import isabelle.prover.{Prover, Command, CommandChangeInfo}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    14
import isabelle.prover.Command.Phase
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    15
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    16
import javax.swing.Timer
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    17
import javax.swing.event.{CaretListener, CaretEvent}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    18
import java.awt.Graphics2D
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    19
import java.awt.event.{ActionEvent, ActionListener}
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    20
import java.awt.Color
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    21
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    22
import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    23
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
    24
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
    25
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    26
34318
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
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    29
  def choose_color(state: Command): Color = {
34318
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
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
    40
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    41
  def choose_color(markup: String): Color = {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    42
    // TODO: as properties
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    43
    markup match {
34445
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    44
      // logical entities
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    45
      case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    46
        | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    47
        | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255)
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    48
      // inner syntax
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    49
      case Markup.TFREE | Markup.FREE => Color.blue
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    50
      case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    51
      case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    52
        | Markup.INNER_COMMENT => new Color(255, 128, 128)
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    53
      case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    54
        | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow
34445
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    55
      // embedded source text
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    56
      case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    57
        | Markup.DOC_ANTIQ => new Color(0, 192, 0)
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    58
      // outer syntax
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    59
      case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    60
      case Markup.VERBATIM => Color.green
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    61
      case Markup.COMMENT => Color.gray
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    62
      case Markup.CONTROL => Color.white
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    63
      case Markup.MALFORMED => Color.red
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    64
      case Markup.STRING | Markup.ALTSTRING => Color.orange
61ffe9a35f1d use symbolic Markup elements instead of literal strings;
wenzelm
parents: 34440
diff changeset
    65
      // other
34399
5b8b89b7e597 interpretation of STATUS messages in one place, deleting inner syntax
immler@in.tum.de
parents: 34393
diff changeset
    66
      case _ => Color.white
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
    67
    }
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
    68
  }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    69
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    70
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    71
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    72
class TheoryView (text_area: JEditTextArea)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    73
    extends TextAreaExtension with Text with BufferListener {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents: 34405
diff changeset
    74
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    75
  private val buffer = text_area.getBuffer
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents: 34405
diff changeset
    76
  buffer.addBufferListener(this)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    77
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    78
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    79
  private var col: Text.Changed = null
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    80
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    81
  private val col_timer = new Timer(300, new ActionListener() {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    82
    override def actionPerformed(e: ActionEvent) = commit()
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    83
  })
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents: 34405
diff changeset
    84
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    85
  col_timer.stop
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    86
  col_timer.setRepeats(true)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    87
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    88
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    89
  private val changes_source = new EventSource[Text.Changed]
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    90
  private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    91
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    92
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    93
  /* activation */
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    94
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    95
  Isabelle.plugin.font_changed.add(font => update_font())
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    96
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    97
  private def update_font() = {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents: 34405
diff changeset
    98
    if (text_area != null) {
34440
561a6d19bd95 renamed object Plugin to Isabelle;
wenzelm
parents: 34434
diff changeset
    99
      if (Isabelle.plugin.font != null) {
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   100
        val painter = text_area.getPainter
34434
ba08fc74f98a renamed Plugin.plugin to Plugin.self;
wenzelm
parents: 34408
diff changeset
   101
        painter.setStyles(painter.getStyles.map(style =>
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   102
          new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   103
        ))
34440
561a6d19bd95 renamed object Plugin to Isabelle;
wenzelm
parents: 34434
diff changeset
   104
        painter.setFont(Isabelle.plugin.font)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   105
        repaint_all()
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   106
      }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   107
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   108
  }
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   109
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   110
  private val selected_state_controller = new CaretListener {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   111
    override def caretUpdate(e: CaretEvent) = {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   112
      val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   113
      if (cmd != null && cmd.start <= e.getDot &&
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   114
          Isabelle.prover_setup(buffer).selectedState != cmd)
34440
561a6d19bd95 renamed object Plugin to Isabelle;
wenzelm
parents: 34434
diff changeset
   115
        Isabelle.prover_setup(buffer).selectedState = cmd
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   116
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   117
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   118
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   119
  def activate() = {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   120
    text_area.addCaretListener(selected_state_controller)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   121
    phase_overview.textarea = text_area
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   122
    text_area.addLeftOfScrollBar(phase_overview)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   123
    text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   124
    update_font()
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   125
  }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   126
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   127
  def deactivate() = {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   128
    text_area.getPainter.removeExtension(this)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   129
    text_area.removeLeftOfScrollBar(phase_overview)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   130
    text_area.removeCaretListener(selected_state_controller)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   131
  }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   132
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   133
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   134
  /* painting */
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   135
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   136
  val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   137
  Isabelle.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   138
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   139
  private def from_current(pos: Int) =
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   140
    if (col != null && col.start <= pos)
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   141
      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
   142
      else pos - col.added + col.removed
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   143
    else pos
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   144
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   145
  private def to_current(pos : Int) =
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   146
    if (col != null && col.start <= pos)
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   147
      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
   148
      else pos + col.added - col.removed
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   149
    else pos
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   150
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   151
  def repaint(cmd: Command) =
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   152
  {
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   153
    val phase = cmd.phase
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   154
    if (text_area != null && phase != Phase.REMOVE && phase != Phase.REMOVED) {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   155
      val start = text_area.getLineOfOffset(to_current(cmd.start))
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   156
      val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents: 34405
diff changeset
   157
      text_area.invalidateLineRange(start, stop)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   158
34440
561a6d19bd95 renamed object Plugin to Isabelle;
wenzelm
parents: 34434
diff changeset
   159
      if (Isabelle.prover_setup(buffer).selectedState == cmd)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   160
        Isabelle.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
   161
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   162
  }
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   163
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   164
  def repaint_all() =
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   165
  {
34406
f81cd75ae331 restructured: independent provers in different buffers
immler@in.tum.de
parents: 34405
diff changeset
   166
    if (text_area != null)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   167
      text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   168
  }
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
   169
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   170
  def encolor(gfx: Graphics2D,
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   171
    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) =
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   172
  {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   173
    val start = text_area.offsetToXY(begin)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   174
    val stop =
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   175
      if (finish < buffer.getLength) text_area.offsetToXY(finish)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   176
      else {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   177
        val p = text_area.offsetToXY(finish - 1)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   178
        p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ')
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   179
        p
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
   180
      }
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   181
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   182
    if (start != null && stop != null) {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   183
      gfx.setColor(color)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   184
      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   185
      else gfx.drawRect(start.x, y, stop.x - start.x, height)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   186
    }
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
   187
  }
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
   188
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   189
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   190
  /* TextAreaExtension methods */
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   191
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   192
  override def paintValidLine(gfx: Graphics2D,
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   193
    screen_line: Int, pl: Int, start: Int, end: Int, y: Int) =
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   194
  {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   195
    val saved_color = gfx.getColor
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   196
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   197
    val metrics = text_area.getPainter.getFontMetrics
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   198
    var e = Isabelle.prover(buffer).document.getNextCommandContaining(from_current(start))
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
   199
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   200
    // encolor phase
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   201
    while (e != null && to_current(e.start) < end) {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   202
      val begin = start max to_current(e.start)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   203
      val finish = end - 1 min to_current(e.stop)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   204
      encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   205
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
   206
      // paint details of command
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   207
      for (node <- e.root_node.dfs) {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   208
        val begin = to_current(node.start + e.start)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   209
        val finish = to_current(node.end + e.start)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   210
        if (finish > start && begin < end) {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   211
          encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end,
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   212
            TheoryView.choose_color(node.short), true)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   213
        }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   214
      }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   215
      e = e.next
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   216
    }
34391
7b5f44553aaf ugly fine-grained buffer markup
immler@in.tum.de
parents: 34387
diff changeset
   217
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   218
    gfx.setColor(saved_color)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   219
  }
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   220
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   221
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   222
  /* Text methods */
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   223
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   224
  def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   225
  def length = buffer.getLength
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   226
  def changes = changes_source
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   227
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   228
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   229
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   230
  /* BufferListener methods */
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   231
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   232
  private def commit() {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   233
    if (col != null)
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   234
      changes.fire(col)
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   235
    col = null
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   236
    if (col_timer.isRunning())
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   237
      col_timer.stop()
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   238
  }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   239
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   240
  private def delay_commit() {
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   241
    if (col_timer.isRunning())
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   242
      col_timer.restart()
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   243
    else
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   244
      col_timer.start()
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   245
  }
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   246
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   247
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   248
  override def contentInserted(buffer: JEditBuffer,
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   249
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   250
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   251
  override def contentRemoved(buffer: JEditBuffer,
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   252
    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   253
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   254
  override def preContentInserted(buffer: JEditBuffer,
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   255
    start_line: Int, offset: Int, num_lines: Int, length: Int) =
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   256
  {
34364
8df6519599ef playing with xsymbols
immler@in.tum.de
parents: 34318
diff changeset
   257
    if (col == null)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   258
      col = new Text.Changed(offset, length, 0)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   259
    else if (col.start <= offset && offset <= col.start + col.added)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   260
      col = new Text.Changed(col.start, col.added + length, col.removed)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   261
    else {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   262
      commit()
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   263
      col = new Text.Changed(offset, length, 0)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   264
    }
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   265
    delay_commit()
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   266
  }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   267
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   268
  override def preContentRemoved(buffer: JEditBuffer,
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   269
    start_line: Int, start: Int, num_lines: Int, removed: Int) =
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   270
  {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   271
    if (col == null)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   272
      col = new Text.Changed(start, 0, removed)
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   273
    else if (col.start > start + removed || start > col.start + col.added) {
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   274
      commit()
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   275
      col = new Text.Changed(start, 0, removed)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   276
    }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   277
    else {
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   278
      val offset = start - col.start
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   279
      val diff = col.added - removed
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   280
      val (added, add_removed) =
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   281
        if (diff < offset)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   282
          (offset max 0, diff - (offset max 0))
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   283
        else
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   284
          (diff - (offset min 0), offset min 0)
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   285
      col = new Text.Changed(start min col.start, added, col.removed - add_removed)
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   286
    }
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   287
    delay_commit()
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   288
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   289
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   290
  override def bufferLoaded(buffer: JEditBuffer) { }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   291
  override def foldHandlerChanged(buffer: JEditBuffer) { }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   292
  override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
   293
  override def transactionComplete(buffer: JEditBuffer) { }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
   294
}