# 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)