src/Tools/jEdit/src/prover/State.scala
author wenzelm
Sun Sep 06 22:27:32 2009 +0200 (2009-09-06)
changeset 34717 3f32e08bbb6c
parent 34715 826e476947f9
child 34724 b1079c3ba1da
permissions -rw-r--r--
sidekick root data: set buffer length to avoid crash of initial caret move;
separate Markup_Node, Markup_Tree, Markup_Text;
added Markup_Text.flatten;
Command.type_at: null-free version;
eliminated Command.RootInfo;
simplified printing of TypeInfo, RefInfo;
added Command.content(Int, Int);
     1 /*
     2  * Accumulating results from prover
     3  *
     4  * @author Fabian Immler, TU Munich
     5  * @author Makarius
     6  */
     7 
     8 package isabelle.prover
     9 
    10 
    11 class State(
    12   val command: Command,
    13   val status: Command.Status.Value,
    14   rev_results: List[XML.Tree],
    15   val markup_root: Markup_Text)
    16 {
    17   def this(command: Command) =
    18     this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
    19 
    20 
    21   /* content */
    22 
    23   private def set_status(st: Command.Status.Value): State =
    24     new State(command, st, rev_results, markup_root)
    25 
    26   private def add_result(res: XML.Tree): State =
    27     new State(command, status, res :: rev_results, markup_root)
    28 
    29   private def add_markup(node: Markup_Tree): State =
    30     new State(command, status, rev_results, markup_root + node)
    31 
    32   lazy val results = rev_results.reverse
    33 
    34 
    35   /* markup */
    36 
    37   lazy val highlight: Markup_Text =
    38   {
    39     markup_root.filter(_.info match {
    40       case Command.HighlightInfo(_) => true
    41       case _ => false
    42     })
    43   }
    44 
    45   private lazy val types: List[Markup_Node] =
    46     markup_root.filter(_.info match {
    47       case Command.TypeInfo(_) => true
    48       case _ => false }).flatten
    49 
    50   def type_at(pos: Int): Option[String] =
    51   {
    52     types.find(t => t.start <= pos && pos < t.stop) match {
    53       case Some(t) =>
    54         t.info match {
    55           case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
    56           case _ => None
    57         }
    58       case None => None
    59     }
    60   }
    61 
    62   private lazy val refs: List[Markup_Node] =
    63     markup_root.filter(_.info match {
    64       case Command.RefInfo(_, _, _, _) => true
    65       case _ => false }).flatten
    66 
    67   def ref_at(pos: Int): Option[Markup_Node] =
    68     refs.find(t => t.start <= pos && pos < t.stop)
    69 
    70 
    71   /* message dispatch */
    72 
    73   def + (message: XML.Tree): State =
    74   {
    75     val changed: State =
    76       message match {
    77         case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
    78           (this /: elems)((state, elem) =>
    79             elem match {
    80               case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    81               case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    82               case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    83               case XML.Elem(kind, atts, body) =>
    84                 val (begin, end) = Position.offsets_of(atts)
    85                 if (begin.isEmpty || end.isEmpty) state
    86                 else if (kind == Markup.ML_TYPING) {
    87                   val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
    88                   state.add_markup(
    89                     command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
    90                 }
    91                 else if (kind == Markup.ML_REF) {
    92                   body match {
    93                     case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    94                       state.add_markup(command.markup_node(
    95                         begin.get - 1, end.get - 1,
    96                         Command.RefInfo(
    97                           Position.file_of(atts),
    98                           Position.line_of(atts),
    99                           Position.id_of(atts),
   100                           Position.offset_of(atts))))
   101                     case _ => state
   102                   }
   103                 }
   104                 else {
   105                   state.add_markup(
   106                     command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
   107                 }
   108               case _ =>
   109                 System.err.println("ignored status report: " + elem)
   110                 state
   111             })
   112         case _ => add_result(message)
   113       }
   114     if (!(this eq changed)) command.changed()
   115     changed
   116   }
   117 }