src/Tools/jEdit/src/isabelle_hyperlinks.scala
changeset 46178 1c5c88f6feb5
parent 45709 87017fcbad83
child 46198 cd040c5772de
     1.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Jan 10 18:12:55 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Jan 10 23:26:27 2012 +0100
     1.3 @@ -57,40 +57,40 @@
     1.4          case Some(model) =>
     1.5            val snapshot = model.snapshot()
     1.6            val markup =
     1.7 -            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
     1.8 -              Markup_Tree.Select[Hyperlink](
     1.9 -                {
    1.10 -                  // FIXME Protocol.Hyperlink extractor
    1.11 -                  case Text.Info(info_range,
    1.12 -                      XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
    1.13 -                    if (props.find(
    1.14 -                      { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
    1.15 -                        case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
    1.16 -                        case _ => false }).isEmpty) =>
    1.17 -                    val Text.Range(begin, end) = info_range
    1.18 -                    val line = buffer.getLineOfOffset(begin)
    1.19 -                    (Position.File.unapply(props), Position.Line.unapply(props)) match {
    1.20 -                      case (Some(def_file), Some(def_line)) =>
    1.21 -                        new External_Hyperlink(begin, end, line, def_file, def_line)
    1.22 -                      case _ if !snapshot.is_outdated =>
    1.23 -                        (props, props) match {
    1.24 -                          case (Position.Id(def_id), Position.Offset(def_offset)) =>
    1.25 -                            snapshot.state.find_command(snapshot.version, def_id) match {
    1.26 -                              case Some((def_node, def_cmd)) =>
    1.27 -                                def_node.command_start(def_cmd) match {
    1.28 -                                  case Some(def_cmd_start) =>
    1.29 -                                    new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    1.30 -                                      def_cmd_start + def_cmd.decode(def_offset))
    1.31 -                                  case None => null
    1.32 -                                }
    1.33 -                              case None => null
    1.34 -                            }
    1.35 -                          case _ => null
    1.36 -                        }
    1.37 -                      case _ => null
    1.38 -                    }
    1.39 -                },
    1.40 -                Some(Set(Isabelle_Markup.ENTITY))))
    1.41 +            snapshot.select_markup[Hyperlink](
    1.42 +              Text.Range(buffer_offset, buffer_offset + 1),
    1.43 +              Some(Set(Isabelle_Markup.ENTITY)),
    1.44 +              {
    1.45 +                // FIXME Protocol.Hyperlink extractor
    1.46 +                case Text.Info(info_range,
    1.47 +                    XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
    1.48 +                  if (props.find(
    1.49 +                    { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
    1.50 +                      case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
    1.51 +                      case _ => false }).isEmpty) =>
    1.52 +                  val Text.Range(begin, end) = info_range
    1.53 +                  val line = buffer.getLineOfOffset(begin)
    1.54 +                  (Position.File.unapply(props), Position.Line.unapply(props)) match {
    1.55 +                    case (Some(def_file), Some(def_line)) =>
    1.56 +                      new External_Hyperlink(begin, end, line, def_file, def_line)
    1.57 +                    case _ if !snapshot.is_outdated =>
    1.58 +                      (props, props) match {
    1.59 +                        case (Position.Id(def_id), Position.Offset(def_offset)) =>
    1.60 +                          snapshot.state.find_command(snapshot.version, def_id) match {
    1.61 +                            case Some((def_node, def_cmd)) =>
    1.62 +                              def_node.command_start(def_cmd) match {
    1.63 +                                case Some(def_cmd_start) =>
    1.64 +                                  new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    1.65 +                                    def_cmd_start + def_cmd.decode(def_offset))
    1.66 +                                case None => null
    1.67 +                              }
    1.68 +                            case None => null
    1.69 +                          }
    1.70 +                        case _ => null
    1.71 +                      }
    1.72 +                    case _ => null
    1.73 +                  }
    1.74 +              })
    1.75            markup match {
    1.76              case Text.Info(_, Some(link)) #:: _ => link
    1.77              case _ => null