# HG changeset patch
# User wenzelm
# Date 1345664597 -7200
# Node ID 04deeb14327c78556764bef5e0ee4c4e7b7c71d0
# Parent  74ad16f794252d23abf989da739613232d4aec11
add keywords of this node as well (e.g. relevant for Pure.thy);

diff -r 74ad16f79425 -r 04deeb14327c src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Wed Aug 22 21:28:33 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Wed Aug 22 21:43:17 2012 +0200
@@ -108,7 +108,7 @@
       {
         val string = text.toString
         val header = check_thy_text(name, string)
-        val more_uses = find_files(syntax, string)
+        val more_uses = find_files(syntax.add_keywords(header.keywords), string)
         header.copy(uses = header.uses ::: more_uses.map((_, false)))
       })
 }