# HG changeset patch # User wenzelm # Date 1281614358 -7200 # Node ID b609d0b271faaafde239caba568d23aace2ed72b # Parent 53224a4d2f0e5f1d33e77097555de5fcf3deca3f specific command state; diff -r 53224a4d2f0e -r b609d0b271fa src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Aug 12 13:49:08 2010 +0200 +++ b/src/Pure/PIDE/command.scala Thu Aug 12 13:59:18 2010 +0200 @@ -1,5 +1,4 @@ /* Title: Pure/PIDE/command.scala - Author: Johannes Hölzl, TU Munich Author: Fabian Immler, TU Munich Author: Makarius @@ -29,8 +28,128 @@ case class TypeInfo(ty: String) case class RefInfo(file: Option[String], line: Option[Int], command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. State_ID !? + + + /** accumulated results from prover **/ + + class State( + val command: Command, + val status: Command.Status.Value, + val forks: Int, + val reverse_results: List[XML.Tree], + val markup_root: Markup_Text) + { + def this(command: Command) = + this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup) + + + /* 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) + + private def add_result(res: XML.Tree): State = + new State(command, status, forks, res :: reverse_results, markup_root) + + private def add_markup(node: Markup_Tree): State = + new State(command, status, forks, reverse_results, markup_root + node) + + lazy val results = reverse_results.reverse + + + /* markup */ + + lazy val highlight: Markup_Text = + { + markup_root.filter(_.info match { + case Command.HighlightInfo(_, _) => true + case _ => false + }) + } + + private lazy val types: List[Markup_Node] = + markup_root.filter(_.info match { + case Command.TypeInfo(_) => true + case _ => false }).flatten + + def type_at(pos: Int): Option[String] = + { + types.find(t => t.start <= pos && pos < t.stop) match { + case Some(t) => + t.info match { + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty) + case _ => None + } + case None => None + } + } + + private lazy val refs: List[Markup_Node] = + markup_root.filter(_.info match { + case Command.RefInfo(_, _, _, _) => true + case _ => false }).flatten + + def ref_at(pos: Int): Option[Markup_Node] = + refs.find(t => t.start <= pos && pos < t.stop) + + + /* message dispatch */ + + def accumulate(message: XML.Tree): Command.State = + message match { + 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 _ => System.err.println("Ignored status message: " + elem); state + }) + + case XML.Elem(Markup(Markup.REPORT, _), elems) => + (this /: elems)((state, elem) => + elem match { + case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => + atts match { + case Position.Range(begin, end) => + if (kind == Markup.ML_TYPING) { + val info = Pretty.string_of(body, margin = 40) + state.add_markup( + command.markup_node(begin - 1, end - 1, Command.TypeInfo(info))) + } + 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)))) + case _ => state + } + } + else { + state.add_markup( + command.markup_node(begin - 1, end - 1, + Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) + } + case _ => state + } + case _ => System.err.println("Ignored report message: " + elem); state + }) + case _ => add_result(message) + } + } } + class Command( val id: Document.Command_ID, val span: Thy_Syntax.Span, @@ -59,8 +178,8 @@ /* accumulated messages */ - @volatile protected var state = new State(this) - def current_state: State = state + @volatile protected var state = new Command.State(this) + def current_state: Command.State = state private case class Consume(message: XML.Tree, forward: Command => Unit) private case object Assign diff -r 53224a4d2f0e -r b609d0b271fa src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 12 13:49:08 2010 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 12 13:59:18 2010 +0200 @@ -101,7 +101,7 @@ val is_outdated: Boolean def convert(offset: Int): Int def revert(offset: Int): Int - def state(command: Command): State + def state(command: Command): Command.State } object Change @@ -146,7 +146,7 @@ val is_outdated = !(pending_edits.isEmpty && latest == stable.get) def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) - def state(command: Command): State = document.current_state(command) + def state(command: Command): Command.State = document.current_state(command) } } } @@ -281,12 +281,12 @@ tmp_states = Map() } - def current_state(cmd: Command): State = + def current_state(cmd: Command): Command.State = { require(assignment.is_finished) (assignment.join).get(cmd) match { case Some(cmd_state) => cmd_state.current_state - case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup) + case None => new Command.State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup) } } } diff -r 53224a4d2f0e -r b609d0b271fa src/Pure/PIDE/state.scala --- a/src/Pure/PIDE/state.scala Thu Aug 12 13:49:08 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,125 +0,0 @@ -/* Title: Pure/PIDE/state.scala - Author: Fabian Immler, TU Munich - Author: Makarius - -Accumulated results from prover. -*/ - -package isabelle - - -class State( - val command: Command, - val status: Command.Status.Value, - val forks: Int, - val reverse_results: List[XML.Tree], - val markup_root: Markup_Text) -{ - def this(command: Command) = - this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup) - - - /* 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) - - private def add_result(res: XML.Tree): State = - new State(command, status, forks, res :: reverse_results, markup_root) - - private def add_markup(node: Markup_Tree): State = - new State(command, status, forks, reverse_results, markup_root + node) - - lazy val results = reverse_results.reverse - - - /* markup */ - - lazy val highlight: Markup_Text = - { - markup_root.filter(_.info match { - case Command.HighlightInfo(_, _) => true - case _ => false - }) - } - - private lazy val types: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.TypeInfo(_) => true - case _ => false }).flatten - - def type_at(pos: Int): Option[String] = - { - types.find(t => t.start <= pos && pos < t.stop) match { - case Some(t) => - t.info match { - case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty) - case _ => None - } - case None => None - } - } - - private lazy val refs: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.RefInfo(_, _, _, _) => true - case _ => false }).flatten - - def ref_at(pos: Int): Option[Markup_Node] = - refs.find(t => t.start <= pos && pos < t.stop) - - - /* message dispatch */ - - def accumulate(message: XML.Tree): State = - message match { - 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 _ => System.err.println("Ignored status message: " + elem); state - }) - - case XML.Elem(Markup(Markup.REPORT, _), elems) => - (this /: elems)((state, elem) => - elem match { - case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => - atts match { - case Position.Range(begin, end) => - if (kind == Markup.ML_TYPING) { - val info = Pretty.string_of(body, margin = 40) - state.add_markup( - command.markup_node(begin - 1, end - 1, Command.TypeInfo(info))) - } - 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)))) - case _ => state - } - } - else { - state.add_markup( - command.markup_node(begin - 1, end - 1, - Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) - } - case _ => state - } - case _ => System.err.println("Ignored report message: " + elem); state - }) - case _ => add_result(message) - } -} diff -r 53224a4d2f0e -r b609d0b271fa src/Pure/build-jars --- a/src/Pure/build-jars Thu Aug 12 13:49:08 2010 +0200 +++ b/src/Pure/build-jars Thu Aug 12 13:59:18 2010 +0200 @@ -42,7 +42,6 @@ PIDE/document.scala PIDE/event_bus.scala PIDE/markup_node.scala - PIDE/state.scala PIDE/text_edit.scala System/cygwin.scala System/download.scala