# HG changeset patch # User wenzelm # Date 1281615743 -7200 # Node ID 754ad6340055810abdcfc44ab263368993b105c6 # Parent b609d0b271faaafde239caba568d23aace2ed72b misc tuning and simplification; diff -r b609d0b271fa -r 754ad6340055 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Aug 12 13:59:18 2010 +0200 +++ b/src/Pure/PIDE/command.scala Thu Aug 12 14:22:23 2010 +0200 @@ -30,14 +30,15 @@ command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. State_ID !? + /** accumulated results from prover **/ - class State( + case class State( val command: Command, val status: Command.Status.Value, val forks: Int, val reverse_results: List[XML.Tree], - val markup_root: Markup_Text) + val markup: Markup_Text) { def this(command: Command) = this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup) @@ -45,33 +46,25 @@ /* content */ - private def set_status(st: Command.Status.Value): State = - new State(command, st, forks, reverse_results, markup_root) - - private def add_forks(i: Int): State = - new State(command, status, forks + i, reverse_results, markup_root) + lazy val results = reverse_results.reverse - private def add_result(res: XML.Tree): State = - new State(command, status, forks, res :: reverse_results, markup_root) + def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) - private def add_markup(node: Markup_Tree): State = - new State(command, status, forks, reverse_results, markup_root + node) - - lazy val results = reverse_results.reverse + def add_markup(node: Markup_Tree): State = copy(markup = markup + node) /* markup */ lazy val highlight: Markup_Text = { - markup_root.filter(_.info match { + markup.filter(_.info match { case Command.HighlightInfo(_, _) => true case _ => false }) } private lazy val types: List[Markup_Node] = - markup_root.filter(_.info match { + markup.filter(_.info match { case Command.TypeInfo(_) => true case _ => false }).flatten @@ -88,7 +81,7 @@ } private lazy val refs: List[Markup_Node] = - markup_root.filter(_.info match { + markup.filter(_.info match { case Command.RefInfo(_, _, _, _) => true case _ => false }).flatten @@ -103,11 +96,11 @@ case XML.Elem(Markup(Markup.STATUS, _), elems) => (this /: elems)((state, elem) => elem match { - case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED) - case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED) - case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED) - case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1) - case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1) + case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED) + case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED) + case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED) + case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1) + case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1) case _ => System.err.println("Ignored status message: " + elem); state }) @@ -125,13 +118,14 @@ else if (kind == Markup.ML_REF) { body match { case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) => - state.add_markup(command.markup_node( - begin - 1, end - 1, - Command.RefInfo( - Position.get_file(props), - Position.get_line(props), - Position.get_id(props), - Position.get_offset(props)))) + state.add_markup( + command.markup_node( + begin - 1, end - 1, + Command.RefInfo( + Position.get_file(props), + Position.get_line(props), + Position.get_id(props), + Position.get_offset(props)))) case _ => state } } diff -r b609d0b271fa -r 754ad6340055 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 12 13:59:18 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 12 14:22:23 2010 +0200 @@ -130,7 +130,7 @@ val root = data.root val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) { - root.add(snapshot.state(command).markup_root.swing_tree((node: Markup_Node) => + root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) => { val content = command.source(node.start, node.stop).replace('\n', ' ') val id = command.id