# HG changeset patch # User wenzelm # Date 1381529407 -7200 # Node ID ffa4e0b1701e353dd7a23ee21867f941f42bedbe # Parent 148903e47b26adb0eab28f8df23574e7e94e89e7 more strict find_command -- avoid invalid hyperlink_command; diff -r 148903e47b26 -r ffa4e0b1701e src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Oct 11 23:12:04 2013 +0200 +++ b/src/Pure/PIDE/document.scala Sat Oct 12 00:10:07 2013 +0200 @@ -416,7 +416,7 @@ case Some(st) => val command = st.command val node = version.nodes(command.node_name) - Some((node, command)) + if (node.commands.contains(command)) Some((node, command)) else None } def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)