# HG changeset patch # User wenzelm # Date 1282487835 -7200 # Node ID 80d962964216773961521fc4913593d291e09f29 # Parent 79cb7b4c908a7f4381a3dea88888b24330b99794 Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo; diff -r 79cb7b4c908a -r 80d962964216 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sun Aug 22 13:59:47 2010 +0200 +++ b/src/Pure/PIDE/command.scala Sun Aug 22 16:37:15 2010 +0200 @@ -14,11 +14,6 @@ object Command { - case class RefInfo(file: Option[String], line: Option[Int], - command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !? - - - /** accumulated results from prover **/ case class State( @@ -40,17 +35,6 @@ def markup_root: Markup_Tree = markup + markup_root_node - /* markup */ - - private lazy val refs: List[Markup_Tree.Node[Any]] = - markup.filter(_.info match { - case Command.RefInfo(_, _, _, _) => true - case _ => false }).flatten(markup_root_node) - - def ref_at(pos: Text.Offset): Option[Markup_Tree.Node[Any]] = - refs.find(_.range.contains(pos)) - - /* message dispatch */ def accumulate(message: XML.Tree): Command.State = diff -r 79cb7b4c908a -r 80d962964216 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Aug 22 13:59:47 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sun Aug 22 16:37:15 2010 +0200 @@ -38,37 +38,47 @@ class Isabelle_Hyperlinks extends HyperlinkSource { - def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = + def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = { Swing_Thread.assert() Document_Model(buffer) match { case Some(model) => val snapshot = model.snapshot() - val offset = snapshot.revert(original_offset) + val offset = snapshot.revert(buffer_offset) snapshot.node.command_at(offset) match { case Some((command, command_start)) => - snapshot.state(command).ref_at(offset - command_start) match { - case Some(ref) => - val Text.Range(begin, end) = snapshot.convert(ref.range + command_start) + val root_node = + Markup_Tree.Node[Hyperlink]((Text.Range(offset) - command_start), null) + + (snapshot.state(command).markup.select(root_node) { + case XML.Elem(Markup(Markup.ML_REF, _), + List(XML.Elem(Markup(Markup.ML_DEF, props), _))) => +//{{{ + val node_range = root_node.range // FIXME proper range + val Text.Range(begin, end) = snapshot.convert(node_range + command_start) val line = buffer.getLineOfOffset(begin) - ref.info match { - case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => + + (Position.get_file(props), Position.get_line(props)) match { + case (Some(ref_file), Some(ref_line)) => new External_Hyperlink(begin, end, line, ref_file, ref_line) - case Command.RefInfo(_, _, Some(id), Some(offset)) => - snapshot.lookup_command(id) match { // FIXME Command_ID vs. Exec_ID (!??) - case Some(ref_cmd) => - snapshot.node.command_start(ref_cmd) match { - case Some(ref_cmd_start) => - new Internal_Hyperlink(begin, end, line, - snapshot.convert(ref_cmd_start + offset - 1)) - case None => null // FIXME external ref + case _ => + (Position.get_id(props), Position.get_offset(props)) match { + case (Some(ref_id), Some(ref_offset)) => + snapshot.lookup_command(ref_id) match { + case Some(ref_cmd) => + snapshot.node.command_start(ref_cmd) match { + case Some(ref_cmd_start) => + new Internal_Hyperlink(begin, end, line, + snapshot.convert(ref_cmd_start + ref_offset - 1)) // FIXME Command.decode_range + case None => null + } + case None => null } case _ => null } - case _ => null } - case None => null - } +//}}} + }).head.info case None => null } case None => null