equal
deleted
inserted
replaced
30 |
30 |
31 private var zoom_factor = 100 |
31 private var zoom_factor = 100 |
32 private var show_tracing = false |
32 private var show_tracing = false |
33 private var do_update = true |
33 private var do_update = true |
34 private var current_state = Command.empty.init_state |
34 private var current_state = Command.empty.init_state |
35 private var current_body: XML.Body = Nil |
35 private var current_output: List[XML.Tree] = Nil |
36 |
36 |
37 |
37 |
38 /* pretty text panel */ |
38 /* pretty text panel */ |
39 |
39 |
40 private val pretty_text_area = new Pretty_Text_Area(view) |
40 private val pretty_text_area = new Pretty_Text_Area(view) |
65 case None => Command.empty.init_state |
65 case None => Command.empty.init_state |
66 } |
66 } |
67 } |
67 } |
68 else current_state |
68 else current_state |
69 |
69 |
70 val new_body = |
70 val new_output = |
71 if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
71 if (!restriction.isDefined || restriction.get.contains(new_state.command)) |
72 new_state.results.iterator.map(_._2).filter( |
72 new_state.results.iterator.map(_._2).filter( |
73 { // FIXME not scalable |
73 { // FIXME not scalable |
74 case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing |
74 case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing |
75 case _ => true |
75 case _ => true |
76 }).toList |
76 }).toList |
77 else current_body |
77 else current_output |
78 |
78 |
79 if (new_body != current_body) pretty_text_area.update(new_body) |
79 if (new_output != current_output) |
|
80 pretty_text_area.update(Library.separate(Pretty.FBreak, new_output)) |
80 |
81 |
81 current_state = new_state |
82 current_state = new_state |
82 current_body = new_body |
83 current_output = new_output |
83 } |
84 } |
84 |
85 |
85 |
86 |
86 /* main actor */ |
87 /* main actor */ |
87 |
88 |