specific command state;
authorwenzelm
Thu Aug 12 13:59:18 2010 +0200 (2010-08-12)
changeset 38361b609d0b271fa
parent 38360 53224a4d2f0e
child 38362 754ad6340055
specific command state;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/state.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 12 13:49:08 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 12 13:59:18 2010 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  /*  Title:      Pure/PIDE/command.scala
     1.5 -    Author:     Johannes Hölzl, TU Munich
     1.6      Author:     Fabian Immler, TU Munich
     1.7      Author:     Makarius
     1.8  
     1.9 @@ -29,8 +28,128 @@
    1.10    case class TypeInfo(ty: String)
    1.11    case class RefInfo(file: Option[String], line: Option[Int],
    1.12      command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
    1.13 +
    1.14 +
    1.15 +  /** accumulated results from prover **/
    1.16 +
    1.17 +  class State(
    1.18 +    val command: Command,
    1.19 +    val status: Command.Status.Value,
    1.20 +    val forks: Int,
    1.21 +    val reverse_results: List[XML.Tree],
    1.22 +    val markup_root: Markup_Text)
    1.23 +  {
    1.24 +    def this(command: Command) =
    1.25 +      this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
    1.26 +
    1.27 +
    1.28 +    /* content */
    1.29 +
    1.30 +    private def set_status(st: Command.Status.Value): State =
    1.31 +      new State(command, st, forks, reverse_results, markup_root)
    1.32 +
    1.33 +    private def add_forks(i: Int): State =
    1.34 +      new State(command, status, forks + i, reverse_results, markup_root)
    1.35 +
    1.36 +    private def add_result(res: XML.Tree): State =
    1.37 +      new State(command, status, forks, res :: reverse_results, markup_root)
    1.38 +
    1.39 +    private def add_markup(node: Markup_Tree): State =
    1.40 +      new State(command, status, forks, reverse_results, markup_root + node)
    1.41 +
    1.42 +    lazy val results = reverse_results.reverse
    1.43 +
    1.44 +
    1.45 +    /* markup */
    1.46 +
    1.47 +    lazy val highlight: Markup_Text =
    1.48 +    {
    1.49 +      markup_root.filter(_.info match {
    1.50 +        case Command.HighlightInfo(_, _) => true
    1.51 +        case _ => false
    1.52 +      })
    1.53 +    }
    1.54 +
    1.55 +    private lazy val types: List[Markup_Node] =
    1.56 +      markup_root.filter(_.info match {
    1.57 +        case Command.TypeInfo(_) => true
    1.58 +        case _ => false }).flatten
    1.59 +
    1.60 +    def type_at(pos: Int): Option[String] =
    1.61 +    {
    1.62 +      types.find(t => t.start <= pos && pos < t.stop) match {
    1.63 +        case Some(t) =>
    1.64 +          t.info match {
    1.65 +            case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
    1.66 +            case _ => None
    1.67 +          }
    1.68 +        case None => None
    1.69 +      }
    1.70 +    }
    1.71 +
    1.72 +    private lazy val refs: List[Markup_Node] =
    1.73 +      markup_root.filter(_.info match {
    1.74 +        case Command.RefInfo(_, _, _, _) => true
    1.75 +        case _ => false }).flatten
    1.76 +
    1.77 +    def ref_at(pos: Int): Option[Markup_Node] =
    1.78 +      refs.find(t => t.start <= pos && pos < t.stop)
    1.79 +
    1.80 +
    1.81 +    /* message dispatch */
    1.82 +
    1.83 +    def accumulate(message: XML.Tree): Command.State =
    1.84 +      message match {
    1.85 +        case XML.Elem(Markup(Markup.STATUS, _), elems) =>
    1.86 +          (this /: elems)((state, elem) =>
    1.87 +            elem match {
    1.88 +              case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
    1.89 +              case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
    1.90 +              case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
    1.91 +              case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
    1.92 +              case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
    1.93 +              case _ => System.err.println("Ignored status message: " + elem); state
    1.94 +            })
    1.95 +
    1.96 +        case XML.Elem(Markup(Markup.REPORT, _), elems) =>
    1.97 +          (this /: elems)((state, elem) =>
    1.98 +            elem match {
    1.99 +              case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
   1.100 +                atts match {
   1.101 +                  case Position.Range(begin, end) =>
   1.102 +                    if (kind == Markup.ML_TYPING) {
   1.103 +                      val info = Pretty.string_of(body, margin = 40)
   1.104 +                      state.add_markup(
   1.105 +                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
   1.106 +                    }
   1.107 +                    else if (kind == Markup.ML_REF) {
   1.108 +                      body match {
   1.109 +                        case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
   1.110 +                          state.add_markup(command.markup_node(
   1.111 +                            begin - 1, end - 1,
   1.112 +                            Command.RefInfo(
   1.113 +                              Position.get_file(props),
   1.114 +                              Position.get_line(props),
   1.115 +                              Position.get_id(props),
   1.116 +                              Position.get_offset(props))))
   1.117 +                        case _ => state
   1.118 +                      }
   1.119 +                    }
   1.120 +                    else {
   1.121 +                      state.add_markup(
   1.122 +                        command.markup_node(begin - 1, end - 1,
   1.123 +                          Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
   1.124 +                    }
   1.125 +                  case _ => state
   1.126 +                }
   1.127 +              case _ => System.err.println("Ignored report message: " + elem); state
   1.128 +            })
   1.129 +        case _ => add_result(message)
   1.130 +      }
   1.131 +  }
   1.132  }
   1.133  
   1.134 +
   1.135  class Command(
   1.136      val id: Document.Command_ID,
   1.137      val span: Thy_Syntax.Span,
   1.138 @@ -59,8 +178,8 @@
   1.139  
   1.140    /* accumulated messages */
   1.141  
   1.142 -  @volatile protected var state = new State(this)
   1.143 -  def current_state: State = state
   1.144 +  @volatile protected var state = new Command.State(this)
   1.145 +  def current_state: Command.State = state
   1.146  
   1.147    private case class Consume(message: XML.Tree, forward: Command => Unit)
   1.148    private case object Assign
     2.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 12 13:49:08 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 12 13:59:18 2010 +0200
     2.3 @@ -101,7 +101,7 @@
     2.4      val is_outdated: Boolean
     2.5      def convert(offset: Int): Int
     2.6      def revert(offset: Int): Int
     2.7 -    def state(command: Command): State
     2.8 +    def state(command: Command): Command.State
     2.9    }
    2.10  
    2.11    object Change
    2.12 @@ -146,7 +146,7 @@
    2.13          val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
    2.14          def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    2.15          def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    2.16 -        def state(command: Command): State = document.current_state(command)
    2.17 +        def state(command: Command): Command.State = document.current_state(command)
    2.18        }
    2.19      }
    2.20    }
    2.21 @@ -281,12 +281,12 @@
    2.22      tmp_states = Map()
    2.23    }
    2.24  
    2.25 -  def current_state(cmd: Command): State =
    2.26 +  def current_state(cmd: Command): Command.State =
    2.27    {
    2.28      require(assignment.is_finished)
    2.29      (assignment.join).get(cmd) match {
    2.30        case Some(cmd_state) => cmd_state.current_state
    2.31 -      case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
    2.32 +      case None => new Command.State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
    2.33      }
    2.34    }
    2.35  }
     3.1 --- a/src/Pure/PIDE/state.scala	Thu Aug 12 13:49:08 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,125 +0,0 @@
     3.4 -/*  Title:      Pure/PIDE/state.scala
     3.5 -    Author:     Fabian Immler, TU Munich
     3.6 -    Author:     Makarius
     3.7 -
     3.8 -Accumulated results from prover.
     3.9 -*/
    3.10 -
    3.11 -package isabelle
    3.12 -
    3.13 -
    3.14 -class State(
    3.15 -  val command: Command,
    3.16 -  val status: Command.Status.Value,
    3.17 -  val forks: Int,
    3.18 -  val reverse_results: List[XML.Tree],
    3.19 -  val markup_root: Markup_Text)
    3.20 -{
    3.21 -  def this(command: Command) =
    3.22 -    this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
    3.23 -
    3.24 -
    3.25 -  /* content */
    3.26 -
    3.27 -  private def set_status(st: Command.Status.Value): State =
    3.28 -    new State(command, st, forks, reverse_results, markup_root)
    3.29 -
    3.30 -  private def add_forks(i: Int): State =
    3.31 -    new State(command, status, forks + i, reverse_results, markup_root)
    3.32 -
    3.33 -  private def add_result(res: XML.Tree): State =
    3.34 -    new State(command, status, forks, res :: reverse_results, markup_root)
    3.35 -
    3.36 -  private def add_markup(node: Markup_Tree): State =
    3.37 -    new State(command, status, forks, reverse_results, markup_root + node)
    3.38 -
    3.39 -  lazy val results = reverse_results.reverse
    3.40 -
    3.41 -
    3.42 -  /* markup */
    3.43 -
    3.44 -  lazy val highlight: Markup_Text =
    3.45 -  {
    3.46 -    markup_root.filter(_.info match {
    3.47 -      case Command.HighlightInfo(_, _) => true
    3.48 -      case _ => false
    3.49 -    })
    3.50 -  }
    3.51 -
    3.52 -  private lazy val types: List[Markup_Node] =
    3.53 -    markup_root.filter(_.info match {
    3.54 -      case Command.TypeInfo(_) => true
    3.55 -      case _ => false }).flatten
    3.56 -
    3.57 -  def type_at(pos: Int): Option[String] =
    3.58 -  {
    3.59 -    types.find(t => t.start <= pos && pos < t.stop) match {
    3.60 -      case Some(t) =>
    3.61 -        t.info match {
    3.62 -          case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty)
    3.63 -          case _ => None
    3.64 -        }
    3.65 -      case None => None
    3.66 -    }
    3.67 -  }
    3.68 -
    3.69 -  private lazy val refs: List[Markup_Node] =
    3.70 -    markup_root.filter(_.info match {
    3.71 -      case Command.RefInfo(_, _, _, _) => true
    3.72 -      case _ => false }).flatten
    3.73 -
    3.74 -  def ref_at(pos: Int): Option[Markup_Node] =
    3.75 -    refs.find(t => t.start <= pos && pos < t.stop)
    3.76 -
    3.77 -
    3.78 -  /* message dispatch */
    3.79 -
    3.80 -  def accumulate(message: XML.Tree): State =
    3.81 -    message match {
    3.82 -      case XML.Elem(Markup(Markup.STATUS, _), elems) =>
    3.83 -        (this /: elems)((state, elem) =>
    3.84 -          elem match {
    3.85 -            case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
    3.86 -            case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
    3.87 -            case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
    3.88 -            case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
    3.89 -            case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
    3.90 -            case _ => System.err.println("Ignored status message: " + elem); state
    3.91 -          })
    3.92 -
    3.93 -      case XML.Elem(Markup(Markup.REPORT, _), elems) =>
    3.94 -        (this /: elems)((state, elem) =>
    3.95 -          elem match {
    3.96 -            case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
    3.97 -              atts match {
    3.98 -                case Position.Range(begin, end) =>
    3.99 -                  if (kind == Markup.ML_TYPING) {
   3.100 -                    val info = Pretty.string_of(body, margin = 40)
   3.101 -                    state.add_markup(
   3.102 -                      command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
   3.103 -                  }
   3.104 -                  else if (kind == Markup.ML_REF) {
   3.105 -                    body match {
   3.106 -                      case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
   3.107 -                        state.add_markup(command.markup_node(
   3.108 -                          begin - 1, end - 1,
   3.109 -                          Command.RefInfo(
   3.110 -                            Position.get_file(props),
   3.111 -                            Position.get_line(props),
   3.112 -                            Position.get_id(props),
   3.113 -                            Position.get_offset(props))))
   3.114 -                      case _ => state
   3.115 -                    }
   3.116 -                  }
   3.117 -                  else {
   3.118 -                    state.add_markup(
   3.119 -                      command.markup_node(begin - 1, end - 1,
   3.120 -                        Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
   3.121 -                  }
   3.122 -                case _ => state
   3.123 -              }
   3.124 -            case _ => System.err.println("Ignored report message: " + elem); state
   3.125 -          })
   3.126 -      case _ => add_result(message)
   3.127 -    }
   3.128 -}
     4.1 --- a/src/Pure/build-jars	Thu Aug 12 13:49:08 2010 +0200
     4.2 +++ b/src/Pure/build-jars	Thu Aug 12 13:59:18 2010 +0200
     4.3 @@ -42,7 +42,6 @@
     4.4    PIDE/document.scala
     4.5    PIDE/event_bus.scala
     4.6    PIDE/markup_node.scala
     4.7 -  PIDE/state.scala
     4.8    PIDE/text_edit.scala
     4.9    System/cygwin.scala
    4.10    System/download.scala