18 import scala.swing.{BorderPanel, Component} |
18 import scala.swing.{BorderPanel, Component} |
19 |
19 |
20 |
20 |
21 object Pretty_Text_Area |
21 object Pretty_Text_Area |
22 { |
22 { |
23 def document_state(formatted_body: XML.Body): Document.State = |
23 def document_state(formatted_body: XML.Body): (String, Document.State) = |
24 { |
24 { |
25 val command = Command.rich_text(Document.new_id(), formatted_body) |
25 val command = Command.rich_text(Document.new_id(), formatted_body) |
26 val node_name = command.node_name |
26 val node_name = command.node_name |
27 |
27 |
28 val edits: List[Document.Edit_Text] = |
28 val edits: List[Document.Edit_Text] = |
37 val state1 = |
37 val state1 = |
38 state0.continue_history(Future.value(version0), edits, Future.value(version1))._2 |
38 state0.continue_history(Future.value(version0), edits, Future.value(version1))._2 |
39 .define_version(version1, state0.the_assignment(version0)) |
39 .define_version(version1, state0.the_assignment(version0)) |
40 .assign(version1.id, List(command.id -> Some(Document.new_id())))._2 |
40 .assign(version1.id, List(command.id -> Some(Document.new_id())))._2 |
41 |
41 |
42 state1 |
42 (command.source, state1) |
43 } |
43 } |
44 } |
44 } |
45 |
45 |
46 class Pretty_Text_Area(view: View) extends BorderPanel |
46 class Pretty_Text_Area(view: View) extends BorderPanel |
47 { |
47 { |
50 private var current_font_metrics: FontMetrics = null |
50 private var current_font_metrics: FontMetrics = null |
51 private var current_font_family = "Dialog" |
51 private var current_font_family = "Dialog" |
52 private var current_font_size: Int = 12 |
52 private var current_font_size: Int = 12 |
53 private var current_margin: Int = 0 |
53 private var current_margin: Int = 0 |
54 private var current_body: XML.Body = Nil |
54 private var current_body: XML.Body = Nil |
55 private var current_rendering: Isabelle_Rendering = make_rendering() |
55 private var current_rendering: Isabelle_Rendering = text_rendering()._2 |
56 |
56 |
57 private def make_rendering(): Isabelle_Rendering = |
57 val text_area = new JEditEmbeddedTextArea |
|
58 val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering) |
|
59 |
|
60 private def text_rendering(): (String, Isabelle_Rendering) = |
58 { |
61 { |
59 Swing_Thread.require() |
62 Swing_Thread.require() |
60 |
63 |
61 val body = |
64 val body = |
62 Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics)) |
65 Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics)) |
63 Isabelle_Rendering(Pretty_Text_Area.document_state(body).snapshot(), Isabelle.options.value) |
66 val (text, state) = Pretty_Text_Area.document_state(body) |
|
67 val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value) |
|
68 |
|
69 (text, rendering) |
64 } |
70 } |
65 |
|
66 val text_area = new JEditEmbeddedTextArea |
|
67 val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering) |
|
68 |
71 |
69 def refresh() |
72 def refresh() |
70 { |
73 { |
71 Swing_Thread.require() |
74 Swing_Thread.require() |
72 |
75 |
78 painter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) |
81 painter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) |
79 |
82 |
80 current_font_metrics = painter.getFontMetrics(font) |
83 current_font_metrics = painter.getFontMetrics(font) |
81 current_margin = (size.width / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20 |
84 current_margin = (size.width / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20 |
82 |
85 |
83 val text = |
86 val (text, rendering) = text_rendering() |
84 Pretty.string_of(current_body, current_margin, Pretty.font_metric(current_font_metrics)) |
87 current_rendering = rendering |
85 |
88 |
86 val buffer = text_area.getBuffer |
89 val buffer = text_area.getBuffer |
87 try { |
90 try { |
88 buffer.beginCompoundEdit |
91 buffer.beginCompoundEdit |
89 text_area.setText(text) |
92 text_area.setText(text) |