changeset 34813 | f0107bc96961 |
parent 34777 | 91d6089cef88 |
child 34817 | b4efd0ef2f3e |
--- a/src/Tools/jEdit/src/proofdocument/state.scala Wed Dec 30 13:21:46 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/state.scala Wed Dec 30 17:48:58 2009 +0100 @@ -11,7 +11,7 @@ class State( val command: Command, val status: Command.Status.Value, - rev_results: List[XML.Tree], + val rev_results: List[XML.Tree], val markup_root: Markup_Text) { def this(command: Command) =