# HG changeset patch
# User aspinall
# Date 1094673439 -7200
# Node ID 294f2eb211dd5e15287e90866f1a1b228ffada83
# Parent  5ca1fd9dec83784a9c6b607e04dde0f323559f7a
Tweak parentnames attribute on opentheory

diff -r 5ca1fd9dec83 -r 294f2eb211dd src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Sep 08 21:48:10 2004 +0200
+++ b/src/Pure/proof_general.ML	Wed Sep 08 21:57:19 2004 +0200
@@ -777,8 +777,10 @@
 	let 
 	    val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
 	in 
-	    markup_text_attrs str "opentheory" [("thyname",thyname),
-						("parentnames", space_implode ";" imports)]
+	    markup_text_attrs str "opentheory" 
+			      ([("thyname",thyname)] @
+			       (if imports=[] then [] else
+				[("parentnames", (space_implode ";" imports) ^ ";")]))
 	end 
 
     fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)