Tweak parentnames attribute on opentheory
authoraspinall
Wed, 08 Sep 2004 21:57:19 +0200
changeset 15192 294f2eb211dd
parent 15191 5ca1fd9dec83
child 15193 4ed712d3551f
Tweak parentnames attribute on opentheory
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  *)