src/Tools/jEdit/src/pretty_text_area.scala
author wenzelm
Tue, 18 Sep 2012 19:42:32 +0200
changeset 49420 32cb1f1a6a5d
parent 49419 e2726211f834
child 49421 0988d31e9140
permissions -rw-r--r--
token marker for extended syntax styles;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/pretty_text_area.scala
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     3
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     4
GUI component for pretty-printed with markup, rendered like jEdit text area.
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     5
*/
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     6
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     8
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     9
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    10
import isabelle._
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    11
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    12
import java.awt.{Font, FontMetrics}
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    13
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    14
import org.gjt.sp.jedit.{jEdit, View}
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    15
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    16
import org.gjt.sp.util.SyntaxUtilities
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    17
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    18
import scala.swing.{BorderPanel, Component}
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    19
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    20
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    21
object Pretty_Text_Area
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    22
{
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    23
  def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    24
    : (String, Document.State) =
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    25
  {
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49413
diff changeset
    26
    val command = Command.rich_text(Document.new_id(), formatted_body)
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    27
    val node_name = command.node_name
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    28
    val edits: List[Document.Edit_Text] =
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49413
diff changeset
    29
      List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    30
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    31
    val state0 = base_snapshot.state.define_command(command)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    32
    val version0 = base_snapshot.version
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    33
    val nodes0 = version0.nodes
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    34
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    35
    assert(nodes0(node_name).commands.isEmpty)
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    36
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    37
    val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    38
    val version1 = Document.Version.make(version0.syntax, nodes1)
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    39
    val state1 =
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    40
      state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    41
        .define_version(version1, state0.the_assignment(version0))
49414
d7b5fb2e9ca2 some support for inital command markup;
wenzelm
parents: 49413
diff changeset
    42
        .assign(version1.id, List(command.id -> Some(Document.new_id())))._2
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    43
49416
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    44
    (command.source, state1)
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    45
  }
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    46
}
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    47
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    48
class Pretty_Text_Area(view: View) extends BorderPanel
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    49
{
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    50
  Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    51
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    52
  private var current_font_metrics: FontMetrics = null
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    53
  private var current_font_family = "Dialog"
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    54
  private var current_font_size: Int = 12
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    55
  private var current_margin: Int = 0
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    56
  private var current_body: XML.Body = Nil
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    57
  private var current_base_snapshot = Document.State.init.snapshot()
49416
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    58
  private var current_rendering: Isabelle_Rendering = text_rendering()._2
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    59
49416
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    60
  val text_area = new JEditEmbeddedTextArea
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    61
  val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    62
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    63
  private def text_rendering(): (String, Isabelle_Rendering) =
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    64
  {
49413
8c9925d31617 more static rendering state;
wenzelm
parents: 49412
diff changeset
    65
    Swing_Thread.require()
8c9925d31617 more static rendering state;
wenzelm
parents: 49412
diff changeset
    66
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    67
    val body =
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    68
      Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics))
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
    69
    val (text, state) = Pretty_Text_Area.document_state(current_base_snapshot, body)
49416
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    70
    val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    71
49416
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    72
    (text, rendering)
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    73
  }
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
    74
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    75
  def refresh()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    76
  {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    77
    Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    78
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    79
    val font = new Font(current_font_family, Font.PLAIN, current_font_size)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    80
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    81
    val painter = text_area.getPainter
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    82
    painter.setFont(font)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    83
    painter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    84
    painter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    85
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    86
    current_font_metrics = painter.getFontMetrics(font)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    87
    current_margin = (size.width / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    88
49416
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    89
    val (text, rendering) = text_rendering()
1053a564dd25 some actual rich text markup via XML.content_markup;
wenzelm
parents: 49414
diff changeset
    90
    current_rendering = rendering
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    91
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    92
    val buffer = text_area.getBuffer
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    93
    try {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    94
      buffer.beginCompoundEdit
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    95
      text_area.setText(text)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    96
      text_area.setCaretPosition(0)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    97
    }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    98
    finally {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    99
      buffer.endCompoundEdit
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   100
    }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   101
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   102
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   103
  def resize(font_family: String, font_size: Int)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   104
  {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   105
    Swing_Thread.require()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   106
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   107
    current_font_family = font_family
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   108
    current_font_size = font_size
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   109
    refresh()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   110
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   111
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
   112
  def update(base_snapshot: Document.Snapshot, body: XML.Body)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   113
  {
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   114
    Swing_Thread.require()
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
   115
    require(!base_snapshot.is_outdated)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   116
49419
e2726211f834 pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents: 49416
diff changeset
   117
    current_base_snapshot = base_snapshot
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   118
    current_body = body
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   119
    refresh()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   120
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   121
49420
32cb1f1a6a5d token marker for extended syntax styles;
wenzelm
parents: 49419
diff changeset
   122
  text_area.getBuffer.setTokenMarker(new Token_Markup.Marker(true, None))
49412
4cac648e0f85 Pretty_Text_Area is based on Rich_Text_Area;
wenzelm
parents: 49398
diff changeset
   123
  rich_text_area.activate()
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   124
  layout(Component.wrap(text_area)) = BorderPanel.Position.Center
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   125
}
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   126