src/Tools/jEdit/src/proofdocument/state.scala
changeset 34817 b4efd0ef2f3e
parent 34813 f0107bc96961
child 34859 f986d84dd44b
equal deleted inserted replaced
34816:d33312514220 34817:b4efd0ef2f3e
    79             elem match {
    79             elem match {
    80               case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    80               case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    81               case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    81               case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    82               case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    82               case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    83               case XML.Elem(kind, atts, body) =>
    83               case XML.Elem(kind, atts, body) =>
    84                 val (begin, end) = Position.offsets_of(atts)
    84                 val (begin, end) = Position.get_offsets(atts)
    85                 if (begin.isEmpty || end.isEmpty) state
    85                 if (begin.isEmpty || end.isEmpty) state
    86                 else if (kind == Markup.ML_TYPING) {
    86                 else if (kind == Markup.ML_TYPING) {
    87                   val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
    87                   val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
    88                   state.add_markup(
    88                   state.add_markup(
    89                     command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
    89                     command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
    92                   body match {
    92                   body match {
    93                     case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    93                     case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    94                       state.add_markup(command.markup_node(
    94                       state.add_markup(command.markup_node(
    95                         begin.get - 1, end.get - 1,
    95                         begin.get - 1, end.get - 1,
    96                         Command.RefInfo(
    96                         Command.RefInfo(
    97                           Position.file_of(atts),
    97                           Position.get_file(atts),
    98                           Position.line_of(atts),
    98                           Position.get_line(atts),
    99                           Position.id_of(atts),
    99                           Position.get_id(atts),
   100                           Position.offset_of(atts))))
   100                           Position.get_offset(atts))))
   101                     case _ => state
   101                     case _ => state
   102                   }
   102                   }
   103                 }
   103                 }
   104                 else {
   104                 else {
   105                   state.add_markup(
   105                   state.add_markup(